9 $frame-max-width: 50em;
10 $intrusion-width: 1.0em;
13 $small-width: $frame-max-width + 2*$outer-margin;
14 $medium-width: $small-width + $intrusion-width + $navi-width;
16 $background-color: white;
18 $light-text-color: #808080;
19 $code-background-color: #F7F7F7;
24 font-family: DejaVu Sans, Verdana, Arial, sans-serif;
30 text-decoration: none;
34 text-decoration: underline;
36 /* Header Size & Spacing */
65 /* Layout and Color stuff */
67 /* General page structure */
71 body { /* This centers us in the page, and handles the "too wide" case */
74 background-color: $background-color;
75 max-width: calc(#{$medium-width + $navi-width} + 1px); /* add the right-hand "navi" space for centering - and the border... ;-) */
77 #-frame { /* Add a frame, full height */
78 margin: 0 $navi-width;
79 padding-top: $outer-margin;
80 border-left: solid $text-color 1px;
81 min-height: calc(100vh - #{$outer-margin});
84 /* The content of the frame */
86 margin-left: $intrusion-width;
87 padding: $outer-margin;
88 padding-top: 1px; /* If we use 0 here, some paddings add up things get ugly. What?!? */
95 margin-left: -#{$navi-indent};
96 width: #{$navi-width + $navi-indent};
97 /* Put it into the right spot */
100 left: calc(-#{$navi-width} - 1px);
101 /* Make it not take space away from the main text */
108 list-style-type: none;
109 /* Indentation for nested nodes */
110 margin-left: $navi-indent;
114 width: calc(100% - 2*0.25em - 1px + #{$intrusion-width}); /* minus the padding, the border, and plus how much we want to overlap */
115 padding: 0.08em 0.25em 0.02em; /* top left-right bottom */
116 /* Always have *one* border, for the width to stay constant */
117 border-left: solid transparent 1px;
124 border: solid $text-color 1px;
125 border-right: none; /* solid $background-color 1px; */
126 background-color: $background-color;
130 border-bottom: solid $text-color 1px;
131 margin-bottom: 0.3em;
135 /* Medium-size screens */
136 @media screen and (max-width:#{ $medium-width + $navi-width } ) {
139 max-width: calc(#{ $medium-width} + 1px); /* add the left-hand *only* navi space for centering - and the border... ;-) */
147 @media screen and (max-width:#{ $small-width } ) {
151 body, #-frame, #-content, #-navi {
162 padding: $outer-margin;
165 padding: $outer-margin;
166 border-bottom: solid $text-color 1px;
174 display: inline-block;
176 /* Display only parent and children, and decorate them appropriately */
178 display:inline-block;
179 margin: 0 0.3em !important;
180 padding: 0 !important;
181 border: none !important;
182 width: auto !important;
188 text-decoration: underline;
190 li.parent::before, li.current:before {
196 li.child + li.child::before {
204 body, #-frame, #-content {
219 /* Content styling */
223 color: $light-text-color;
226 .pretitle, .subtitle {
228 display: inline-block;
248 background-color: $code-background-color;
249 font-family: monospace;
253 padding: 0.1em 0.2em;