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