--- /dev/null
+---
+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;
+ }
+}
projects / web.git / blobdiff