---
-# YAML front matter
+hide: true
---
@charset "utf-8";
/* 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;
-$link-color: #9ed2ff;
-$link-color-visited: #bfe1ff;
-$link-color-hover: #5089ba;
+$navi-indent: 1.2em;
+$frame-max-width: 50em;
+$intrusion-width: 1.0em;
+$outer-margin: 0.8em;
+$full-content-width: $frame-max-width + $navi-width + 2*$outer-margin + $intrusion-width;
+$background-color: white;
+$text-color: #313131;
+$light-text-color: #808080;
+$code-background-color: #F7F7F7;
+$link-color: #268BD2;
/* General page structure */
body { /* This centers us in the page, and handles the "too wide" case */
- padding: $outer-margin;
+ padding: 0;
margin: 0 auto;
color: $text-color;
- background-color: $outer-background-color;
- max-width: calc(#{$frame-max-width + 2 * $navi-width} + 2px);
+ 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 */
+#-frame { /* Add a frame, full height */
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);
+ padding-top: 1em;
+ border-left: solid $text-color 1px;
+ min-height: calc(100vh);
}
/* The content of the frame */
-#title {
- border-bottom: solid $title-color 2px;
- text-align: center;
-}
-#title h1 {
- padding: 0 0.7em;
- margin-bottom: 0;
+#-title h1 {
+ margin: 0;
}
-#content {
- padding: 0.7em;
+#-content {
+ margin-left: $intrusion-width;
+ padding: $outer-margin;
padding-top: 1px; /* If we use 0 here, things get ugly. What?!? */
}
/* Navigation menu */
-#navi {
- /* No border, no padding, so all the width computations become easy. */
- float: left;
- background-color: $outer-background-color;
- width: $navi-width;
+#-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};
- margin-bottom: calc(-100% - #{$frame-max-width});
-}
-#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%;
+ /* 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: center;
-}
-#navi li.current
-{
- border-color: $current-color;
-}
-#navi li:hover {
- border-color: $title-color;
- border-radius: 0;
+ 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;
+ }
}
-#navi li:hover a {
- color: $text-color;
+
+/* 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 + 2 * $outer-margin } ) {
- body, #frame, #title, #content, #navi {
+@media screen and (max-width:#{ $frame-max-width + 2*$outer-margin } ) {
+ body, #-frame, #-title, #-content, #-navi {
margin: 0;
+ padding: 0;
+ height: auto;
width: auto;
max-width: none;
clear: both;
- }
- #navi {
- /* Place navi above the title */
float: none;
position: static;
- background-color: $inner-background-color;
- padding: 0;
- }
- #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: "» ";
+ #-content {
+ padding: $outer-margin;
}
- #navi li.child:before {
- content: "» ";
- }
- #navi li.child + li:before {
- content: "| ";
- }
- #navi li {
- border: none;
- }
- #navi li.current a {
- text-decoration: underline;
+ #-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 {
+ body, #-frame, #-title, #-content {
margin: 0;
padding: 0;
width: auto;
max-width: none;
border: none;
}
- #title h1 {
+ #-title h1 {
border: none;
}
- #navi {
+ #-navi {
display: none;
}
}
-/* RST styling */
-article.rst dt {
- font-weight: bold;
-}
-article.rst dd {
- margin-bottom: 1em;
-}
-article.rst a.rst-footnote {
- vertical-align: super;
-}
-article.rst div.rst-footnote {
- display: table;
-}
-article.rst div.rst-footnote > * {
- display: table-cell;
-}
-article.rst div.rst-footnote a {
- min-width: 3em;
-}
-article.rst .rst-literal, article.rst pre {
- font-family: monospace;
- font-size: 82%;
-}
-article.rst .rst-literal {
- padding: 0.1em 0.2em;
- background-color: $outer-background-color;
-}
-article.rst pre {
- padding: 0.6em;
- background-color: $outer-background-color;
-}
-
/* Content styling */
-#content p {
- margin: 0.5em 0;
- line-height: 1.3;
-}
-#content a {
- color:$link-color;
-}
-#content a:visited {
- color:$link-color-visited;
-}
-#content a:hover {
- color:$link-color-hover;
+#-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.9em;
+ }
+ }
+ .subtitle {
+ margin-top: 1.5em;
+ }
+
+ #-title {
+ clear: both;
+ }
+
+ 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;
+ }
+ a {
+ text-decoration: none;
+ color: $link-color;
+ }
+ a:hover, a:focus {
+ text-decoration: underline;
+ }
}