diff options
Diffstat (limited to 'src/util/doc.css')
-rw-r--r-- | src/util/doc.css | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/src/util/doc.css b/src/util/doc.css new file mode 100644 index 0000000..ab653e4 --- /dev/null +++ b/src/util/doc.css @@ -0,0 +1,67 @@ +#main { + margin-left: auto; + margin-right: auto; + max-width: 55em; + text-align: justify; +} + +h2 { + font-family: monospace; + margin-bottom: 2em; + background-color: #b2c9db; + padding: 7px; + border-radius: 7px; +} + +ol { + list-style: none; + margin-bottom: 4em; +} + +li a { + color: black; +} + +li.header { + margin-top: 1em; + margin-bottom: 0.3em; + font-weight: bold; +} + +div.decl p:first-child { + margin-top: 2.5em; +} + +div.decl p:first-child .first-word { + font-weight: bold; + font-family: monospace; +} + +.sectionpreamble { + margin-top: 5em; +} + +.sectionpreamble p:first-child { + font-weight: bold; + font-size: 1.5em; +} + +.section pre { + background-color: #b2c9db; + padding: 5px; + border-radius: 5px; +} + +td { + padding: 2px; +} + +tr:nth-child(even) { + background-color: #eee; +} + +tr.header td { + font-weight: bold; + padding-top: 1em; + padding-bottom: 0.5em; +} |