--- hide: true --- @charset "utf-8"; /* General Fonts */ html, body, div, p { font-family: DejaVu Sans, Verdana, Arial, sans-serif; font-size: 12pt; } /* Header Size & Spacing */ h1 { margin-top: 0.1em; font-size: 200%; margin-bottom: 0.4em; } h2 { margin-top: 0.5em; font-size: 150%; margin-bottom: 0.2em; } h3 { margin-top: 0.5em; font-size: 135%; margin-bottom: 0.1em; } h4 { margin-top: 0.5em; font-size: 120%; margin-bottom: 0.0em; } /* Layout and Color stuff */ $navi-width: 11em; $navi-indent: 1.2em; $frame-max-width: 50em; $intrusion-width: 0.8em; $outer-margin: 0.8em; $full-content-width: $frame-max-width + $navi-width + 2*$outer-margin + $intrusion-width; $frame-color: #121212; $title-color: #08f; $navi-color: #36ff00; $current-color: #ffa700; $background-color: white; $text-color: #313131; $code-background-color: #505050; $light-text-color: #888; $link-color: #268BD2; /* General page structure */ body { /* This centers us in the page, and handles the "too wide" case */ padding: 0; margin: 0 auto; color: $text-color; background-color: $background-color; max-width: calc(#{$full-content-width + $navi-width} + 1px); /* add the right-hand "navi" for centering - and the border... ;-) */ } #-frame { /* Add a frame, full height */ margin: 0 $navi-width; padding-top: 1em; border-left: solid $text-color 1px; min-height: calc(100vh); } /* The content of the frame */ #-title h1 { margin: 0; } #-content { margin-left: $intrusion-width; padding: $outer-margin; padding-top: 1px; /* If we use 0 here, things get ugly. What?!? */ } /* Navigation menu */ #-navi { padding: 0; margin: 0; margin-left: -#{$navi-indent}; width: #{$navi-width + $navi-indent}; /* Put it into the right spot */ float: left; position: relative; left: -#{$navi-width}; /* Make it not take space away from the main text */ height: 0; overflow: visible; ul { margin: 0; padding: 0; list-style-type: none; /* Indentation for nested nodes */ margin-left: $navi-indent; } a { display: block; width: calc(100% - 2*0.1em - 2*1px + #{$intrusion-width}); padding: 0 0.1em; /* Always have a border, for the width to stay constant */ border: solid transparent 1px; color: $link-color; font-size:110%; text-decoration: none; text-align: left; } a.current { padding-top: 0.1em; margin: 0.05em 0; border: solid $text-color 1px; border-right: solid $background-color 1px; background-color: $background-color; } a.root { margin-top: 0.5em; border-bottom: solid $text-color 1px; margin-bottom: 0.3em; } a:hover, a:focus { text-decoration: underline; } } /* Medium-size screens */ @media screen and (max-width:#{ $full-content-width } ) { #-frame { margin-right: 0; } } /* Small screens */ @media screen and (max-width:#{ $frame-max-width } ) { body, #-frame, #-title, #-content, #-navi { margin: 0; padding: 0; height: auto; width: auto; max-width: none; clear: both; float: none; position: static; } #-content { padding: $outer-margin; } #-navi { padding: $outer-margin; border-bottom: solid $text-color 1px; ul { display: inline; padding: 0; margin: 0; } li { display: inline-block; } /* Display only parent and children, and decorate them appropriately */ a { display:inline-block; margin: 0 0.3em !important; padding: 0 !important; border: none !important; width: auto !important; } a.sibling { display:none; } a.current { text-decoration: underline; } li.parent::before, li.current:before { content: "»"; } li.child::before { content: "»"; } li.child + li.child::before { content: "|"; } } } /* Printing */ @media print { body, #-frame, #-title, #-content { margin: 0; padding: 0; width: auto; max-width: none; border: none; } #-title h1 { border: none; } #-navi { display: none; } } /* Content styling */ #-content { .subtitle .side { float: right; color: $light-text-color; } code { padding: 0.1em 0.2em; font-family: monospace; font-size: 82%; } pre { padding: 0.6em; } pre code { background-color: $code-background-color; padding: 0; } p { margin: 0.5em 0; line-height: 1.3; } a { text-decoration: none; color:$link-color; } a:hover, a:focus { text-decoration: underline; } }