style.scss

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