diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss
index 5404d01..3644603 100644
--- a/assets/sass/_content.scss
+++ b/assets/sass/_content.scss
@@ -138,6 +138,14 @@ pre > code {
     font-size: 0.9em;
 }
 
+details {
+    font-size: 0.95rem;
+
+    summary {
+        cursor: pointer;
+    }
+}
+
 table.table {
     border: 1px solid $faded;
     border-collapse: collapse;
diff --git a/assets/sass/_syntax.scss b/assets/sass/_syntax.scss
index f1aa7b2..7b96ba7 100644
--- a/assets/sass/_syntax.scss
+++ b/assets/sass/_syntax.scss
@@ -1,70 +1,178 @@
-pre.highlight { background-color: #444444; color: #cccccc }
-.highlight .hll { background-color: #444444; color: #cccccc }
-.highlight .c { color: #608b4e } /* Comment */
-.highlight .err { color: #cccccc; border: 1px solid #f44747 } /* Error */
-.highlight .g { color: #cccccc } /* Generic */
-.highlight .k { color: #569cd6 } /* Keyword */
-.highlight .l { color: #cccccc } /* Literal */
-.highlight .n { color: #cccccc } /* Name */
-.highlight .o { color: #d4d4d4 } /* Operator */
-.highlight .x { color: #cccccc } /* Other */
-.highlight .p { color: #cccccc } /* Punctuation */
-.highlight .cm { color: #608b4e } /* Comment.Multiline */
-.highlight .cp { color: #569cd6 } /* Comment.Preproc */
-.highlight .c1 { color: #608b4e } /* Comment.Single */
-.highlight .cs { color: #cd0000; font-weight: bold } /* Comment.Special */
-.highlight .gd { color: #cd0000 } /* Generic.Deleted */
-.highlight .ge { color: #cccccc; font-style: italic } /* Generic.Emph */
-.highlight .gr { color: #FF0000 } /* Generic.Error */
-.highlight .gh { color: #000080; font-weight: bold } /* Generic.Heading */
-.highlight .gi { color: #00cd00 } /* Generic.Inserted */
-.highlight .go { color: #808080 } /* Generic.Output */
-.highlight .gp { color: #000080; font-weight: bold } /* Generic.Prompt */
-.highlight .gs { color: #cccccc; font-weight: bold } /* Generic.Strong */
-.highlight .gu { color: #800080; font-weight: bold } /* Generic.Subheading */
-.highlight .gt { color: #0040D0 } /* Generic.Traceback */
-.highlight .kc { color: #569cd6 } /* Keyword.Constant */
-.highlight .kd { color: #00cd00 } /* Keyword.Declaration */
-.highlight .kn { color: #cd00cd } /* Keyword.Namespace */
-.highlight .kp { color: #569cd6 } /* Keyword.Pseudo */
-.highlight .kr { color: #569cd6 } /* Keyword.Reserved */
-.highlight .kt { color: #4EC9B0 } /* Keyword.Type */
-.highlight .ld { color: #cccccc } /* Literal.Date */
-.highlight .m { color: #b5cea8 } /* Literal.Number */
-.highlight .s { color: #ce9178 } /* Literal.String */
-.highlight .na { color: #cccccc } /* Name.Attribute */
-.highlight .nb { color: #b5cea8 } /* Name.Builtin */
-.highlight .nc { color: #00cdcd } /* Name.Class */
-.highlight .no { color: #cccccc } /* Name.Constant */
-.highlight .nd { color: #cccccc } /* Name.Decorator */
-.highlight .ni { color: #cccccc } /* Name.Entity */
-.highlight .ne { color: #666699; font-weight: bold } /* Name.Exception */
-.highlight .nf { color: #cccccc } /* Name.Function */
-.highlight .nl { color: #cccccc } /* Name.Label */
-.highlight .nn { color: #cccccc } /* Name.Namespace */
-.highlight .nx { color: #cccccc } /* Name.Other */
-.highlight .py { color: #cccccc } /* Name.Property */
-.highlight .nt { color: #cccccc } /* Name.Tag */
-.highlight .nv { color: #00cdcd } /* Name.Variable */
-.highlight .ow { color: #cdcd00 } /* Operator.Word */
-.highlight .w { color: #cccccc } /* Text.Whitespace */
-.highlight .mf { color: #b5cea8 } /* Literal.Number.Float */
-.highlight .mh { color: #b5cea8 } /* Literal.Number.Hex */
-.highlight .mi { color: #b5cea8 } /* Literal.Number.Integer */
-.highlight .mo { color: #b5cea8 } /* Literal.Number.Oct */
-.highlight .sb { color: #ce9178 } /* Literal.String.Backtick */
-.highlight .sc { color: #ce9178 } /* Literal.String.Char */
-.highlight .sd { color: #ce9178 } /* Literal.String.Doc */
-.highlight .s2 { color: #ce9178 } /* Literal.String.Double */
-.highlight .se { color: #ce9178 } /* Literal.String.Escape */
-.highlight .sh { color: #ce9178 } /* Literal.String.Heredoc */
-.highlight .si { color: #ce9178 } /* Literal.String.Interpol */
-.highlight .sx { color: #ce9178 } /* Literal.String.Other */
-.highlight .sr { color: #ce9178 } /* Literal.String.Regex */
-.highlight .s1 { color: #ce9178 } /* Literal.String.Single */
-.highlight .ss { color: #ce9178 } /* Literal.String.Symbol */
-.highlight .bp { color: #b5cea8 } /* Name.Builtin.Pseudo */
-.highlight .vc { color: #569cd6 } /* Name.Variable.Class */
-.highlight .vg { color: #00cdcd } /* Name.Variable.Global */
-.highlight .vi { color: #00cdcd } /* Name.Variable.Instance */
-.highlight .il { color: #b5cea8 } /* Literal.Number.Integer.Long */
+.highlight .chroma {
+    margin: 0;
+
+    .lntable td.lntd:last-child {
+        background-color: $faded-background-color;
+        padding-right: 12px;
+    }
+}
+
+@media (prefers-color-scheme: light) {
+    /* Background */ .highlight { background-color: #ffffff }
+    /* Other */ .highlight .x {  }
+    /* Error */ .highlight .err { color: #a61717; background-color: #e3d2d2 }
+    /* LineTableTD */ .highlight .lntd { vertical-align: top; padding: 0; margin: 0; border: 0; }
+    /* LineTable */ .highlight .lntable { border-spacing: 0; padding: 0; margin: 0; border: 0; width: auto; overflow: auto; display: block; }
+    /* LineHighlight */ .highlight .hl { display: block; width: 100%;background-color: #ffffcc }
+    /* LineNumbersTable */ .highlight .lnt { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #7f7f7f }
+    /* LineNumbers */ .highlight .ln { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #7f7f7f }
+    /* Keyword */ .highlight .k { color: #000000; font-weight: bold }
+    /* KeywordConstant */ .highlight .kc { color: #000000; font-weight: bold }
+    /* KeywordDeclaration */ .highlight .kd { color: #000000; font-weight: bold }
+    /* KeywordNamespace */ .highlight .kn { color: #000000; font-weight: bold }
+    /* KeywordPseudo */ .highlight .kp { color: #000000; font-weight: bold }
+    /* KeywordReserved */ .highlight .kr { color: #000000; font-weight: bold }
+    /* KeywordType */ .highlight .kt { color: #445588; font-weight: bold }
+    /* Name */ .highlight .n {  }
+    /* NameAttribute */ .highlight .na { color: #008080 }
+    /* NameBuiltin */ .highlight .nb { color: #0086b3 }
+    /* NameBuiltinPseudo */ .highlight .bp { color: #999999 }
+    /* NameClass */ .highlight .nc { color: #445588; font-weight: bold }
+    /* NameConstant */ .highlight .no { color: #008080 }
+    /* NameDecorator */ .highlight .nd { color: #3c5d5d; font-weight: bold }
+    /* NameEntity */ .highlight .ni { color: #800080 }
+    /* NameException */ .highlight .ne { color: #990000; font-weight: bold }
+    /* NameFunction */ .highlight .nf { color: #990000; font-weight: bold }
+    /* NameFunctionMagic */ .highlight .fm {  }
+    /* NameLabel */ .highlight .nl { color: #990000; font-weight: bold }
+    /* NameNamespace */ .highlight .nn { color: #555555 }
+    /* NameOther */ .highlight .nx {  }
+    /* NameProperty */ .highlight .py {  }
+    /* NameTag */ .highlight .nt { color: #000080 }
+    /* NameVariable */ .highlight .nv { color: #008080 }
+    /* NameVariableClass */ .highlight .vc { color: #008080 }
+    /* NameVariableGlobal */ .highlight .vg { color: #008080 }
+    /* NameVariableInstance */ .highlight .vi { color: #008080 }
+    /* NameVariableMagic */ .highlight .vm {  }
+    /* Literal */ .highlight .l {  }
+    /* LiteralDate */ .highlight .ld {  }
+    /* LiteralString */ .highlight .s { color: #dd1144 }
+    /* LiteralStringAffix */ .highlight .sa { color: #dd1144 }
+    /* LiteralStringBacktick */ .highlight .sb { color: #dd1144 }
+    /* LiteralStringChar */ .highlight .sc { color: #dd1144 }
+    /* LiteralStringDelimiter */ .highlight .dl { color: #dd1144 }
+    /* LiteralStringDoc */ .highlight .sd { color: #dd1144 }
+    /* LiteralStringDouble */ .highlight .s2 { color: #dd1144 }
+    /* LiteralStringEscape */ .highlight .se { color: #dd1144 }
+    /* LiteralStringHeredoc */ .highlight .sh { color: #dd1144 }
+    /* LiteralStringInterpol */ .highlight .si { color: #dd1144 }
+    /* LiteralStringOther */ .highlight .sx { color: #dd1144 }
+    /* LiteralStringRegex */ .highlight .sr { color: #009926 }
+    /* LiteralStringSingle */ .highlight .s1 { color: #dd1144 }
+    /* LiteralStringSymbol */ .highlight .ss { color: #990073 }
+    /* LiteralNumber */ .highlight .m { color: #009999 }
+    /* LiteralNumberBin */ .highlight .mb { color: #009999 }
+    /* LiteralNumberFloat */ .highlight .mf { color: #009999 }
+    /* LiteralNumberHex */ .highlight .mh { color: #009999 }
+    /* LiteralNumberInteger */ .highlight .mi { color: #009999 }
+    /* LiteralNumberIntegerLong */ .highlight .il { color: #009999 }
+    /* LiteralNumberOct */ .highlight .mo { color: #009999 }
+    /* Operator */ .highlight .o { color: #000000; font-weight: bold }
+    /* OperatorWord */ .highlight .ow { color: #000000; font-weight: bold }
+    /* Punctuation */ .highlight .p {  }
+    /* Comment */ .highlight .c { color: #999988; font-style: italic }
+    /* CommentHashbang */ .highlight .ch { color: #999988; font-style: italic }
+    /* CommentMultiline */ .highlight .cm { color: #999988; font-style: italic }
+    /* CommentSingle */ .highlight .c1 { color: #999988; font-style: italic }
+    /* CommentSpecial */ .highlight .cs { color: #999999; font-weight: bold; font-style: italic }
+    /* CommentPreproc */ .highlight .cp { color: #999999; font-weight: bold; font-style: italic }
+    /* CommentPreprocFile */ .highlight .cpf { color: #999999; font-weight: bold; font-style: italic }
+    /* Generic */ .highlight .g {  }
+    /* GenericDeleted */ .highlight .gd { color: #000000; background-color: #ffdddd }
+    /* GenericEmph */ .highlight .ge { color: #000000; font-style: italic }
+    /* GenericError */ .highlight .gr { color: #aa0000 }
+    /* GenericHeading */ .highlight .gh { color: #999999 }
+    /* GenericInserted */ .highlight .gi { color: #000000; background-color: #ddffdd }
+    /* GenericOutput */ .highlight .go { color: #888888 }
+    /* GenericPrompt */ .highlight .gp { color: #555555 }
+    /* GenericStrong */ .highlight .gs { font-weight: bold }
+    /* GenericSubheading */ .highlight .gu { color: #aaaaaa }
+    /* GenericTraceback */ .highlight .gt { color: #aa0000 }
+    /* GenericUnderline */ .highlight .gl { text-decoration: underline }
+    /* TextWhitespace */ .highlight .w { color: #bbbbbb }
+}
+
+@media (prefers-color-scheme: dark) {
+    /* Background */ .highlight { color: #e5e5e5; background-color: #000000 }
+    /* Other */ .highlight .x {  }
+    /* Error */ .highlight .err { color: #ff0000 }
+    /* LineTableTD */ .highlight .lntd { vertical-align: top; padding: 0; margin: 0; border: 0; }
+    /* LineTable */ .highlight .lntable { border-spacing: 0; padding: 0; margin: 0; border: 0; width: auto; overflow: auto; display: block; }
+    /* LineHighlight */ .highlight .hl { display: block; width: 100%;background-color: #ffffcc }
+    /* LineNumbersTable */ .highlight .lnt { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #727272 }
+    /* LineNumbers */ .highlight .ln { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #727272 }
+    /* Keyword */ .highlight .k { color: #ffffff; font-weight: bold }
+    /* KeywordConstant */ .highlight .kc { color: #ffffff; font-weight: bold }
+    /* KeywordDeclaration */ .highlight .kd { color: #ffffff; font-weight: bold }
+    /* KeywordNamespace */ .highlight .kn { color: #ffffff; font-weight: bold }
+    /* KeywordPseudo */ .highlight .kp { color: #ffffff; font-weight: bold }
+    /* KeywordReserved */ .highlight .kr { color: #ffffff; font-weight: bold }
+    /* KeywordType */ .highlight .kt { color: #ffffff; font-weight: bold }
+    /* Name */ .highlight .n {  }
+    /* NameAttribute */ .highlight .na { color: #007f7f }
+    /* NameBuiltin */ .highlight .nb { color: #ffffff; font-weight: bold }
+    /* NameBuiltinPseudo */ .highlight .bp {  }
+    /* NameClass */ .highlight .nc {  }
+    /* NameConstant */ .highlight .no {  }
+    /* NameDecorator */ .highlight .nd {  }
+    /* NameEntity */ .highlight .ni {  }
+    /* NameException */ .highlight .ne {  }
+    /* NameFunction */ .highlight .nf {  }
+    /* NameFunctionMagic */ .highlight .fm {  }
+    /* NameLabel */ .highlight .nl {  }
+    /* NameNamespace */ .highlight .nn {  }
+    /* NameOther */ .highlight .nx {  }
+    /* NameProperty */ .highlight .py {  }
+    /* NameTag */ .highlight .nt { font-weight: bold }
+    /* NameVariable */ .highlight .nv {  }
+    /* NameVariableClass */ .highlight .vc {  }
+    /* NameVariableGlobal */ .highlight .vg {  }
+    /* NameVariableInstance */ .highlight .vi {  }
+    /* NameVariableMagic */ .highlight .vm {  }
+    /* Literal */ .highlight .l {  }
+    /* LiteralDate */ .highlight .ld { color: #ffff00; font-weight: bold }
+    /* LiteralString */ .highlight .s { color: #00ffff; font-weight: bold }
+    /* LiteralStringAffix */ .highlight .sa { color: #00ffff; font-weight: bold }
+    /* LiteralStringBacktick */ .highlight .sb { color: #00ffff; font-weight: bold }
+    /* LiteralStringChar */ .highlight .sc { color: #00ffff; font-weight: bold }
+    /* LiteralStringDelimiter */ .highlight .dl { color: #00ffff; font-weight: bold }
+    /* LiteralStringDoc */ .highlight .sd { color: #00ffff; font-weight: bold }
+    /* LiteralStringDouble */ .highlight .s2 { color: #00ffff; font-weight: bold }
+    /* LiteralStringEscape */ .highlight .se { color: #00ffff; font-weight: bold }
+    /* LiteralStringHeredoc */ .highlight .sh { color: #00ffff; font-weight: bold }
+    /* LiteralStringInterpol */ .highlight .si { color: #00ffff; font-weight: bold }
+    /* LiteralStringOther */ .highlight .sx { color: #00ffff; font-weight: bold }
+    /* LiteralStringRegex */ .highlight .sr { color: #00ffff; font-weight: bold }
+    /* LiteralStringSingle */ .highlight .s1 { color: #00ffff; font-weight: bold }
+    /* LiteralStringSymbol */ .highlight .ss { color: #00ffff; font-weight: bold }
+    /* LiteralNumber */ .highlight .m { color: #ffff00; font-weight: bold }
+    /* LiteralNumberBin */ .highlight .mb { color: #ffff00; font-weight: bold }
+    /* LiteralNumberFloat */ .highlight .mf { color: #ffff00; font-weight: bold }
+    /* LiteralNumberHex */ .highlight .mh { color: #ffff00; font-weight: bold }
+    /* LiteralNumberInteger */ .highlight .mi { color: #ffff00; font-weight: bold }
+    /* LiteralNumberIntegerLong */ .highlight .il { color: #ffff00; font-weight: bold }
+    /* LiteralNumberOct */ .highlight .mo { color: #ffff00; font-weight: bold }
+    /* Operator */ .highlight .o {  }
+    /* OperatorWord */ .highlight .ow {  }
+    /* Punctuation */ .highlight .p {  }
+    /* Comment */ .highlight .c { color: #007f7f }
+    /* CommentHashbang */ .highlight .ch { color: #007f7f }
+    /* CommentMultiline */ .highlight .cm { color: #007f7f }
+    /* CommentSingle */ .highlight .c1 { color: #007f7f }
+    /* CommentSpecial */ .highlight .cs { color: #007f7f }
+    /* CommentPreproc */ .highlight .cp { color: #00ff00; font-weight: bold }
+    /* CommentPreprocFile */ .highlight .cpf { color: #00ff00; font-weight: bold }
+    /* Generic */ .highlight .g {  }
+    /* GenericDeleted */ .highlight .gd {  }
+    /* GenericEmph */ .highlight .ge {  }
+    /* GenericError */ .highlight .gr {  }
+    /* GenericHeading */ .highlight .gh { font-weight: bold }
+    /* GenericInserted */ .highlight .gi {  }
+    /* GenericOutput */ .highlight .go {  }
+    /* GenericPrompt */ .highlight .gp {  }
+    /* GenericStrong */ .highlight .gs { font-weight: bold }
+    /* GenericSubheading */ .highlight .gu { font-weight: bold }
+    /* GenericTraceback */ .highlight .gt {  }
+    /* GenericUnderline */ .highlight .gl { text-decoration: underline }
+    /* TextWhitespace */ .highlight .w {  }
+}
diff --git a/assets/sass/main.scss b/assets/sass/main.scss
index 6ea5363..ba153d1 100644
--- a/assets/sass/main.scss
+++ b/assets/sass/main.scss
@@ -1,6 +1,5 @@
 @import "agda";
 @import "mixins";
-@import "syntax";
 @import "fonts";
 
 $sansfont: "Poppins", "Helvetica", "Arial", "Liberation Sans", sans-serif;
@@ -19,6 +18,7 @@ $monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline",
     $link-color: royalblue;
     $code-color: firebrick;
     $tag-color: lighten($link-color, 35%);
+    @import "syntax";
     @import "content";
 }
 
@@ -33,5 +33,6 @@ $monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline",
     $link-color: lightskyblue;
     $code-color: lighten(firebrick, 25%);
     $tag-color: darken($link-color, 55%);
+    @import "syntax";
     @import "content";
 }
diff --git a/config.toml b/config.toml
index 2db8a33..7119f22 100644
--- a/config.toml
+++ b/config.toml
@@ -14,3 +14,17 @@ startLevel = 2
 
 [markup.goldmark.renderer]
 unsafe = true
+
+[markup.highlight]
+anchorLineNos = true
+codeFences = true
+guessSyntax = false
+hl_Lines = ''
+lineAnchors = ''
+lineNoStart = 1
+lineNos = true
+lineNumbersInTable = true
+noClasses = false
+style = 'monokai'
+tabWidth = 4
+
diff --git a/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md b/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md
index 5030d05..c181339 100644
--- a/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md
+++ b/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md
@@ -30,11 +30,11 @@ My lambda calculus implemented `call/cc` on top of a CEK machine.
   output. If this were a library function I'd like to tell people who write code
   that uses this function "don't give me an empty list!"
 
-  Unfortunately, just writing this in documentation isn't enough. What we'd
-  really like is for a tool (like a compiler) to tell any developer who is
-  trying to pass an empty list into our maximum function "You can't do that."
-  Unfortunately, most of the popular languages being used today have no way of
-  describing "a list that's not empty."
+  But just writing this in documentation isn't enough. What we'd really like is
+  for a tool (like a compiler) to tell any developer who is trying to pass an
+  empty list into our maximum function "You can't do that." Unfortunately, most
+  of the popular languages being used today have no way of describing "a list
+  that's not empty."
 
   We still have a way to prevent people from running into this problem, though
   it involves pushing the problem to runtime rather than compile time. The