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