/* ================== STYLING ================= */ * { box-sizing: border-box; } /* Body styling */ body { font-family: sans; font-size: 12pt; color: black; background: #bdbdbd; margin: 0; } h1, h2, h3, h4, h5, h6 { font-family: times; } h3, h4, h5, h6 { font-weight: normal; } p { margin-top: 0px; } p.tiny { font-size: 5pt; } li { margin-bottom: 1em; } ul { margin-top: 0px; } pre { margin-left: 20px; margin-right: 20px; margin-top: 0px; background-color: white; border-style: solid; border-color: #888A85; border-width: 1px; font-size: 11pt; font-family: monospace; } pre.commandLine { background-color: #2E3436; color: #C3F097; } a { text-decoration: none; } a:link { color: #90BA45; } a:hover { color: #FF2A00; } a:visited { color: #FCAF3E; } span.structure { color: #FCAF3E; font-weight: bold; } span.primitive { color: #729FCF; font-weight: bold; } span.className { color: #8AE234; font-weight: bold; } span.type { color: #729FCF; } span.value { color: #C17D11; } span.function { color: #75507B; } span.name { color: #8AE234; } span.comment { color: #888A85; } /* in-line code block */ span.codeBlockInText{ background-color: white; border-color: black; border-style: solid; border-width: 1px; font-size: 11pt; font-family: monospace; padding-left: 5px; padding-right: 5px; } .disclaimer { font-size: 8pt; color: red; } /* TODO The following is broken because we're not using tables anymore. Find another solution. */ p.explanation { border-left-color: #8ED424; } p.general { border-left-color: #888A85; } p.warning { border-left-color: #EF2929; } /* ================== LAYOUT ================== */ /* Header containing title etc. */ .header { text-align: center; background: #795548; color: white; padding: 4px; } /* Navigation bar at top of page */ .navbar { display: flex; background-color: #4b2c20; } /* Styling of navigation bar links */ .navbar a { color: white; padding: 14px 20px; text-decoration: none; text-align: center; } /* Change color of navigation bar links on hover */ .navbar a:hover { background-color: #a98274; color: black; } /* Align page elements in a row */ .row { display: flex; flex-wrap: wrap; } /* Sidebar column */ .side { flex: 15%; font-size: 10pt; font-style: italic; background-color: #efefef; padding: 20px; max-width: 500px; } /* Main column */ .main { flex: 40%; background-color: #ffffff; padding: 20px; max-width: 1000px; } /* Spacer */ .spacer { flex: auto; } /* Footer */ .footer { padding: 20px; text-align: center; background: #8d8d8d; } /* Adaptively change layout based on window size */ @media only screen and (max-width: 1000px) { .spacer { display: none; } .main, .side { max-width: none; } } @media only screen and (max-width: 700px) { .row, .navbar { flex-direction: column; } }