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