From 9f50966339d1d3bbe50305ba50cf3e293d3ed7a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 20 Jun 2022 18:39:55 +0200
Subject: [PATCH] feat: initial LeanInk HTML generation

---
 DocGen4/LeanInk/Output.lean         | 158 +++++-
 DocGen4/Output.lean                 |  32 +-
 DocGen4/Output/Base.lean            |   4 +
 DocGen4/Output/ToHtmlFormat.lean    |  34 +-
 static/alectryon/alectryon.css      | 777 ++++++++++++++++++++++++++++
 static/alectryon/alectryon.js       | 172 ++++++
 static/alectryon/docutils_basic.css | 593 +++++++++++++++++++++
 7 files changed, 1729 insertions(+), 41 deletions(-)
 create mode 100644 static/alectryon/alectryon.css
 create mode 100644 static/alectryon/alectryon.js
 create mode 100644 static/alectryon/docutils_basic.css

diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean
index 41986d9..91db9b6 100644
--- a/DocGen4/LeanInk/Output.lean
+++ b/DocGen4/LeanInk/Output.lean
@@ -14,27 +14,151 @@ namespace LeanInk.Annotation.Alectryon
 open DocGen4 Output
 open scoped DocGen4.Jsx
 
-def TypeInfo.toHtml : TypeInfo → HtmlM Html := sorry
+structure AlectryonContext where
+  counter : Nat
 
-def Token.toHtml : Token → HtmlM Html := sorry
+abbrev AlectryonM := StateT AlectryonContext HtmlM
 
-def Contents.toHtml : Contents → HtmlM Html
-  | .string value => sorry
-  | .experimentalTokens value => sorry
+def getNextButtonLabel : AlectryonM String := do
+  let val ← get
+  let newCounter := val.counter + 1
+  set { val with counter := newCounter }
+  pure s!"plain-lean4-lean-chk{val.counter}"
 
-def Hypothesis.toHtml : Hypothesis → HtmlM Html := sorry
+def TypeInfo.toHtml : TypeInfo → AlectryonM Html := sorry
 
-def Goal.toHtml : Goal → HtmlM Html := sorry
+def Token.toHtml (t : Token) : AlectryonM Html := do
+  -- TODO: Show rest of token
+  pure $ Html.text t.raw
 
-def Message.toHtml : Message → HtmlM Html := sorry
+def Contents.toHtml : Contents → AlectryonM (Array Html)
+  | .string value => pure #[Html.text value]
+  | .experimentalTokens values => values.mapM Token.toHtml
 
-def Sentence.toHtml : Sentence → HtmlM Html := sorry
+def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
+  let mut hypParts := #[<var>[h.names.intersperse ", " |>.map Html.text |>.toArray]<//var>]
+  if h.body != "" then
+    hypParts := hypParts.push
+      <span class="hyp-body">
+        <b>:= <//b>
+        <span>{h.body}<//span>
+      <//span>
+  hypParts := hypParts.push
+      <span class="hyp-type">
+        <b>: <//b>
+        <span >{h.type}<//span>
+      <//span>
 
-def Text.toHtml : Text → HtmlM Html := sorry
+  pure
+    <span>
+      [hypParts]
+    <//span>
 
-def Fragment.toHtml : Fragment → HtmlM Html
-  | .text value => sorry
-  | .sentence value => sorry
+def Goal.toHtml (g : Goal) : AlectryonM Html := do
+  let mut hypotheses := #[]
+  for hyp in g.hypotheses do
+    let rendered ← hyp.toHtml
+    hypotheses := hypotheses.push rendered
+    hypotheses := hypotheses.push <br/>
+  pure
+    <blockquote class="alectryon-goal">
+      <div class="goal-hyps">
+        [hypotheses]
+      <//div>
+      <span class="goal-separator">
+        <hr><span class="goal-name">{g.name}<//span><//hr>
+      <//span>
+      <div class="goal-conclusion">
+        {g.conclusion}
+      <//div>
+    <//blockquote>
+
+def Message.toHtml (m : Message) : AlectryonM Html := do
+  pure
+    <blockquote class="alectryon-message">
+      -- TODO: This might have to be done in a fancier way
+      {m.contents}
+    <//blockquote>
+
+def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
+  let messages :=
+    if s.messages.size > 0 then
+      #[
+        <div class="alectryon-messages">
+          [←s.messages.mapM Message.toHtml]
+        <//div>
+      ]
+    else
+      #[]
+  
+  let goals :=
+    if s.goals.size > 0 then
+      -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
+      #[
+        <div class="alectryon-goals">
+          [←s.goals.mapM Goal.toHtml]
+        <//div>
+      ]
+    else
+      #[]
+
+  let buttonLabel ← getNextButtonLabel
+
+  pure
+    <span class="alectryon-sentence">
+      <input class="alectryon-toggle" id={buttonLabel} style="display: none" type="checkbox"/>
+      <label class="alectryon-input" for={buttonLabel}>
+        [←s.contents.toHtml]
+      <//label>
+      <small class="alectryon-output">
+        [messages]
+        [goals]
+      <//small>
+    <//span>
+
+def Text.toHtml (t : Text) : AlectryonM Html := do
+  pure
+    <span class="alectryon-wsp">
+      [←t.contents.toHtml]
+    <//span>
+
+def Fragment.toHtml : Fragment → AlectryonM Html
+  | .text value => value.toHtml
+  | .sentence value => value.toHtml
+
+def baseHtml (content : Array Html) : AlectryonM Html := do
+  let banner :=
+    <div «class»="alectryon-banner">
+      Built with <a href="https://github.com/leanprover/doc-gen4">doc-gen4<//a>, running Lean4.
+      Bubbles (<span class="alectryon-bubble"><//span>) indicate interactive fragments: hover for details, tap to reveal contents.
+      Use <kbd>Ctrl+↑<//kbd> <kbd>Ctrl+↓<//kbd> to navigate, <kbd>Ctrl+🖱️<//kbd> to focus.
+      On Mac, use <kbd>Cmd<//kbd> instead of <kbd>Ctrl<//kbd>.
+    </div>
+
+  pure
+    <html lang="en" class="alectryon-standalone">
+      <head>
+        <meta charset="UTF-8"/>
+        <meta name="viewport" content="width=device-width, initial-scale=1"/>
+
+        <link rel="stylesheet" href={s!"{←getRoot}src/alectryon.css"}/>
+        <link rel="stylesheet" href={s!"{←getRoot}src/docutils_basic.css"}/>
+        <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
+
+        <script defer="true" src={s!"{←getRoot}src/alectryon.js"}></script>
+      </head>
+      <body>
+        <article class="alectryon-root alectryon-centered">
+          {banner}
+          <pre class="alectryon-io highlight">
+            [content]
+          </pre>
+        </article>
+      </body>
+    </html>
+
+def renderFragments (fs : Array Fragment) : AlectryonM Html :=
+  fs.mapM Fragment.toHtml >>= baseHtml
 
 end LeanInk.Annotation.Alectryon
 
@@ -46,9 +170,13 @@ open scoped DocGen4.Jsx
 
 def moduleToHtml (module : Process.Module) (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : HtmlT IO Html := withReader (setCurrentName module.name) do
   let json ← runInk inkPath sourceFilePath
-  let fragments : Except String (Array Fragment) := fromJson? json
+  let fragments := fromJson? json
   match fragments with
-  | .ok fragments => pure $ <div>hello</div>
+  | .ok fragments =>
+    let render := StateT.run (LeanInk.Annotation.Alectryon.renderFragments fragments) { counter := 0 }
+    let ctx ← read
+    let (html, _) := ReaderT.run render ctx
+    pure html
   | .error err => throw $ IO.userError s!"Error while parsing LeanInk Output: {err}"
 
 end DocGen4.Output.LeanInk
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 3947a7d..5c11ebc 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -59,14 +59,6 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
       declList := declList.push obj
       let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config 
       FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml
-    if let some inkPath := inkPath then
-      if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" mod.name then
-        IO.println s!"Inking: {mod.name.toString}"
-        let srcHtml ← ReaderT.run (LeanInk.moduleToHtml mod inkPath inputPath) config
-        let srcDir := moduleNameToDirectory srcBasePath mod.name
-        let srcPath := moduleNameToFile srcBasePath mod.name
-        FS.createDirAll srcDir
-        FS.writeFile srcPath srcHtml.toString
   let json := Json.arr declList
 
   FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config 
@@ -87,16 +79,30 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
   FS.writeFile (basePath / "how-about.js") howAboutJs
   FS.writeFile (basePath / "search.js") searchJs
   FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs
+  FS.writeFile (srcBasePath / "alectryon.css") alectryonCss
+  FS.writeFile (srcBasePath / "alectryon.js") alectryonJs
+  FS.writeFile (srcBasePath / "docutils_basic.css") docUtilsCss
 
-  for (module, content) in result.moduleInfo.toArray do
-    let fileDir := moduleNameToDirectory basePath module
-    let filePath := moduleNameToFile basePath module
+  for (modName, module) in result.moduleInfo.toArray do
+    let fileDir := moduleNameToDirectory basePath modName
+    let filePath := moduleNameToFile basePath modName
     -- path: 'basePath/module/components/till/last.html'
     -- The last component is the file name, so we drop it from the depth to root.
-    let config := { config with depthToRoot := module.components.dropLast.length }
-    let moduleHtml := ReaderT.run (moduleToHtml content) config
+    let config := { config with depthToRoot := modName.components.dropLast.length }
+    let moduleHtml := ReaderT.run (moduleToHtml module) config
     FS.createDirAll $ fileDir
     FS.writeFile filePath moduleHtml.toString
+    if let some inkPath := inkPath then
+      if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
+        IO.println s!"Inking: {modName.toString}"
+        -- path: 'basePath/src/module/components/till/last.html'
+        -- The last component is the file name, however we are in src/ here so dont drop it this time
+        let config := { config with depthToRoot := modName.components.length }
+        let srcHtml ← ReaderT.run (LeanInk.moduleToHtml module inkPath inputPath) config
+        let srcDir := moduleNameToDirectory srcBasePath modName
+        let srcPath := moduleNameToFile srcBasePath modName
+        FS.createDirAll srcDir
+        FS.writeFile srcPath srcHtml.toString
 
 end DocGen4
 
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 9d7aa10..63b1af1 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -111,6 +111,10 @@ are used in documentation generation, notably JS and CSS ones.
   def searchJs : String := include_str "../../static/search.js"
   def findJs : String := include_str "../../static/find/find.js"
   def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
+  
+  def alectryonCss : String := include_str "../../static/alectryon/alectryon.css"
+  def alectryonJs : String := include_str "../../static/alectryon/alectryon.js"
+  def docUtilsCss : String  := include_str "../../static/alectryon/docutils_basic.css"
 end Static
 
 /--
diff --git a/DocGen4/Output/ToHtmlFormat.lean b/DocGen4/Output/ToHtmlFormat.lean
index bd6f875..6120511 100644
--- a/DocGen4/Output/ToHtmlFormat.lean
+++ b/DocGen4/Output/ToHtmlFormat.lean
@@ -89,6 +89,7 @@ syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
 
 syntax "<" rawIdent jsxAttr* "/>" : jsxElement
 syntax "<" rawIdent jsxAttr* ">" jsxChild* "</" rawIdent ">" : jsxElement
+syntax "<" rawIdent jsxAttr* ">" jsxChild* "<//" rawIdent ">" : jsxElement
 
 syntax jsxText      : jsxChild
 syntax "{" term "}" : jsxChild
@@ -115,23 +116,30 @@ def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
     | _ => Macro.throwUnsupported
   return as
 
+private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × Syntax):= do
+  unless n.getId == m.getId do
+    withRef m <| Macro.throwError s!"Leading and trailing part of tags don't match: '{n}', '{m}'"
+  let mut cs ← `(#[])
+  for child in children do
+    cs ← match child with
+    | `(jsxChild|$t:jsxText)    => `(($cs).push (Html.text $(quote t[0].getAtomVal!)))
+    -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
+    | `(jsxChild|{$t})          => `(($cs).push ($t : Html))
+    | `(jsxChild|[$t])          => `($cs ++ ($t : Array Html))
+    | `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html))
+    | _                         => Macro.throwUnsupported
+  let tag := toString n.getId
+  pure $ (tag, cs)
+
 macro_rules
   | `(<$n $attrs* />) => do
     `(Html.element $(quote (toString n.getId)) true $(← translateAttrs attrs) #[])
   | `(<$n $attrs* >$children*</$m>) => do
-    unless n.getId == m.getId do
-      withRef m <| Macro.throwError s!"expected </{n.getId}>"
-    let mut cs ← `(#[])
-    for child in children do
-      cs ← match child with
-      | `(jsxChild|$t:jsxText)    => `(($cs).push (Html.text $(quote t[0].getAtomVal!)))
-      -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
-      | `(jsxChild|{$t})          => `(($cs).push ($t : Html))
-      | `(jsxChild|[$t])          => `($cs ++ ($t : Array Html))
-      | `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html))
-      | _                         => Macro.throwUnsupported
-    let tag := toString n.getId
-    `(Html.element $(quote tag) false $(← translateAttrs attrs) $cs)
+    let (tag, children) ← htmlHelper n children m
+    `(Html.element $(quote tag) false $(← translateAttrs attrs) $children)
+  | `(<$n $attrs* >$children*<//$m>) => do
+    let (tag, children) ← htmlHelper n children m
+    `(Html.element $(quote tag) true $(← translateAttrs attrs) $children)
 
 end Jsx
 
diff --git a/static/alectryon/alectryon.css b/static/alectryon/alectryon.css
new file mode 100644
index 0000000..67988e3
--- /dev/null
+++ b/static/alectryon/alectryon.css
@@ -0,0 +1,777 @@
+@charset "UTF-8";
+/*
+Copyright © 2019 Clément Pit-Claudel
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+*/
+
+/*******************************/
+/* CSS reset for .alectryon-io */
+/*******************************/
+
+.alectryon-io blockquote {
+    line-height: inherit;
+}
+
+.alectryon-io blockquote:after {
+    display: none;
+}
+
+.alectryon-io label {
+    display: inline;
+    font-size: inherit;
+    margin: 0;
+}
+
+.alectryon-io a {
+    text-decoration: none !important;
+    font-style: oblique !important;
+    color: unset;
+}
+
+/* Undo <small> and <blockquote>, added to improve RSS rendering. */
+
+.alectryon-io small.alectryon-output,
+.alectryon-io small.alectryon-type-info {
+    font-size: inherit;
+}
+
+.alectryon-io blockquote.alectryon-goal,
+.alectryon-io blockquote.alectryon-message {
+    font-weight: normal;
+    font-size: inherit;
+}
+
+/***************/
+/* Main styles */
+/***************/
+
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .comment,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-mref,
+.alectryon-block, .alectryon-io,
+.alectryon-toggle-label, .alectryon-banner {
+    font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important;
+    font-size: 0.875em;
+    font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
+    line-height: initial;
+}
+
+.alectryon-io, .alectryon-block, .alectryon-toggle-label, .alectryon-banner {
+    overflow: visible;
+    overflow-wrap: break-word;
+    position: relative;
+    white-space: pre-wrap;
+}
+
+/*
+CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply
+respects the user's `bidi-display-reordering` setting), so don't turn it off
+here either.  But beware unexpected results like `Definition test_אב := 0.`
+
+.alectryon-io span {
+    direction: ltr;
+    unicode-bidi: bidi-override;
+}
+
+In any case, make an exception for comments:
+
+.highlight .c {
+    direction: embed;
+    unicode-bidi: initial;
+}
+*/
+
+.alectryon-mref,
+.alectryon-mref-marker {
+    align-self: center;
+    box-sizing: border-box;
+    display: inline-block;
+    font-size: 80%;
+    font-weight: bold;
+    line-height: 1;
+    box-shadow: 0 0 0 1pt black;
+    padding: 1pt 0.3em;
+    text-decoration: none;
+}
+
+.alectryon-block .alectryon-mref-marker,
+.alectryon-io .alectryon-mref-marker {
+    user-select: none;
+    margin: -0.25em 0 -0.25em 0.5em;
+}
+
+.alectryon-inline .alectryon-mref-marker {
+    margin: -0.25em 0.15em -0.25em 0.625em; /* 625 = 0.5em / 80% */
+}
+
+.alectryon-mref {
+    color: inherit;
+    margin: -0.5em 0.25em;
+}
+
+.alectryon-goal:target .goal-separator .alectryon-mref-marker,
+:target > .alectryon-mref-marker {
+    animation: blink 0.2s step-start 0s 3 normal none;
+    background-color: #fcaf3e;
+    position: relative;
+}
+
+@keyframes blink {
+    50% {
+        box-shadow: 0 0 0 3pt #fcaf3e, 0 0 0 4pt black;
+        z-index: 10;
+    }
+}
+
+.alectryon-toggle,
+.alectryon-io .alectryon-extra-goal-toggle {
+    display: none;
+}
+
+.alectryon-bubble,
+.alectryon-io label,
+.alectryon-toggle-label {
+    cursor: pointer;
+}
+
+.alectryon-toggle-label {
+    display: block;
+    font-size: 0.8em;
+}
+
+.alectryon-io .alectryon-input {
+    padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */
+}
+
+.alectryon-io .alectryon-token {
+    white-space: pre-wrap;
+    display: inline;
+}
+
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-input {
+    /* FIXME if keywords were ‘bolder’ we wouldn't need !important */
+    font-weight: bold !important; /* Use !important to avoid a * selector */
+}
+
+.alectryon-bubble:before,
+.alectryon-toggle-label:before,
+.alectryon-io label.alectryon-input:after,
+.alectryon-io .alectryon-goal > label:before {
+    border: 1px solid #babdb6;
+    border-radius: 1em;
+    box-sizing: border-box;
+    content: '';
+    display: inline-block;
+    font-weight: bold;
+    height: 0.25em;
+    margin-bottom: 0.15em;
+    vertical-align: middle;
+    width: 0.75em;
+}
+
+.alectryon-toggle-label:before,
+.alectryon-io .alectryon-goal > label:before {
+    margin-right: 0.25em;
+}
+
+.alectryon-io .alectryon-goal > label:before {
+    margin-top: 0.125em;
+}
+
+.alectryon-io label.alectryon-input {
+    padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
+}
+
+.alectryon-io label.alectryon-input:after {
+    margin-left: 0.25em;
+    margin-right: -1em; /* Compensate for the anti-wrapping space */
+}
+
+.alectryon-failed {
+    /* Underlines are broken in Chrome (they reset at each element boundary)… */
+    /* text-decoration: red wavy underline; */
+    /* … but it isn't too noticeable with dots */
+    text-decoration: red dotted underline;
+    text-decoration-skip-ink: none;
+    /* Chrome prints background images in low resolution, yielding a blurry underline */
+    /* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
+}
+
+/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
+   doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to
+   hide its output causes it to remain visible (its :hover state gets triggered.
+   We only do it for the default style though, since other styles don't put the
+   output over the main text, so showing too much is not an issue. */
+@media (any-hover: hover) {
+    .alectryon-bubble:hover:before,
+    .alectryon-toggle-label:hover:before,
+    .alectryon-io label.alectryon-input:hover:after {
+        background: #eeeeec;
+    }
+
+    .alectryon-io label.alectryon-input:hover {
+        text-decoration: underline dotted #babdb6;
+	    text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */
+    }
+
+    .alectryon-io .alectryon-sentence:hover .alectryon-output,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {
+        z-index: 2; /* Place hovered goals above .alectryon-sentence.alectryon-target ones */
+    }
+}
+
+.alectryon-toggle:checked + .alectryon-toggle-label:before,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked + label.alectryon-input:after,
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal > label:before {
+    background-color: #babdb6;
+    border-color: #babdb6;
+}
+
+/* Disable clicks on sentences when the document-wide toggle is set. */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input {
+    cursor: unset;
+    pointer-events: none;
+}
+
+/* Hide individual checkboxes when the document-wide toggle is set. */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input:after {
+    display: none;
+}
+
+/* .alectryon-output is displayed by toggles, :hover, and .alectryon-target rules */
+.alectryon-io .alectryon-output {
+    box-sizing: border-box;
+    display: none;
+    left: 0;
+    right: 0;
+    position: absolute;
+    padding: 0.25em 0;
+    overflow: visible; /* Let box-shadows overflow */
+    z-index: 1; /* Default to an index lower than that used by :hover */
+}
+
+.alectryon-io .alectryon-type-info-wrapper {
+    position: absolute;
+    display: inline-block;
+    width: 100%;
+}
+
+.alectryon-io .alectryon-type-info-wrapper.full-width {
+    left: 0;
+    min-width: 100%;
+    max-width: 100%;
+}
+
+.alectryon-io .alectryon-type-info .goal-separator {
+    height: unset;
+    margin-top: 0em;
+}
+
+.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info {
+    box-sizing: border-box;
+    bottom: 100%;
+    position: absolute;
+    /*padding: 0.25em 0;*/
+    visibility: hidden;
+    overflow: visible; /* Let box-shadows overflow */
+    z-index: 1; /* Default to an index lower than that used by :hover */
+    white-space: pre-wrap !important;
+}
+
+.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info .alectryon-goal.alectryon-docstring {
+    white-space: pre-wrap !important;
+}
+
+@media (any-hover: hover) { /* See note above about this @media query */
+    .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) {
+        display: block;
+    }
+
+    .alectryon-io.output-hidden .alectryon-sentence:hover .alectryon-output:not(:hover) {
+        display: none !important;
+    }
+
+    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
+    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+        /*visibility: hidden !important;*/
+    }
+
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+        visibility: visible;
+        transition-delay: 0.5s;
+    }
+}
+
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output {
+    display: block;
+}
+
+/* Indicate active (hovered or targeted) goals with a shadow. */
+.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
+.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals,
+.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+    box-shadow: 2px 2px 2px gray;
+}
+
+.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-hyps {
+    display: none;
+}
+
+.alectryon-io .alectryon-extra-goals .alectryon-extra-goal-toggle:not(:checked) + .alectryon-goal label.goal-separator hr {
+    /* Dashes indicate that the hypotheses are hidden */
+    border-top-style: dashed;
+}
+
+
+/* Show just a small preview of the other goals; this is undone by the
+   "extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */
+.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-conclusion {
+    max-height: 5.2em;
+    overflow-y: auto;
+    /* Combining ‘overflow-y: auto’ with ‘display: inline-block’ causes extra space
+       to be added below the box. ‘vertical-align: middle’ gets rid of it. */
+    vertical-align: middle;
+}
+
+.alectryon-io .alectryon-goals,
+.alectryon-io .alectryon-messages {
+    background: #f6f7f6;
+	/*border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
+    display: block;
+    padding: 0.25em;
+}
+
+.alectryon-message::before {
+    content: '';
+    float: right;
+    /* etc/svg/square-bubble-xl.svg */
+    background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat;
+    height: 14px;
+    width: 14px;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container {
+    width: unset;
+}
+
+/* Show goals when a toggle is set */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output {
+    display: block;
+    position: static;
+    width: unset;
+    background: unset; /* Override the backgrounds set in floating in windowed mode */
+    padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
+}
+
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output .goal-hyps {
+    /* Overridden back in windowed style */
+    flex-flow: row wrap;
+    justify-content: flex-start;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
+    display: block;
+}
+
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-hyps {
+    display: flex;
+}
+
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion {
+    max-height: unset;
+    overflow-y: unset;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence > .alectryon-toggle ~ .alectryon-wsp,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-wsp {
+    display: none;
+}
+
+.alectryon-io .alectryon-messages,
+.alectryon-io .alectryon-message,
+.alectryon-io .alectryon-goals,
+.alectryon-io .alectryon-goal,
+.alectryon-io .goal-hyps > span,
+.alectryon-io .goal-conclusion {
+    border-radius: 0.15em;
+}
+
+.alectryon-io .alectryon-goal,
+.alectryon-io .alectryon-message {
+    align-items: center;
+    background: #f6f7f6;
+    border: 0em;
+    display: block;
+    flex-direction: column;
+    margin: 0.25em;
+    padding: 0.5em;
+    position: relative;
+}
+
+.alectryon-io .goal-hyps {
+    align-content: space-around;
+    align-items: baseline;
+    display: flex;
+    flex-flow: column nowrap; /* re-stated in windowed mode */
+    justify-content: space-around;
+    /* LATER use a ‘gap’ property instead of margins once supported */
+    margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
+    padding-bottom: 0.35em; /* 0.5em-0.15em to cancel the 0.5em of .goal-separator */
+}
+
+.alectryon-io .goal-hyps > br {
+    display: none; /* Only for RSS readers */
+}
+
+.alectryon-io .goal-hyps > span,
+.alectryon-io .goal-conclusion {
+    /*background: #eeeeec;*/
+    display: inline-block;
+    padding: 0.15em 0.35em;
+}
+
+.alectryon-io .goal-hyps > span {
+    align-items: baseline;
+    display: inline-flex;
+    margin: 0.15em 0.25em;
+}
+
+.alectryon-block var,
+.alectryon-inline var,
+.alectryon-io .goal-hyps > span > var {
+    font-weight: 600;
+    font-style: unset;
+}
+
+.alectryon-io .goal-hyps > span > var {
+    /* Shrink the list of names, but let it grow as long as space is available. */
+    flex-basis: min-content;
+    flex-grow: 1;
+}
+
+.alectryon-io .goal-hyps > span b {
+    font-weight: 600;
+    margin: 0 0 0 0.5em;
+    white-space: pre;
+}
+
+.alectryon-io .hyp-body,
+.alectryon-io .hyp-type {
+    display: flex;
+    align-items: baseline;
+}
+
+.alectryon-io .goal-separator {
+    align-items: center;
+    display: flex;
+    flex-direction: row;
+    height: 1em; /* Fixed height to ignore goal name and markers */
+    margin-top: -0.5em; /* Compensated in .goal-hyps when shown */
+}
+
+.alectryon-io .goal-separator hr {
+    border: none;
+    border-top: thin solid #555753;
+    display: block;
+    flex-grow: 1;
+    margin: 0;
+}
+
+.alectryon-io .goal-separator .goal-name {
+    font-size: 0.75em;
+    margin-left: 0.5em;
+}
+
+/**********/
+/* Banner */
+/**********/
+
+.alectryon-banner {
+    background: #eeeeec;
+    border: 1px solid #babcbd;
+    font-size: 0.75em;
+    padding: 0.25em;
+    text-align: center;
+    margin: 1em 0;
+}
+
+.alectryon-banner a {
+    cursor: pointer;
+    text-decoration: underline;
+}
+
+.alectryon-banner kbd {
+    background: #d3d7cf;
+    border-radius: 0.15em;
+    border: 1px solid #babdb6;
+    box-sizing: border-box;
+    display: inline-block;
+    font-family: inherit;
+    font-size: 0.9em;
+    height: 1.3em;
+    line-height: 1.2em;
+    margin: -0.25em 0;
+    padding: 0 0.25em;
+    vertical-align: middle;
+}
+
+/**********/
+/* Toggle */
+/**********/
+
+.alectryon-toggle-label {
+    margin: 1rem 0;
+}
+
+/******************/
+/* Floating style */
+/******************/
+
+/* If there's space, display goals to the right of the code, not below it. */
+@media (min-width: 80rem) {
+    /* Unlike the windowed case, we don't want to move output blocks to the side
+       when they are both :checked and -targeted, since it gets confusing as
+       things jump around; hence the commented-output part of the selector,
+       which would otherwise increase specificity */
+    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output,
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
+        top: 0;
+        left: 100%;
+        right: -100%;
+        padding: 0 0.5em;
+        position:  absolute;
+    }
+
+    .alectryon-floating .alectryon-output {
+        min-height: 100%;
+    }
+
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
+        background: white; /* Ensure that short goals hide long ones */
+    }
+
+    /* This odd margin-bottom property prevents the sticky div from bumping
+       against the bottom of its container (.alectryon-output).  The alternative
+       would be enlarging .alectryon-output, but that would cause overflows,
+       enlarging scrollbars and yielding scrolling towards the bottom of the
+       page.  Doing things this way instead makes it possible to restrict
+       .alectryon-output to a reasonable size (100%, through top = bottom = 0).
+       See also https://stackoverflow.com/questions/43909940/. */
+    /* See note on specificity above */
+    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output > div,
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output > div {
+        margin-bottom: -200%;
+        position: sticky;
+        top: 0;
+    }
+
+    .alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
+    .alectryon-floating .alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
+        margin-bottom: unset; /* Undo the margin */
+    }
+
+    /* Float underneath the current fragment
+    @media (max-width: 80rem) {
+        .alectryon-floating .alectryon-output {
+            top: 100%;
+        }
+    } */
+}
+
+/********************/
+/* Multi-pane style */
+/********************/
+
+.alectryon-windowed {
+    border: 0 solid #2e3436;
+    box-sizing: border-box;
+}
+
+.alectryon-windowed .alectryon-sentence:hover .alectryon-output {
+    background: white; /* Ensure that short goals hide long ones */
+}
+
+.alectryon-windowed .alectryon-output {
+    position: fixed; /* Overwritten by the ‘:checked’ rules */
+}
+
+/* See note about specificity below */
+.alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
+    padding: 0.5em;
+    overflow-y: auto; /* Windowed contents may need to scroll */
+}
+
+.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
+.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals {
+    box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */
+}
+
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .goal-hyps {
+    /* Restated to override the :checked style */
+    flex-flow: column nowrap;
+    justify-content: space-around;
+}
+
+
+.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-extra-goals .alectryon-goal .goal-conclusion
+/* Like .alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion */ {
+    max-height: unset;
+    overflow-y: unset;
+}
+
+.alectryon-windowed .alectryon-output > div {
+    display: flex; /* Put messages after goals */
+    flex-direction: column-reverse;
+}
+
+/*********************/
+/* Standalone styles */
+/*********************/
+
+.alectryon-standalone {
+    font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
+    line-height: 1.5;
+}
+
+@media screen and (min-width: 50rem) {
+    html.alectryon-standalone {
+        /* Prevent flickering when hovering a block causes scrollbars to appear. */
+        margin-left: calc(100vw - 100%);
+        margin-right: 0;
+    }
+}
+
+/* Coqdoc */
+
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-coqdoc .doc .comment {
+    display: inline;
+}
+
+.alectryon-coqdoc .doc .comment {
+    color: #eeeeec;
+}
+
+.alectryon-coqdoc .doc .paragraph {
+    height: 0.75em;
+}
+
+/* Centered, Floating */
+
+.alectryon-standalone .alectryon-centered,
+.alectryon-standalone .alectryon-floating {
+    max-width: 50rem;
+    margin: auto;
+}
+
+@media (min-width: 80rem) {
+    .alectryon-standalone .alectryon-floating {
+        max-width: 80rem;
+    }
+
+    .alectryon-standalone .alectryon-floating > * {
+        width: 50%;
+        margin-left: 0;
+    }
+}
+
+/* Windowed */
+
+.alectryon-standalone .alectryon-windowed {
+    display: block;
+    margin: 0;
+    overflow-y: auto;
+    position: absolute;
+    padding: 0 1em;
+}
+
+.alectryon-standalone .alectryon-windowed > * {
+    /* Override properties of docutils_basic.css */
+    margin-left: 0;
+    max-width: unset;
+}
+
+.alectryon-standalone .alectryon-windowed .alectryon-io {
+    box-sizing: border-box;
+    width: 100%;
+}
+
+/* No need to predicate the ‘:hover’ rules below on ‘:not(:checked)’, since ‘left’,
+   ‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting
+   ‘position’ to ‘static’ */
+
+
+/* Specificity: We want the output to stay inline when hovered while unfolded
+   (:checked), but we want it to move when it's targeted (i.e. when the user
+   is browsing goals one by one using the keyboard, in which case we want to
+   goals to appear in consistent locations).  The selectors below ensure
+   that :hover < :checked < -targeted in terms of specificity. */
+/* LATER: Reimplement this stuff with CSS variables */
+.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
+    position: fixed;
+}
+
+@media screen and (min-width: 60rem) {
+    .alectryon-standalone .alectryon-windowed {
+        border-right-width: thin;
+        bottom: 0;
+        left: 0;
+        right: 50%;
+        top: 0;
+    }
+
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
+        bottom: 0;
+        left: 50%;
+        right: 0;
+        top: 0;
+    }
+}
+
+@media screen and (max-width: 60rem) {
+    .alectryon-standalone .alectryon-windowed {
+        border-bottom-width: 1px;
+        bottom: 40%;
+        left: 0;
+        right: 0;
+        top: 0;
+    }
+
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
+        bottom: 0;
+        left: 0;
+        right: 0;
+        top: 60%;
+    }
+}
diff --git a/static/alectryon/alectryon.js b/static/alectryon/alectryon.js
new file mode 100644
index 0000000..6a469d0
--- /dev/null
+++ b/static/alectryon/alectryon.js
@@ -0,0 +1,172 @@
+var Alectryon;
+(function(Alectryon) {
+    (function (slideshow) {
+        function anchor(sentence) { return "#" + sentence.id; }
+
+        function current_sentence() { return slideshow.sentences[slideshow.pos]; }
+
+        function unhighlight() {
+            var sentence = current_sentence();
+            if (sentence) sentence.classList.remove("alectryon-target");
+            slideshow.pos = -1;
+        }
+
+        function highlight(sentence) {
+            sentence.classList.add("alectryon-target");
+        }
+
+        function scroll(sentence) {
+            // Put the top of the current fragment close to the top of the
+            // screen, but scroll it out of view if showing it requires pushing
+            // the sentence past half of the screen.  If sentence is already in
+            // a reasonable position, don't move.
+            var parent = sentence.parentElement;
+            /* We want to scroll the whole document, so start at root… */
+            while (parent && !parent.classList.contains("alectryon-root"))
+                parent = parent.parentElement;
+            /* … and work up from there to find a scrollable element.
+               parent.scrollHeight can be greater than parent.clientHeight
+               without showing scrollbars, so we add a 10px buffer. */
+            while (parent && parent.scrollHeight <= parent.clientHeight + 10)
+                parent = parent.parentElement;
+            /* <body> and <html> elements can have their client rect overflow
+             * the window if their height is unset, so scroll the window
+             * instead */
+            if (parent && (parent.nodeName == "BODY" || parent.nodeName == "HTML"))
+                parent = null;
+
+            var rect = function(e) { return e.getBoundingClientRect(); };
+            var parent_box = parent ? rect(parent) : { y: 0, height: window.innerHeight },
+                sentence_y = rect(sentence).y - parent_box.y,
+                fragment_y = rect(sentence.parentElement).y - parent_box.y;
+
+            // The assertion below sometimes fails for the first element in a block.
+            // console.assert(sentence_y >= fragment_y);
+
+            if (sentence_y < 0.1 * parent_box.height ||
+                sentence_y > 0.7 * parent_box.height) {
+                (parent || window).scrollBy(
+                    0, Math.max(sentence_y - 0.5 * parent_box.height,
+                                fragment_y - 0.1 * parent_box.height));
+            }
+        }
+
+        function highlighted(pos) {
+            return slideshow.pos == pos;
+        }
+
+        function navigate(pos, inhibitScroll) {
+            unhighlight();
+            slideshow.pos = Math.min(Math.max(pos, 0), slideshow.sentences.length - 1);
+            var sentence = current_sentence();
+            highlight(sentence);
+            if (!inhibitScroll)
+                scroll(sentence);
+        }
+
+        var keys = {
+            PAGE_UP: 33,
+            PAGE_DOWN: 34,
+            ARROW_UP: 38,
+            ARROW_DOWN: 40,
+            h: 72, l: 76, p: 80, n: 78
+        };
+
+        function onkeydown(e) {
+            e = e || window.event;
+            if (e.ctrlKey || e.metaKey) {
+                if (e.keyCode == keys.ARROW_UP)
+                    slideshow.previous();
+                else if (e.keyCode == keys.ARROW_DOWN)
+                    slideshow.next();
+                else
+                    return;
+            } else {
+                // if (e.keyCode == keys.PAGE_UP || e.keyCode == keys.p || e.keyCode == keys.h)
+                //     slideshow.previous();
+                // else if (e.keyCode == keys.PAGE_DOWN || e.keyCode == keys.n || e.keyCode == keys.l)
+                //     slideshow.next();
+                // else
+                return;
+            }
+            e.preventDefault();
+        }
+
+        function start() {
+            slideshow.navigate(0);
+        }
+
+        function toggleHighlight(idx) {
+            if (highlighted(idx))
+                unhighlight();
+            else
+                navigate(idx, true);
+        }
+
+        function handleClick(evt) {
+            if (evt.ctrlKey || evt.metaKey) {
+                var sentence = evt.currentTarget;
+
+                // Ensure that the goal is shown on the side, not inline
+                var checkbox = sentence.getElementsByClassName("alectryon-toggle")[0];
+                if (checkbox)
+                    checkbox.checked = false;
+
+                toggleHighlight(sentence.alectryon_index);
+                evt.preventDefault();
+            }
+        }
+
+        function init() {
+            document.onkeydown = onkeydown;
+            slideshow.pos = -1;
+            slideshow.sentences = Array.from(document.getElementsByClassName("alectryon-sentence"));
+            slideshow.sentences.forEach(function (s, idx) {
+                s.addEventListener('click', handleClick, false);
+                s.alectryon_index = idx;
+            });
+        }
+
+        slideshow.start = start;
+        slideshow.end = unhighlight;
+        slideshow.navigate = navigate;
+        slideshow.next = function() { navigate(slideshow.pos + 1); };
+        slideshow.previous = function() { navigate(slideshow.pos + -1); };
+        window.addEventListener('DOMContentLoaded', init);
+    })(Alectryon.slideshow || (Alectryon.slideshow = {}));
+
+    (function (styles) {
+        var styleNames = ["centered", "floating", "windowed"];
+
+        function className(style) {
+            return "alectryon-" + style;
+        }
+
+        function setStyle(style) {
+            var root = document.getElementsByClassName("alectryon-root")[0];
+            styleNames.forEach(function (s) {
+                root.classList.remove(className(s)); });
+            root.classList.add(className(style));
+        }
+
+        function init() {
+            var banner = document.getElementsByClassName("alectryon-banner")[0];
+            if (banner) {
+                banner.append(" Style: ");
+                styleNames.forEach(function (styleName, idx) {
+                    var s = styleName;
+                    var a = document.createElement("a");
+                    a.onclick = function() { setStyle(s); };
+                    a.append(styleName);
+                    if (idx > 0) banner.append("; ");
+                    banner.appendChild(a);
+                });
+                banner.append(".");
+            }
+        }
+
+        window.addEventListener('DOMContentLoaded', init);
+
+        styles.setStyle = setStyle;
+    })(Alectryon.styles || (Alectryon.styles = {}));
+})(Alectryon || (Alectryon = {}));
diff --git a/static/alectryon/docutils_basic.css b/static/alectryon/docutils_basic.css
new file mode 100644
index 0000000..75d0615
--- /dev/null
+++ b/static/alectryon/docutils_basic.css
@@ -0,0 +1,593 @@
+/******************************************************************************
+The MIT License (MIT)
+
+Copyright (c) 2014 Matthias Eisen
+Further changes Copyright (c) 2020, 2021 Clément Pit-Claudel
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+******************************************************************************/
+
+kbd,
+pre,
+samp,
+tt,
+body code, /* Increase specificity to override IBM's stylesheet */
+body code.highlight,
+.docutils.literal {
+    font-family: 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', 'Iosevka', 'Fira Code', monospace;
+    font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
+}
+
+body {
+    color: #111;
+    font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
+    line-height: 1.5;
+}
+
+main, div.document {
+    margin: 0 auto;
+    max-width: 720px;
+}
+
+
+/* ========== Headings ========== */
+
+h1, h2, h3, h4, h5, h6 {
+    font-weight: normal;
+    margin-top: 1.5em;
+}
+
+h1.section-subtitle, 
+h2.section-subtitle, 
+h3.section-subtitle,
+h4.section-subtitle, 
+h5.section-subtitle, 
+h6.section-subtitle {
+    margin-top: 0.4em;
+}
+
+h1.title {
+    text-align: center;
+}
+
+h2.subtitle {
+    text-align: center;
+}
+
+span.section-subtitle {
+    font-size: 80%,
+}
+
+/* //-------- Headings ---------- */
+
+
+/* ========== Images ========== */
+
+img, 
+.figure, 
+object {
+    display:        block;
+    margin-left:    auto;
+    margin-right:   auto;
+}
+
+div.figure {
+    margin-left:    2em;
+    margin-right:   2em;
+}
+
+img.align-left, .figure.align-left, object.align-left {
+    clear:          left;
+    float:          left;
+    margin-right:   1em;
+}
+
+img.align-right, .figure.align-right, object.align-right {
+    clear:          right;
+    float:          right;
+    margin-left:    1em;
+}
+
+img.align-center, .figure.align-center, object.align-center {
+    display:        block;
+    margin-left:    auto;
+    margin-right:   auto;
+}
+
+/* reset inner alignment in figures */
+div.align-right {
+    text-align: inherit;
+}
+
+object[type="image/svg+xml"], 
+object[type="application/x-shockwave-flash"] {
+    overflow: hidden;
+}
+
+/* //-------- Images ---------- */
+
+
+
+/* ========== Literal Blocks ========== */
+
+.docutils.literal {
+    background-color: #eee;
+    padding: 0 0.2em;
+    border-radius: 0.1em;
+}
+
+pre.address {
+    margin-bottom: 0;
+    margin-top: 0;
+    font: inherit;
+}
+
+pre.literal-block {
+    border-left: solid 5px #ccc;
+    padding: 1em; 
+}
+
+pre.literal-block, pre.doctest-block, pre.math, pre.code {
+}
+
+span.interpreted {
+}
+
+span.pre {
+    white-space: pre;
+}
+
+pre.code .ln { 
+    color: grey; 
+}
+pre.code, code {
+    border-style: none;
+    /* ! padding: 1em 0; */ /* Removed because that large hitbox bleeds over links on other lines */
+}
+pre.code .comment, code .comment { 
+    color: #888;
+}
+pre.code .keyword, code .keyword {
+    font-weight: bold; 
+    color: #080;
+}
+pre.code .literal.string, code .literal.string { 
+    color: #d20;
+    background-color: #fff0f0;
+}
+pre.code .literal.number, code .literal.number { 
+    color: #00d;
+}
+pre.code .name.builtin, code .name.builtin {
+    color: #038;
+    color: #820;
+}
+pre.code .name.namespace, code .name.namespace {
+    color: #b06;
+}
+pre.code .deleted, code .deleted {
+    background-color: #fdd;
+}
+pre.code .inserted, code .inserted {
+    background-color: #dfd;
+}
+
+
+/* //-------- Literal Blocks --------- */
+
+
+/* ========== Tables ========== */
+
+table {
+    border-spacing:         0;
+    border-collapse:        collapse;
+    border-style:           none;
+    border-top:             solid thin #111;
+    border-bottom:          solid thin #111;
+}
+
+td, 
+th {
+    border: none;
+    padding:                0.5em;
+    vertical-align:         top;
+}
+
+th {
+    border-top:             solid thin #111;
+    border-bottom:          solid thin #111;
+    background-color:       #ddd;
+}
+
+
+table.field-list,
+table.footnote,
+table.citation,
+table.option-list {
+    border:                 none;
+}
+table.docinfo {
+    margin:                 2em 4em;
+}
+
+table.docutils {
+    margin:                 1em 0;
+}
+
+table.docutils th.field-name, 
+table.docinfo th.docinfo-name {
+    border:                 none;
+    background:             none;
+    font-weight:            bold ;
+    text-align:             left ;
+    white-space:            nowrap ;
+    padding-left:           0;
+    vertical-align:         middle; 
+}
+
+table.docutils.booktabs {
+    border:                 none;
+    border-top:             medium solid;
+    border-bottom:          medium solid;
+    border-collapse:        collapse;
+}
+
+table.docutils.booktabs * {
+    border:                 none;
+}
+table.docutils.booktabs th {
+    border-bottom:          thin solid;
+    text-align:             left;
+}
+
+span.option {
+    white-space: nowrap;
+}
+
+table caption {
+    margin-bottom: 2px;
+}
+
+/* //-------- Tables ---------- */
+
+
+/* ========== Lists ========== */
+
+ol.simple, ul.simple {
+    margin-bottom: 1em;
+}
+
+ol.arabic {
+    list-style: decimal;
+}
+
+ol.loweralpha {
+    list-style: lower-alpha;
+}
+
+ol.upperalpha {
+    list-style: upper-alpha;
+}
+
+ol.lowerroman {
+    list-style: lower-roman;
+}
+
+ol.upperroman {
+    list-style: upper-roman;
+}
+
+dl.docutils dd {
+    margin-bottom: 0.5em;
+}
+
+
+dl.docutils dt {
+    font-weight: bold;
+}
+
+/* //-------- Lists ---------- */
+
+
+/* ========== Sidebar ========== */
+
+div.sidebar {
+    margin: 0 0 0.5em 1em ;
+    border-left: solid medium #111;
+    padding: 1em ;
+    width: 40% ;
+    float: right ;
+    clear: right;
+}
+
+div.sidebar {
+    font-size: 0.9rem;
+}
+
+p.sidebar-title {
+    font-size: 1rem;
+    font-weight: bold ;
+}
+
+p.sidebar-subtitle {
+    font-weight: bold;
+}
+
+/* //-------- Sidebar ---------- */
+
+
+/* ========== Topic ========== */
+
+div.topic {
+    border-left: thin solid #111;
+    padding-left: 1em;
+}
+
+div.topic p {
+    padding: 0;
+}
+
+p.topic-title {
+    font-weight: bold;
+}
+
+/* //-------- Topic ---------- */
+
+
+/* ========== Header ========== */
+
+div.header {
+    font-family:        "Century Gothic", CenturyGothic, Geneva, AppleGothic, sans-serif;
+    font-size:          0.9rem;
+    margin:             2em auto 4em auto;
+    max-width:          960px;
+    clear:              both;
+}
+
+hr.header {
+    border:             0;
+    height:             1px;
+    margin-top:         1em;
+    background-color:   #111;
+}
+
+/* //-------- Header ---------- */
+
+
+/* ========== Footer ========== */
+
+div.footer {
+    font-family:        "Century Gothic", CenturyGothic, Geneva, AppleGothic, sans-serif;
+    font-size:          0.9rem;
+    margin:             6em auto 2em auto;
+    max-width:          960px;
+    clear:              both;
+    text-align:         center;
+}
+
+hr.footer {
+    border:             0;
+    height:             1px;
+    margin-bottom:      2em;
+    background-color:   #111;
+}
+
+/* //-------- Footer ---------- */
+
+
+/* ========== Admonitions ========== */
+
+div.admonition, 
+div.attention, 
+div.caution, 
+div.danger, 
+div.error,
+div.hint, 
+div.important, 
+div.note, 
+div.tip, 
+div.warning {
+    border: solid thin #111;
+    padding: 0 1em;
+}
+
+div.error,
+div.danger {
+    border-color: #a94442;
+    background-color: #f2dede;
+}
+
+div.hint,
+div.tip {
+    border-color: #31708f;
+    background-color: #d9edf7;
+}
+
+div.attention,
+div.caution,
+div.warning {
+    border-color: #8a6d3b;
+    background-color: #fcf8e3; 
+}
+
+div.hint p.admonition-title,
+div.tip p.admonition-title {
+    color: #31708f;
+    font-weight: bold ;
+}
+
+div.note p.admonition-title,
+div.admonition p.admonition-title, 
+div.important p.admonition-title {
+    font-weight: bold ;
+}
+
+div.attention p.admonition-title,
+div.caution p.admonition-title,
+div.warning p.admonition-title {
+    color: #8a6d3b;
+    font-weight: bold ;
+}
+
+div.danger p.admonition-title, 
+div.error p.admonition-title,
+.code .error {
+    color: #a94442;
+    font-weight: bold ;
+}
+
+/* //-------- Admonitions ---------- */
+
+
+/* ========== Table of Contents ========== */
+
+div.contents {
+    margin: 2em 0;
+    border: none;
+}
+
+ul.auto-toc {
+    list-style-type: none;
+}
+
+a.toc-backref {
+    text-decoration: none ;
+    color: #111;
+}
+
+/* //-------- Table of Contents ---------- */
+
+
+
+/* ========== Line Blocks========== */
+
+div.line-block {
+    display: block ;
+    margin-top: 1em ;
+    margin-bottom: 1em;
+}
+
+div.line-block div.line-block {
+    margin-top: 0 ;
+    margin-bottom: 0 ;
+    margin-left: 1.5em;
+}
+
+/* //-------- Line Blocks---------- */
+
+
+/* ========== System Messages ========== */
+
+div.system-messages {
+    margin: 5em;
+}
+
+div.system-messages h1 {
+    color: red;
+}
+
+div.system-message {
+    border: medium outset ;
+    padding: 1em;
+}
+
+div.system-message p.system-message-title {
+    color: red ;
+    font-weight: bold;
+}
+
+/* //-------- System Messages---------- */
+
+
+/* ========== Helpers ========== */
+
+.hidden {
+    display: none;
+}
+
+.align-left {
+    text-align: left;
+}
+
+.align-center {
+    clear: both ;
+    text-align: center;
+}
+
+.align-right {
+    text-align: right;
+}
+
+/* //-------- Helpers---------- */
+
+
+p.caption {
+    font-style: italic;
+    text-align: center;
+}
+
+p.credits {
+font-style: italic ;
+font-size: smaller }
+
+p.label {
+white-space: nowrap }
+
+p.rubric {
+font-weight: bold ;
+font-size: larger ;
+color: maroon ;
+text-align: center }
+
+p.attribution {
+text-align: right ;
+margin-left: 50% }
+
+blockquote.epigraph {
+    margin: 2em 5em;
+}
+
+div.abstract {
+margin: 2em 5em }
+
+div.abstract {
+font-weight: bold ;
+text-align: center }
+
+div.dedication {
+margin: 2em 5em ;
+text-align: center ;
+font-style: italic }
+
+div.dedication {
+font-weight: bold ;
+font-style: normal }
+
+
+span.classifier {
+font-style: oblique }
+
+span.classifier-delimiter {
+font-weight: bold }
+
+span.problematic {
+color: red }
+
+
+