style.scss

   1 ---
   2 hide: true
   3 ---
   4 @charset "utf-8";
   5
   6 /* General Fonts */
   7 html, body, div, p {
   8     font-family: DejaVu Sans, Verdana, Arial, sans-serif;
   9     font-size: 12pt;
  10 }
  11 /* Header Size & Spacing */
  12 h1 {
  13     margin-top: 0.1em;
  14     font-size: 200%;
  15     margin-bottom: 0.4em;
  16 }
  17 h2 {
  18     margin-top: 0.5em;
  19     font-size: 150%;
  20     margin-bottom: 0.2em;
  21 }
  22 h3 {
  23     margin-top: 0.5em;
  24     font-size: 135%;
  25     margin-bottom: 0.1em;
  26 }
  27 h4 {
  28     margin-top: 0.5em;
  29     font-size: 120%;
  30     margin-bottom: 0.0em;
  31 }
  32
  33 /* Layout and Color stuff */
  34 $navi-width:      11em;
  35 $navi-indent:     1.2em;
  36 $frame-max-width: 50em;
  37 $intrusion-width: 0.8em;
  38 $outer-margin:    0.8em;
  39 $full-content-width: $frame-max-width + $navi-width + 2*$outer-margin + $intrusion-width;
  40
  41 $frame-color: #121212;
  42 $title-color: #08f;
  43 $navi-color: #36ff00;
  44 $current-color: #ffa700;
  45 $background-color: white;
  46 $text-color:             #313131;
  47 $code-background-color: #505050;
  48 $light-text-color:       #888;
  49 $link-color: #268BD2;
  50
  51
  52 /* General page structure */
  53 body { /* This centers us in the page, and handles the "too wide" case */
  54     padding: 0;
  55     margin: 0 auto;
  56     color: $text-color;
  57     background-color: $background-color;
  58     max-width: calc(#{$full-content-width + $navi-width} + 1px); /* add the right-hand "navi" for centering - and the border... ;-) */
  59 }
  60 #-frame { /* Add a frame, full height */
  61     margin: 0 $navi-width;
  62     padding-top: 1em;
  63     border-left: solid $text-color 1px;
  64     min-height: calc(100vh);
  65 }
  66
  67 /* The content of the frame */
  68 #-title h1 {
  69     margin: 0;
  70 }
  71 #-content {
  72     margin-left: $intrusion-width;
  73     padding: $outer-margin;
  74     padding-top: 1px; /* If we use 0 here, things get ugly. What?!? */
  75 }
  76
  77 /* Navigation menu */
  78 #-navi {
  79     padding: 0;
  80     margin: 0;
  81     margin-left: -#{$navi-indent};
  82     width: #{$navi-width + $navi-indent};
  83     /* Put it into the right spot */
  84     float: left;
  85     position: relative;
  86     left: -#{$navi-width};
  87     /* Make it not take space away from the main text */
  88     height: 0;
  89     overflow: visible;
  90
  91     ul {
  92         margin: 0;
  93         padding: 0;
  94         list-style-type: none;
  95         /* Indentation for nested nodes */
  96         margin-left: $navi-indent;
  97     }
  98     a {
  99         display: block;
 100         width: calc(100% - 2*0.1em - 2*1px + #{$intrusion-width});
 101         padding: 0 0.1em;
 102         /* Always have a border, for the width to stay constant */
 103         border: solid transparent 1px;
 104
 105         color: $link-color;
 106         font-size:110%;
 107         text-decoration: none;
 108         text-align: left;
 109     }
 110     a.current {
 111         padding-top: 0.1em;
 112         margin:  0.05em 0;
 113         border: solid $text-color 1px;
 114         border-right: solid $background-color 1px;
 115         background-color: $background-color;
 116     }
 117     a.root {
 118         margin-top: 0.5em;
 119         border-bottom: solid $text-color 1px;
 120         margin-bottom: 0.3em;
 121     }
 122     a:hover, a:focus {
 123         text-decoration: underline;
 124     }
 125 }
 126
 127 /* Medium-size screens */
 128 @media screen and (max-width:#{ $full-content-width } ) {
 129     #-frame {
 130         margin-right: 0;
 131     }
 132 }
 133
 134 /* Small screens */
 135 @media screen and (max-width:#{ $frame-max-width } ) {
 136     body, #-frame, #-title, #-content, #-navi {
 137         margin: 0;
 138         padding: 0;
 139         height: auto;
 140         width: auto;
 141         max-width: none;
 142         clear: both;
 143         float: none;
 144         position: static;
 145     }
 146     #-content {
 147         padding: $outer-margin;
 148     }
 149     #-navi {
 150         padding: $outer-margin;
 151         border-bottom: solid $text-color 1px;
 152
 153         ul {
 154             display: inline;
 155             padding: 0;
 156             margin: 0;
 157         }
 158         li {
 159             display: inline-block;
 160         }
 161         /* Display only parent and children, and decorate them appropriately */
 162         a {
 163             display:inline-block;
 164             margin: 0 0.3em !important;
 165             padding: 0 !important;
 166             border: none !important;
 167             width: auto !important;
 168         }
 169         a.sibling {
 170             display:none;
 171         }
 172         a.current {
 173             text-decoration: underline;
 174         }
 175         li.parent::before, li.current:before {
 176             content: "»";
 177         }
 178         li.child::before {
 179             content: "»";
 180         }
 181         li.child + li.child::before {
 182             content: "|";
 183         }
 184     }
 185 }
 186
 187 /* Printing */
 188 @media print {
 189     body, #-frame, #-title, #-content {
 190         margin: 0;
 191         padding: 0;
 192         width: auto;
 193         max-width: none;
 194         border: none;
 195     }
 196     #-title h1 {
 197         border: none;
 198     }
 199     #-navi {
 200         display: none;
 201     }
 202 }
 203
 204 /* Content styling */
 205 #-content {
 206     .subtitle .side {
 207         float: right;
 208         color: $light-text-color;
 209     }
 210
 211     code {
 212         padding: 0.1em 0.2em;
 213         font-family: monospace;
 214         font-size: 82%;
 215     }
 216     pre {
 217         padding: 0.6em;
 218     }
 219     pre code {
 220         background-color: $code-background-color;
 221         padding: 0;
 222     }
 223
 224     p {
 225         margin: 0.5em 0;
 226         line-height: 1.3;
 227     }
 228     a {
 229         text-decoration: none;
 230         color:$link-color;
 231     }
 232     a:hover, a:focus {
 233         text-decoration: underline;
 234     }
 235 }