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