-$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;
- }
-}