--- hide: true --- @charset "utf-8"; /* Variables */ $navi-width: 11em; $navi-indent: 1.2em; $frame-max-width: 50em; $intrusion-width: 1.0em; $outer-margin: 0.8em; $small-width: $frame-max-width + 2*$outer-margin; $medium-width: $small-width + $intrusion-width + $navi-width; $background-color: white; $text-color: #313131; $light-text-color: #808080; $code-background-color: #F7F7F7; $link-color: #268BD2; /* General Fonts */ html, body, div, p { font-family: DejaVu Sans, Verdana, Arial, sans-serif; font-size: 12pt; color: $text-color; } /* Links */ a { text-decoration: none; color: $link-color; } a:hover, a:focus { text-decoration: underline; } /* Header Size & Spacing */ h1, h2, h3, h4 { color: $text-color; a { color: $text-color; } } h1 { margin-top: 0.1em; font-size: 200%; margin-bottom: 0.2em; } 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 */ /* General page structure */ html { overflow-y: scroll; } body { /* This centers us in the page, and handles the "too wide" case */ padding: 0; margin: 0 auto; background-color: $background-color; max-width: calc(#{$medium-width + $navi-width} + 1px); /* add the right-hand "navi" space for centering - and the border... ;-) */ } #-frame { /* Add a frame, full height */ margin: 0 $navi-width; padding-top: $outer-margin; border-left: solid $text-color 1px; min-height: calc(100vh - #{$outer-margin}); } /* The content of the frame */ #-content { margin-left: $intrusion-width; padding: $outer-margin; padding-top: 1px; /* If we use 0 here, some paddings add up 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: calc(-#{$navi-width} - 1px); /* 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.25em - 1px + #{$intrusion-width}); /* minus the padding, the border, and plus how much we want to overlap */ padding: 0.08em 0.25em 0.02em; /* top left-right bottom */ /* Always have *one* border, for the width to stay constant */ border-left: solid transparent 1px; font-size:110%; text-align: left; } a.current { padding-top: 0.12em; border: solid $text-color 1px; border-right: none; /* solid $background-color 1px; */ background-color: $background-color; } a.root { margin-top: 0.7em; border-bottom: solid $text-color 1px; margin-bottom: 0.3em; } } /* Medium-size screens */ @media screen and (max-width:#{ $medium-width + $navi-width } ) { body { margin-left: 0; max-width: calc(#{ $medium-width} + 1px); /* add the left-hand *only* navi space for centering - and the border... ;-) */ } #-frame { margin-right: 0; } } /* Small screens */ @media screen and (max-width:#{ $small-width } ) { html { overflow-y: auto; } body, #-frame, #-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, #-content { margin: 0; padding: 0; width: auto; max-width: none; border: none; } #-title h1 { border: none; } #-navi { display: none; } } /* Content styling */ #-content { .side { float: right; color: $light-text-color; } .pretitle, .subtitle { h1 { display: inline-block; font-size: 165%; } .side { margin-left: 0.5em; margin-top: 0.8em; } } .pretitle { margin-bottom: 1em; } .subtitle { margin-top: 2em; } .title { clear: both; margin-bottom: 1em; } pre, code { background-color: $code-background-color; font-family: monospace; font-size: 82%; } code { padding: 0.1em 0.2em; } pre { padding: 0.6em; } pre code { padding: 0; font-size: 100%; } p { margin: 0.5em 0; line-height: 1.3; } }