--- 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; $outer-margin: 1em; $frame-max-width: 52em; $frame-color: #121212; $title-color: #08f; $navi-color: #36ff00; $current-color: #ffa700; $outer-background-color: #505050; $inner-background-color: #252525; $text-color: #DDD; $light-text-color: #888; $link-color: #9ed2ff; $link-color-visited: #bfe1ff; $link-color-hover: #5089ba; /* General page structure */ body { /* This centers us in the page, and handles the "too wide" case */ padding: $outer-margin; margin: 0 auto; color: $text-color; background-color: $outer-background-color; max-width: calc(#{$frame-max-width + 2 * $navi-width} + 2px); } #-frame { /* Add a frame */ margin: 0 $navi-width; border: solid $frame-color 1px; background-color: $inner-background-color; border-radius: 10px; min-height: calc(100vh - #{2* $outer-margin} - 2px); } /* The content of the frame */ #-title { border-bottom: solid $title-color 2px; text-align: center; } #-title h1 { padding: 0 0.7em; margin-bottom: 0; } #-content { padding: 0.7em; padding-top: 1px; /* If we use 0 here, things get ugly. What?!? */ } /* Navigation menu */ #-navi { background-color: $outer-background-color; /* No border, no padding, so all the width computations become easy. */ padding: 0; margin: 0; width: $navi-width; /* 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; } #-navi ul { margin: 0px; padding: 0px; list-style-type: none; } #-navi ul ul { /* Indentation for nested nodes */ margin-left: 1.2em; } #-navi li { /* Border around the links */ margin-bottom:0.1em; background-color: $inner-background-color; border-left: solid $navi-color 2px; border-right: solid $navi-color 2px; border-top-left-radius: 10px; border-bottom-left-radius: 10px; } #-navi li a { display: block; width: 100%; color: $link-color; font-size:110%; text-decoration: none; text-align: center; } #-navi li.current { border-color: $current-color; } #-navi li:hover { border-color: $title-color; border-radius: 0; } #-navi li:hover a { color: $text-color; } /* Small screens */ @media screen and (max-width:#{ $frame-max-width + 2 * $outer-margin } ) { body, #-frame, #-title, #-content, #-navi { margin: 0; width: auto; max-width: none; clear: both; } #-navi { /* Place navi above the title */ float: none; position: static; background-color: $inner-background-color; padding: 0; height: auto; } #-navi ul, #-navi ul ul, #-navi li, #-navi li a { margin: 0; padding: 0; display: inline; } #-navi > ul { padding: 0.3em; display: block; border-bottom: solid $navi-color 2px; } /* Display only parent and children, and deocare them appropriately */ #-navi li { display:inline-block; margin: 0 0.2em; } #-navi li.sibling { display:none; } #-navi li.parent:before, #-navi li.current:before { content: "» "; } #-navi li.child:before { content: "» "; } #-navi li.child + li:before { content: "| "; } #-navi li { border: none; } #-navi li.current a { text-decoration: underline; } } /* 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; background-color: $outer-background-color; font-family: monospace; font-size: 82%; } pre { padding: 0.6em; background-color: $outer-background-color; } pre code { padding: 0; } p { margin: 0.5em 0; line-height: 1.3; } a { color:$link-color; } a:visited { color:$link-color-visited; } a:hover { color:$link-color-hover; } }