Migrate to `Felix` namespaceHEADhotg

5 files changed, 0 insertions, 5484 deletions

diff --git a/source/Render/Html.hs b/source/Render/Html.hs
deleted file mode 100644
index c37a278..0000000
--- a/source/Render/Html.hs
+++ /dev/null
@@ -1,3963 +0,0 @@
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RecordWildCards #-}
-
-module Render.Html
-    ( HtmlRenderIndex
-    , HtmlPagePresentation
-    , buildRenderIndex
-    , htmlPagePresentationSource
-    , renderDocument
-    , supportScriptAssetContents
-    ) where
-
-import Syntax.Abstract
-
-import Base
-import Felix.Source (ResolvedSource)
-import Lucid hiding (Term, for_)
-import Lucid.Base (makeAttributes)
-import Lucid.Math
-import Render.Html.Context
-    ( HtmlRenderContext
-    , HtmlRenderContextError
-    , htmlCurrentPageLabel
-    , htmlCurrentSource
-    , htmlSourceFragmentHref
-    , htmlSourceLabel
-    , htmlSourcePageHref
-    , htmlSupportScriptHref
-    )
-import Render.Html.Layout (renderUrlFragment)
-
-import Control.Monad (unless, when)
-import Data.Char (digitToInt, isAlphaNum, isDigit, isSpace, toUpper)
-import Data.List qualified as List
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Map.Strict qualified as Map
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import Data.Text.Lazy qualified as LazyText
-import Report.Location (Location, pattern Nowhere)
-import Syntax.Token (VariableDisplay(..), VariableSuffix(..), displayVariable, tokToText)
-
-
-data HintCategory
-    = OperatorHint
-    | RelationHint
-    | PredicateHint
-    | StructOpHint
-    deriving (Show, Eq, Ord)
-
-data TemplatePiece
-    = Literal Text
-    | Slot Int
-    deriving (Show, Eq, Ord)
-
-data RenderHint = RenderHint
-    { renderHintArity :: Int
-    , renderHintTemplate :: [TemplatePiece]
-    } deriving (Show, Eq, Ord)
-
-type HintMap = Map (HintCategory, Marker, Int) RenderHint
-type AnchorMap = Map Marker Text
-type BlockRenderInfo = (Int, Block, Text)
-type PreviewMap = Map Marker PreviewEntry
-
-data HtmlRenderIndex = HtmlRenderIndex
-    !(Map Marker IndexedReferenceTarget)
-
-data HtmlPagePresentation = HtmlPagePresentation
-    { htmlPagePresentationSource :: !ResolvedSource
-    , pagePresentationBlockInfos :: ![BlockRenderInfo]
-    , pagePresentationAnchors :: !AnchorMap
-    , pagePresentationReferencedMarkers :: !(Set Marker)
-    }
-
-data IndexedReferenceTarget = IndexedReferenceTarget
-    !Int
-    !ResolvedSource
-    !ReferenceTarget
-
-data ReferenceContext = ReferenceContext
-    { referenceAnchors :: AnchorMap
-    , referencePreviews :: PreviewMap
-    }
-
-data PreviewEntry = PreviewEntry
-    { previewMarker :: Marker
-    , previewKind :: Text
-    , previewTitle :: Maybe Text
-    , previewSourceLabel :: Text
-    , previewSourceHref :: Text
-    , previewReferenceHref :: Text
-    , previewId :: Text
-    , previewBody :: HintMap -> Html ()
-    }
-
-data ReferenceTarget = ReferenceTarget
-    { targetMarker :: Marker
-    , targetAnchorId :: Text
-    , targetKind :: Text
-    , targetTitle :: Maybe Text
-    , targetBody :: HintMap -> Html ()
-    }
-
-data StmtMathFragment
-    = StmtMathProse Text
-    | StmtMathNode (Html ())
-
-type StmtMathFragments = [StmtMathFragment]
-
-newtype MissingHintMap = MissingHintMap
-    { unMissingHintMap :: Map HintCategory (Set Marker)
-    } deriving (Show, Eq)
-
-instance Semigroup MissingHintMap where
-    MissingHintMap left <> MissingHintMap right =
-        MissingHintMap (Map.unionWith (<>) left right)
-
-instance Monoid MissingHintMap where
-    mempty = MissingHintMap mempty
-
-proofCollapseThreshold :: Int
-proofCollapseThreshold = 10
-
-referenceGroupThreshold :: Int
-referenceGroupThreshold = 5
-
-
-renderDocument
-    :: HtmlRenderContext
-    -> Text
-    -> HtmlRenderIndex
-    -> HtmlPagePresentation
-    -> Either HtmlRenderContextError Text
-renderDocument
-        context
-        hintsSource
-        renderIndex
-        HtmlPagePresentation
-            { pagePresentationBlockInfos = blockInfos
-            , pagePresentationAnchors = anchors
-            , pagePresentationReferencedMarkers = referencedMarkers
-            } = do
-    previews <-
-        buildPreviewMap
-            context
-            referencedMarkers
-            anchors
-            renderIndex
-    let result =
-            case formatMissingHintWarning missingHints of
-                Nothing -> rendered
-                Just warningText ->
-                    trace (Text.unpack warningText) rendered
-        hints = parseHints hintsSource
-        missingHints =
-            collectMissingHints
-                hints
-                [ block
-                | (_index, block, _blockId) <- blockInfos
-                ]
-        rendered = LazyText.toStrict (renderText (renderPage hints))
-        pageLabel = htmlCurrentPageLabel context
-        tocBlocks = [(index, blockId, block) | (index, block, blockId) <- blockInfos, includeInToc block]
-        referenceContext = ReferenceContext anchors previews
-
-        renderPage :: HintMap -> Html ()
-        renderPage hintMap = doctypehtml_ do
-            head_ do
-                meta_ [charset_ "utf-8"]
-                title_ (toHtml pageLabel)
-                style_ pageStyles
-            body_ do
-                div_ [class_ "page-layout"] do
-                    aside_ [class_ "toc-column"] do
-                        nav_ [class_ "toc"] do
-                            h2_ [class_ "toc-heading"] "Contents"
-                            input_
-                                [ class_ "toc-filter"
-                                , type_ "search"
-                                , placeholder_ "Filter labels"
-                                , makeAttributes "aria-label" "Filter TOC by label"
-                                ]
-                            ol_ [class_ "toc-list"] do
-                                traverse_ renderTocEntry tocBlocks
-                    main_ do
-                        h1_ (toHtml pageLabel)
-                        traverse_ (renderBlock hintMap referenceContext) blockInfos
-                renderPreviewStore hintMap previews
-                div_
-                    [ id_ "reference-preview-popup"
-                    , class_ "reference-preview-popup"
-                    , makeAttributes "role" "tooltip"
-                    , makeAttributes "aria-hidden" "true"
-                    ]
-                    skip
-                script_
-                    [src_ (htmlSupportScriptHref context)]
-                    ("" :: Text)
-    Right result
-
--- | Index every block target and every page's referenced markers once in
--- deterministic source order.  Rendering a page subsequently performs only
--- marker lookups in the shared index.
-buildRenderIndex
-    :: NonEmpty (ResolvedSource, [Block])
-    -> (HtmlRenderIndex, NonEmpty HtmlPagePresentation)
-buildRenderIndex sourceBlocks =
-    ( HtmlRenderIndex
-        (Map.fromList
-            [ ( targetMarker target
-              , IndexedReferenceTarget ordinal source target
-              )
-            | (ordinal, (source, target)) <-
-                zip [1 :: Int ..] orderedTargets
-            ])
-    , pages
-    )
-  where
-    analysedPages =
-        uncurry analysePage <$> sourceBlocks
-    pages =
-        fst <$> analysedPages
-    orderedTargets =
-        [ (htmlPagePresentationSource page, target)
-        | (page, targets) <- NonEmpty.toList analysedPages
-        , target <- targets
-        ]
-
-    analysePage source blocks =
-        ( HtmlPagePresentation
-            { htmlPagePresentationSource = source
-            , pagePresentationBlockInfos = blockInfos
-            , pagePresentationAnchors =
-                Map.fromList
-                    [ (targetMarker, targetAnchorId)
-                    | ReferenceTarget
-                        { targetMarker
-                        , targetAnchorId
-                        } <- targets
-                    ]
-            , pagePresentationReferencedMarkers =
-                foldMap
-                    (\(_blockInfo, _targets, references) -> references)
-                    analysedBlocks
-            }
-        , targets
-        )
-      where
-        analysedBlocks =
-            [ ( blockInfo
-              , referenceTargetsOfBlockRenderInfo blockInfo
-              , collectReferencedMarkersOfBlock block
-              )
-            | (index, block) <- zip [1 :: Int ..] blocks
-            , let blockInfo =
-                    (index, block, blockAnchorId index block)
-            ]
-        blockInfos =
-            [ blockInfo
-            | (blockInfo, _targets, _references) <- analysedBlocks
-            ]
-        targets =
-            concat
-                [ blockTargets
-                | (_blockInfo, blockTargets, _references) <- analysedBlocks
-                ]
-
-
-pageStyles :: Text
-pageStyles = Text.unlines
-    [ ":root {"
-    , "  color-scheme: light dark;"
-    , "  font-family: Georgia, \"Times New Roman\", serif;"
-    , "  --page-bg: #ffffff;"
-    , "  --page-fg: #111111;"
-    , "  --muted-fg: #666666;"
-    , "  --subtle-fg: #444444;"
-    , "  --badge-bg: #f1f1f1;"
-    , "  --badge-border: #dddddd;"
-    , "  --badge-fg: #555555;"
-    , "  --rule-color: #d9d2c2;"
-    , "  --error-fg: #9f1d1d;"
-    , "  --error-bg: #fff1f1;"
-    , "  --toc-active-bg: #f3efe6;"
-    , "  --toc-active-fg: #1b1b1b;"
-    , "  --toc-active-accent: #b9aa7a;"
-    , "  --preview-bg: #fffdf8;"
-    , "  --preview-border: #cfc3a3;"
-    , "  --preview-shadow: rgba(0, 0, 0, 0.18);"
-    , "}"
-    , "html {"
-    , "  height: 100%;"
-    , "}"
-    , "body {"
-    , "  margin: 0;"
-    , "  height: 100vh;"
-    , "  overflow: hidden;"
-    , "  line-height: 1.5;"
-    , "  background: var(--page-bg);"
-    , "  color: var(--page-fg);"
-    , "}"
-    , ".page-layout {"
-    , "  display: grid;"
-    , "  grid-template-columns: minmax(16rem, 24rem) minmax(0, 1fr);"
-    , "  grid-template-rows: minmax(0, 1fr);"
-    , "  gap: 2rem;"
-    , "  align-items: stretch;"
-    , "  box-sizing: border-box;"
-    , "  margin: 0 auto;"
-    , "  max-width: 84rem;"
-    , "  height: 100vh;"
-    , "  padding: 2rem 1.25rem 3rem;"
-    , "}"
-    , ".toc-column {"
-    , "  display: block;"
-    , "  min-height: 0;"
-    , "}"
-    , ".toc {"
-    , "  display: flex;"
-    , "  flex-direction: column;"
-    , "  height: 100%;"
-    , "  min-height: 0;"
-    , "}"
-    , ".toc-heading {"
-    , "  margin: 0 0 0.75rem;"
-    , "  color: var(--muted-fg);"
-    , "  font-size: 0.9rem;"
-    , "  letter-spacing: 0.04em;"
-    , "  text-transform: uppercase;"
-    , "}"
-    , ".toc-filter {"
-    , "  box-sizing: border-box;"
-    , "  width: 100%;"
-    , "  margin: 0 0 0.9rem;"
-    , "  padding: 0.45rem 0.55rem;"
-    , "  border: 1px solid var(--badge-border);"
-    , "  border-radius: 0.35rem;"
-    , "  background: var(--page-bg);"
-    , "  color: var(--page-fg);"
-    , "  font: inherit;"
-    , "}"
-    , ".toc-filter::placeholder {"
-    , "  color: var(--muted-fg);"
-    , "}"
-    , ".toc-list {"
-    , "  flex: 1 1 auto;"
-    , "  min-height: 0;"
-    , "  overflow-y: auto;"
-    , "  list-style: none;"
-    , "  margin: 0;"
-    , "  padding: 0 0.5rem 0 0;"
-    , "}"
-    , ".toc-list > li {"
-    , "  margin: 0 0 0.8rem;"
-    , "}"
-    , ".toc-list > li > a {"
-    , "  display: block;"
-    , "  margin: -0.15rem -0.35rem;"
-    , "  padding: 0.15rem 0.35rem;"
-    , "  border-radius: 0.35rem;"
-    , "  color: inherit;"
-    , "  text-decoration: none;"
-    , "  transition: background-color 120ms ease, box-shadow 120ms ease, color 120ms ease;"
-    , "}"
-    , ".toc-list > li > a:hover,"
-    , ".toc-list > li > a:focus-visible {"
-    , "  text-decoration: underline;"
-    , "}"
-    , ".toc-list > li > a.is-active {"
-    , "  background: var(--toc-active-bg);"
-    , "  box-shadow: inset 0.2rem 0 0 var(--toc-active-accent);"
-    , "  color: var(--toc-active-fg);"
-    , "}"
-    , ".toc-list > li > a.is-active > code {"
-    , "  color: var(--toc-active-fg);"
-    , "}"
-    , ".toc-list > li > a > span:first-child {"
-    , "  display: block;"
-    , "  font-weight: 700;"
-    , "}"
-    , ".toc-list > li > a > code {"
-    , "  display: block;"
-    , "  margin-top: 0.15rem;"
-    , "  color: var(--muted-fg);"
-    , "  font-size: 0.9em;"
-    , "  overflow-wrap: anywhere;"
-    , "}"
-    , "main {"
-    , "  min-width: 0;"
-    , "  min-height: 0;"
-    , "  overflow-y: auto;"
-    , "}"
-    , "main > *[id] {"
-    , "  display: block;"
-    , "  margin: 0 0 1rem;"
-    , "  scroll-margin-top: 1rem;"
-    , "}"
-    , "head- {"
-    , "  font-weight: 700;"
-    , "}"
-    , "title- {"
-    , "  font-weight: 400;"
-    , "}"
-    , "id-,"
-    , "main a[href^=\"#\"],"
-    , ".ref-badge {"
-    , "  display: inline-block;"
-    , "  padding: 0.02rem 0.35rem;"
-    , "  border: 1px solid var(--badge-border);"
-    , "  border-radius: 0.2rem;"
-    , "  background: var(--badge-bg);"
-    , "  color: var(--badge-fg);"
-    , "  font-family: \"SFMono-Regular\", Menlo, Consolas, \"Liberation Mono\", monospace;"
-    , "  font-size: 0.82em;"
-    , "  text-decoration: none;"
-    , "}"
-    , "head- > id- {"
-    , "  margin-left: 0.45rem;"
-    , "}"
-    , "main a[href^=\"#\"]:hover,"
-    , "main a[href^=\"#\"]:focus-visible,"
-    , ".ref-badge.has-preview:hover,"
-    , ".ref-badge.has-preview:focus-visible {"
-    , "  text-decoration: underline;"
-    , "}"
-    , ".ref-badge.has-preview {"
-    , "  cursor: help;"
-    , "}"
-    , ".ref-badge-group {"
-    , "  user-select: none;"
-    , "}"
-    , "proof- > p:first-child,"
-    , "proof- > details > summary + p {"
-    , "  display: inline;"
-    , "  margin: 0;"
-    , "}"
-    , "proof- proof- {"
-    , "  display: block;"
-    , "  margin: 0.5rem 0 0.5rem 1rem;"
-    , "  padding-left: 0.75rem;"
-    , "  border-left: 1px solid var(--rule-color);"
-    , "}"
-    , "proof- > details {"
-    , "  margin: 0;"
-    , "}"
-    , "proof- > details > summary {"
-    , "  cursor: pointer;"
-    , "  font-weight: 700;"
-    , "}"
-    , "proof- > details > summary title- {"
-    , "  font-weight: 400;"
-    , "}"
-    , "proof- > details > :not(summary) {"
-    , "  margin-top: 0.5rem;"
-    , "}"
-    , "inductive- > details {"
-    , "  margin-top: 0.75rem;"
-    , "}"
-    , "inductive- > details > summary {"
-    , "  cursor: pointer;"
-    , "  font-weight: 700;"
-    , "}"
-    , "inductive- > details > :not(summary) {"
-    , "  margin-top: 0.5rem;"
-    , "}"
-    , ".inductive-derived-facts > li {"
-    , "  margin: 0.35rem 0;"
-    , "}"
-    , ".inductive-derived-facts {"
-    , "  margin: 0;"
-    , "  padding-left: 1.5rem;"
-    , "}"
-    , ".reference-preview-store {"
-    , "  display: none;"
-    , "}"
-    , ".reference-preview-popup {"
-    , "  position: fixed;"
-    , "  z-index: 1000;"
-    , "  box-sizing: border-box;"
-    , "  width: 44rem;"
-    , "  max-width: calc(100vw - 2rem);"
-    , "  max-height: 34rem;"
-    , "  max-height: min(34rem, calc(100vh - 2rem));"
-    , "  overflow: auto;"
-    , "  overscroll-behavior: contain;"
-    , "  padding: 0.75rem 0.9rem;"
-    , "  border: 1px solid var(--preview-border);"
-    , "  border-radius: 0.45rem;"
-    , "  background: var(--preview-bg);"
-    , "  color: var(--page-fg);"
-    , "  box-shadow: 0 0.75rem 2.25rem var(--preview-shadow);"
-    , "  opacity: 0;"
-    , "  pointer-events: none;"
-    , "  transform: translateY(0.2rem);"
-    , "  transition: opacity 90ms ease, transform 90ms ease;"
-    , "}"
-    , ".reference-preview-popup[aria-hidden=\"true\"] {"
-    , "  visibility: hidden;"
-    , "}"
-    , ".reference-preview-popup.is-visible {"
-    , "  opacity: 1;"
-    , "  pointer-events: auto;"
-    , "  transform: translateY(0);"
-    , "}"
-    , ".reference-preview-popup * {"
-    , "  box-sizing: border-box;"
-    , "}"
-    , ".reference-preview-template {"
-    , "  display: flex;"
-    , "  flex-direction: column;"
-    , "  gap: 0.45rem;"
-    , "  width: 100%;"
-    , "}"
-    , ".reference-preview-heading {"
-    , "  display: block;"
-    , "  margin: 0;"
-    , "  width: 100%;"
-    , "  color: var(--muted-fg);"
-    , "  font-size: 0.82rem;"
-    , "  letter-spacing: 0.035em;"
-    , "  text-transform: uppercase;"
-    , "}"
-    , ".reference-preview-heading code {"
-    , "  color: var(--page-fg);"
-    , "  font-family: \"SFMono-Regular\", Menlo, Consolas, \"Liberation Mono\", monospace;"
-    , "  letter-spacing: 0;"
-    , "  text-transform: none;"
-    , "}"
-    , ".reference-preview-heading a {"
-    , "  color: inherit;"
-    , "  text-decoration: none;"
-    , "}"
-    , ".reference-preview-heading a:hover,"
-    , ".reference-preview-heading a:focus-visible {"
-    , "  text-decoration: underline;"
-    , "}"
-    , ".reference-preview-source {"
-    , "  display: block;"
-    , "  margin: 0;"
-    , "  color: var(--subtle-fg);"
-    , "  font-size: 0.78rem;"
-    , "  letter-spacing: 0;"
-    , "  text-transform: none;"
-    , "}"
-    , ".reference-preview-body {"
-    , "  display: block;"
-    , "  clear: both;"
-    , "  margin: 0;"
-    , "  width: 100%;"
-    , "}"
-    , ".reference-preview-body p {"
-    , "  margin: 0.35rem 0 0;"
-    , "}"
-    , ".reference-preview-body p:first-child {"
-    , "  margin-top: 0;"
-    , "}"
-    , ".reference-preview-group-template {"
-    , "  display: flex;"
-    , "  flex-direction: column;"
-    , "  gap: 1rem;"
-    , "  margin: 0;"
-    , "  width: 100%;"
-    , "}"
-    , ".reference-preview-group-template > .reference-preview-template + .reference-preview-template {"
-    , "  padding-top: 1rem;"
-    , "  border-top: 1px solid var(--badge-border);"
-    , "}"
-    , ".reference-preview-statement {"
-    , "  display: block;"
-    , "  width: 100%;"
-    , "  white-space: normal;"
-    , "  overflow-wrap: break-word;"
-    , "}"
-    , ".reference-preview-statement math {"
-    , "  max-width: 100%;"
-    , "  overflow-x: auto;"
-    , "  overflow-y: hidden;"
-    , "  vertical-align: middle;"
-    , "}"
-    , "math[display=\"block\"] {"
-    , "  display: block;"
-    , "  margin: 0.5rem 0;"
-    , "}"
-    , "merror {"
-    , "  color: var(--error-fg);"
-    , "  background: var(--error-bg);"
-    , "}"
-    , "@media (prefers-color-scheme: dark) {"
-    , "  :root {"
-    , "    --page-bg: #161616;"
-    , "    --page-fg: #e9e6df;"
-    , "    --muted-fg: #b7b0a4;"
-    , "    --subtle-fg: #cfc8bc;"
-    , "    --badge-bg: #2a2a2a;"
-    , "    --badge-border: #444444;"
-    , "    --badge-fg: #d8d3ca;"
-    , "    --rule-color: #5b5348;"
-    , "    --error-fg: #ffb0b0;"
-    , "    --error-bg: #3b1f1f;"
-    , "    --toc-active-bg: #2b271f;"
-    , "    --toc-active-fg: #f0ebe1;"
-    , "    --toc-active-accent: #99865a;"
-    , "    --preview-bg: #211f1a;"
-    , "    --preview-border: #776a50;"
-    , "    --preview-shadow: rgba(0, 0, 0, 0.55);"
-    , "  }"
-    , "}"
-    , "@media (max-width: 900px) {"
-    , "  body {"
-    , "    height: auto;"
-    , "    overflow: auto;"
-    , "  }"
-    , "  .page-layout {"
-    , "    grid-template-columns: 1fr;"
-    , "    grid-template-rows: auto;"
-    , "    gap: 1.5rem;"
-    , "    height: auto;"
-    , "  }"
-    , "  .toc-column {"
-    , "    display: none;"
-    , "  }"
-    , "  main {"
-    , "    min-height: auto;"
-    , "    overflow: visible;"
-    , "  }"
-    , "}"
-    ]
-
-supportScriptAssetContents :: Text
-supportScriptAssetContents = tocScript <> "\n" <> referencePreviewScript
-
-
-tocScript :: Text
-tocScript = Text.unlines
-    [ "(function () {"
-    , "  const toc = document.querySelector('.toc');"
-    , "  const tocList = toc ? toc.querySelector('.toc-list') : null;"
-    , "  const filterInput = toc ? toc.querySelector('.toc-filter') : null;"
-    , "  const content = document.querySelector('main');"
-    , "  if (!toc || !tocList || !content) return;"
-    , "  const links = Array.from(tocList.querySelectorAll(':scope > li > a[href^=\"#\"]'));"
-    , "  const blocks = Array.from(content.querySelectorAll(':scope > *[id]'));"
-    , "  if (!links.length || !blocks.length) return;"
-    , "  const linkByTarget = new Map(links.map((link) => [decodeURIComponent(link.hash.slice(1)), link]));"
-    , "  const tocEntries = links.map((link) => ({"
-    , "    item: link.parentElement,"
-    , "    link,"
-    , "    label: ((link.querySelector('code') || link.lastElementChild || link).textContent || '').trim().toLowerCase()"
-    , "  }));"
-    , "  let activeTarget = null;"
-    , "  let rafId = 0;"
-    , "  let suspendUntil = 0;"
-    , ""
-    , "  const keepActiveLinkVisible = (link) => {"
-    , "    if (!link || performance.now() < suspendUntil) return;"
-    , "    const item = link.parentElement;"
-    , "    if (item && item.hidden) return;"
-    , "    const tocRect = tocList.getBoundingClientRect();"
-    , "    const linkRect = link.getBoundingClientRect();"
-    , "    const comfortTop = tocRect.top + tocRect.height * 0.2;"
-    , "    const comfortBottom = tocRect.bottom - tocRect.height * 0.2;"
-    , "    if (linkRect.top < comfortTop || linkRect.bottom > comfortBottom) {"
-    , "      link.scrollIntoView({ block: 'nearest', inline: 'nearest' });"
-    , "    }"
-    , "  };"
-    , ""
-    , "  const applyFilter = () => {"
-    , "    const query = filterInput ? filterInput.value.trim().toLowerCase() : '';"
-    , "    for (const { item, label } of tocEntries) {"
-    , "      if (!item) continue;"
-    , "      item.hidden = query !== '' && !label.includes(query);"
-    , "    }"
-    , "    if (activeTarget) {"
-    , "      keepActiveLinkVisible(linkByTarget.get(activeTarget));"
-    , "    }"
-    , "  };"
-    , ""
-    , "  const setActiveTarget = (target) => {"
-    , "    if (!target || target === activeTarget) return;"
-    , "    const previous = activeTarget ? linkByTarget.get(activeTarget) : null;"
-    , "    if (previous) {"
-    , "      previous.classList.remove('is-active');"
-    , "      previous.removeAttribute('aria-current');"
-    , "    }"
-    , "    activeTarget = target;"
-    , "    const next = linkByTarget.get(target);"
-    , "    if (!next) return;"
-    , "    next.classList.add('is-active');"
-    , "    next.setAttribute('aria-current', 'location');"
-    , "    keepActiveLinkVisible(next);"
-    , "  };"
-    , ""
-    , "  const firstTarget = blocks[0].id;"
-    , ""
-    , "  const findActiveTarget = () => {"
-    , "    const contentRect = content.getBoundingClientRect();"
-    , "    const topSnapThreshold = 40;"
-    , "    for (const block of blocks) {"
-    , "      const target = block.id;"
-    , "      const rect = block.getBoundingClientRect();"
-    , "      if (rect.top >= contentRect.top - 4 && rect.top <= contentRect.top + topSnapThreshold) {"
-    , "        return target;"
-    , "      }"
-    , "    }"
-    , "    const activationLine = contentRect.top + contentRect.height * 0.22;"
-    , "    let candidate = firstTarget;"
-    , "    for (const block of blocks) {"
-    , "      const target = block.id;"
-    , "      if (block.getBoundingClientRect().top <= activationLine) {"
-    , "        candidate = target;"
-    , "        continue;"
-    , "      }"
-    , "      break;"
-    , "    }"
-    , "    return candidate;"
-    , "  };"
-    , ""
-    , "  const scheduleUpdate = () => {"
-    , "    if (rafId) return;"
-    , "    rafId = window.requestAnimationFrame(() => {"
-    , "      rafId = 0;"
-    , "      setActiveTarget(findActiveTarget());"
-    , "    });"
-    , "  };"
-    , ""
-    , "  const suspendAutofollow = () => {"
-    , "    suspendUntil = performance.now() + 1500;"
-    , "  };"
-    , ""
-    , "  const revealTarget = (target) => {"
-    , "    let parent = target.parentElement;"
-    , "    while (parent) {"
-    , "      if (parent.localName === 'details') {"
-    , "        parent.open = true;"
-    , "      }"
-    , "      parent = parent.parentElement;"
-    , "    }"
-    , "  };"
-    , ""
-    , "  const scrollToTarget = (targetId) => {"
-    , "    const target = document.getElementById(targetId);"
-    , "    if (!target || !content.contains(target)) return false;"
-    , "    revealTarget(target);"
-    , "    target.scrollIntoView({ block: 'start', inline: 'nearest' });"
-    , "    setActiveTarget(targetId);"
-    , "    return true;"
-    , "  };"
-    , ""
-    , "  content.addEventListener('scroll', scheduleUpdate, { passive: true });"
-    , "  window.addEventListener('resize', scheduleUpdate);"
-    , "  tocList.addEventListener('wheel', suspendAutofollow, { passive: true });"
-    , "  tocList.addEventListener('touchstart', suspendAutofollow, { passive: true });"
-    , "  toc.addEventListener('pointerdown', suspendAutofollow);"
-    , "  toc.addEventListener('focusin', suspendAutofollow);"
-    , "  if (filterInput) {"
-    , "    filterInput.addEventListener('input', applyFilter);"
-    , "  }"
-    , "  for (const details of content.querySelectorAll('details')) {"
-    , "    details.addEventListener('toggle', scheduleUpdate);"
-    , "  }"
-    , ""
-    , "  toc.addEventListener('click', (event) => {"
-    , "    const link = event.target.closest('a[href^=\"#\"]');"
-    , "    if (!link || !tocList.contains(link)) return;"
-    , "    const targetId = decodeURIComponent(link.hash.slice(1));"
-    , "    if (!scrollToTarget(targetId)) return;"
-    , "    event.preventDefault();"
-    , "    suspendUntil = 0;"
-    , "    if (location.hash !== '#' + targetId) {"
-    , "      try {"
-    , "        history.pushState(null, '', '#' + targetId);"
-    , "      } catch (_error) {"
-    , "        location.hash = targetId;"
-    , "      }"
-    , "    }"
-    , "  });"
-    , ""
-    , "  window.addEventListener('hashchange', () => {"
-    , "    if (location.hash.length <= 1) return;"
-    , "    const hashTarget = decodeURIComponent(location.hash.slice(1));"
-    , "    if (!scrollToTarget(hashTarget)) scheduleUpdate();"
-    , "  });"
-    , ""
-    , "  if (location.hash.length > 1) {"
-    , "    const hashTarget = decodeURIComponent(location.hash.slice(1));"
-    , "    window.requestAnimationFrame(() => {"
-    , "      applyFilter();"
-    , "      if (!scrollToTarget(hashTarget)) scheduleUpdate();"
-    , "    });"
-    , "    return;"
-    , "  }"
-    , ""
-    , "  applyFilter();"
-    , "  scheduleUpdate();"
-    , "})();"
-    ]
-
-referencePreviewScript :: Text
-referencePreviewScript = Text.unlines
-    [ "(function () {"
-    , "  const content = document.querySelector('main');"
-    , "  const popup = document.getElementById('reference-preview-popup');"
-    , "  if (!content || !popup) return;"
-    , "  let activeTrigger = null;"
-    , "  let lastPointer = null;"
-    , "  let isPinned = false;"
-    , "  let hideTimer = 0;"
-    , "  const offset = 14;"
-    , "  const margin = 12;"
-    , "  const hideDelay = 180;"
-    , ""
-    , "  const cloneHiddenPreview = (trigger) => {"
-    , "    const previewId = trigger.getAttribute('data-preview-id');"
-    , "    const template = previewId ? document.getElementById(previewId) : null;"
-    , "    if (!template) return null;"
-    , "    const clone = template.cloneNode(true);"
-    , "    clone.removeAttribute('id');"
-    , "    return clone;"
-    , "  };"
-    , ""
-    , "  const buildCurrentPreview = (trigger) => {"
-    , "    const targetId = trigger.getAttribute('data-preview-target-id');"
-    , "    const target = targetId ? document.getElementById(targetId) : null;"
-    , "    if (!target || !content.contains(target)) return null;"
-    , "    const template = document.createElement('div');"
-    , "    template.className = 'reference-preview-template';"
-    , "    const heading = document.createElement('div');"
-    , "    heading.className = 'reference-preview-heading';"
-    , "    const kind = target.getAttribute('data-preview-kind') || 'Reference';"
-    , "    const label = target.getAttribute('data-preview-label') || targetId;"
-    , "    const title = target.getAttribute('data-preview-title');"
-    , "    heading.append(document.createTextNode(kind + ' '));"
-    , "    const code = document.createElement('code');"
-    , "    code.textContent = label;"
-    , "    heading.append(code);"
-    , "    if (title) {"
-    , "      heading.append(document.createTextNode(' (' + title + ')'));"
-    , "    }"
-    , "    template.append(heading);"
-    , "    const body = document.createElement('div');"
-    , "    body.className = 'reference-preview-body';"
-    , "    const statement = document.createElement('div');"
-    , "    statement.className = 'reference-preview-statement';"
-    , "    const head = Array.from(target.children).find((child) => child.localName === 'head-');"
-    , "    const nodes = Array.from(target.childNodes);"
-    , "    const start = head ? nodes.indexOf(head) + 1 : 0;"
-    , "    for (const node of nodes.slice(start)) {"
-    , "      statement.append(node.cloneNode(true));"
-    , "    }"
-    , "    if (!statement.childNodes.length) return null;"
-    , "    body.append(statement);"
-    , "    template.append(body);"
-    , "    return template;"
-    , "  };"
-    , ""
-    , "  const buildMissingPreview = (item) => {"
-    , "    const label = item.getAttribute('data-reference-label') || '';"
-    , "    const template = document.createElement('div');"
-    , "    template.className = 'reference-preview-template';"
-    , "    const heading = document.createElement('div');"
-    , "    heading.className = 'reference-preview-heading';"
-    , "    heading.append(document.createTextNode('Reference '));"
-    , "    const code = document.createElement('code');"
-    , "    code.textContent = label;"
-    , "    heading.append(code);"
-    , "    template.append(heading);"
-    , "    const body = document.createElement('div');"
-    , "    body.className = 'reference-preview-body';"
-    , "    const statement = document.createElement('p');"
-    , "    statement.className = 'reference-preview-statement';"
-    , "    statement.textContent = 'Preview unavailable.';"
-    , "    body.append(statement);"
-    , "    template.append(body);"
-    , "    return template;"
-    , "  };"
-    , ""
-    , "  const linkGroupHeading = (item, template) => {"
-    , "    const href = item.getAttribute('data-preview-link');"
-    , "    if (!href) return template;"
-    , "    const heading = template.querySelector('.reference-preview-heading');"
-    , "    const code = heading ? heading.querySelector('code') : null;"
-    , "    if (!heading || !code || code.closest('a')) return template;"
-    , "    const link = document.createElement('a');"
-    , "    link.href = href;"
-    , "    link.append(code.cloneNode(true));"
-    , "    code.replaceWith(link);"
-    , "    return template;"
-    , "  };"
-    , ""
-    , "  const buildGroupPreview = (trigger) => {"
-    , "    if (!trigger.hasAttribute('data-preview-group')) return null;"
-    , "    const items = Array.from(trigger.querySelectorAll('.reference-preview-group-items > [data-reference-label]'));"
-    , "    if (!items.length) return null;"
-    , "    const template = document.createElement('div');"
-    , "    template.className = 'reference-preview-group-template';"
-    , "    for (const item of items) {"
-    , "      const preview = cloneHiddenPreview(item) || buildCurrentPreview(item) || buildMissingPreview(item);"
-    , "      template.append(linkGroupHeading(item, preview));"
-    , "    }"
-    , "    return template;"
-    , "  };"
-    , ""
-    , "  const previewFor = (trigger) => buildGroupPreview(trigger) || cloneHiddenPreview(trigger) || buildCurrentPreview(trigger);"
-    , ""
-    , "  const clamp = (value, min, max) => Math.min(Math.max(value, min), max);"
-    , "  const findTrigger = (target) => target instanceof Element ? target.closest('[data-preview-group], [data-preview-id], [data-preview-target-id]') : null;"
-    , "  const clearHideTimer = () => {"
-    , "    if (!hideTimer) return;"
-    , "    window.clearTimeout(hideTimer);"
-    , "    hideTimer = 0;"
-    , "  };"
-    , ""
-    , "  const hidePreview = () => {"
-    , "    clearHideTimer();"
-    , "    activeTrigger = null;"
-    , "    lastPointer = null;"
-    , "    isPinned = false;"
-    , "    popup.classList.remove('is-visible');"
-    , "    popup.setAttribute('aria-hidden', 'true');"
-    , "    popup.replaceChildren();"
-    , "  };"
-    , ""
-    , "  const scheduleHide = () => {"
-    , "    if (isPinned) return;"
-    , "    clearHideTimer();"
-    , "    hideTimer = window.setTimeout(() => {"
-    , "      hideTimer = 0;"
-    , "      if (!isPinned) hidePreview();"
-    , "    }, hideDelay);"
-    , "  };"
-    , ""
-    , "  const placePreview = () => {"
-    , "    if (!activeTrigger) return;"
-    , "    const triggerRect = activeTrigger.getBoundingClientRect();"
-    , "    const popupRect = popup.getBoundingClientRect();"
-    , "    const fallbackWidth = Math.min(704, Math.max(0, window.innerWidth - margin * 2));"
-    , "    const popupWidth = popupRect.width || fallbackWidth;"
-    , "    const popupHeight = popupRect.height || 0;"
-    , "    const pointer = lastPointer;"
-    , "    const anchorX = pointer ? pointer.clientX : triggerRect.left;"
-    , "    const anchorY = pointer ? pointer.clientY : triggerRect.bottom;"
-    , "    let left = anchorX + (pointer ? offset : 0);"
-    , "    let top = anchorY + offset;"
-    , "    if (top + popupHeight + margin > window.innerHeight) {"
-    , "      const upperAnchor = pointer ? pointer.clientY : triggerRect.top;"
-    , "      top = Math.max(margin, upperAnchor - popupHeight - offset);"
-    , "    }"
-    , "    left = clamp(left, margin, Math.max(margin, window.innerWidth - popupWidth - margin));"
-    , "    popup.style.left = `${left}px`;"
-    , "    popup.style.top = `${top}px`;"
-    , "  };"
-    , ""
-    , "  const showPreview = (trigger, pointerEvent, pinned = false) => {"
-    , "    const source = previewFor(trigger);"
-    , "    if (!source) {"
-    , "      hidePreview();"
-    , "      return;"
-    , "    }"
-    , "    const wasPinned = isPinned && trigger === activeTrigger;"
-    , "    clearHideTimer();"
-    , "    activeTrigger = trigger;"
-    , "    lastPointer = pointerEvent ? { clientX: pointerEvent.clientX, clientY: pointerEvent.clientY } : null;"
-    , "    isPinned = pinned || wasPinned;"
-    , "    popup.replaceChildren(source);"
-    , "    popup.scrollTop = 0;"
-    , "    popup.setAttribute('aria-hidden', 'false');"
-    , "    popup.classList.add('is-visible');"
-    , "    placePreview();"
-    , "  };"
-    , ""
-    , "  content.addEventListener('pointerover', (event) => {"
-    , "    const trigger = findTrigger(event.target);"
-    , "    if (!trigger || !content.contains(trigger) || trigger === activeTrigger) return;"
-    , "    showPreview(trigger, event);"
-    , "  });"
-    , ""
-    , "  content.addEventListener('pointermove', (event) => {"
-    , "    const trigger = findTrigger(event.target);"
-    , "    if (!trigger || trigger !== activeTrigger) return;"
-    , "    if (isPinned) return;"
-    , "    lastPointer = { clientX: event.clientX, clientY: event.clientY };"
-    , "    placePreview();"
-    , "  });"
-    , ""
-    , "  content.addEventListener('pointerout', (event) => {"
-    , "    const trigger = findTrigger(event.target);"
-    , "    if (!trigger || trigger !== activeTrigger) return;"
-    , "    if (isPinned) return;"
-    , "    const related = event.relatedTarget;"
-    , "    if (related instanceof Node && trigger.contains(related)) return;"
-    , "    if (related instanceof Node && popup.contains(related)) return;"
-    , "    scheduleHide();"
-    , "  });"
-    , ""
-    , "  content.addEventListener('focusin', (event) => {"
-    , "    const trigger = findTrigger(event.target);"
-    , "    if (!trigger || !content.contains(trigger)) return;"
-    , "    showPreview(trigger, null);"
-    , "  });"
-    , ""
-    , "  content.addEventListener('focusout', (event) => {"
-    , "    const trigger = findTrigger(event.target);"
-    , "    if (trigger && trigger === activeTrigger && !isPinned) scheduleHide();"
-    , "  });"
-    , ""
-    , "  content.addEventListener('click', (event) => {"
-    , "    const trigger = findTrigger(event.target);"
-    , "    if (!trigger || !trigger.hasAttribute('data-preview-group') || !content.contains(trigger)) return;"
-    , "    event.preventDefault();"
-    , "    showPreview(trigger, event, true);"
-    , "  });"
-    , ""
-    , "  popup.addEventListener('pointerenter', clearHideTimer);"
-    , "  popup.addEventListener('pointerleave', scheduleHide);"
-    , ""
-    , "  document.addEventListener('click', (event) => {"
-    , "    if (!isPinned) return;"
-    , "    const target = event.target;"
-    , "    if (target instanceof Node && popup.contains(target)) return;"
-    , "    if (activeTrigger && target instanceof Node && activeTrigger.contains(target)) return;"
-    , "    hidePreview();"
-    , "  });"
-    , ""
-    , "  content.addEventListener('scroll', hidePreview, { passive: true });"
-    , "  window.addEventListener('resize', hidePreview);"
-    , "  window.addEventListener('hashchange', hidePreview);"
-    , "  document.addEventListener('keydown', (event) => {"
-    , "    if (event.key === 'Escape') {"
-    , "      hidePreview();"
-    , "      return;"
-    , "    }"
-    , "    if (event.key !== 'Enter' && event.key !== ' ') return;"
-    , "    const trigger = findTrigger(document.activeElement);"
-    , "    if (!trigger || !trigger.hasAttribute('data-preview-group')) return;"
-    , "    event.preventDefault();"
-    , "    showPreview(trigger, null, true);"
-    , "  });"
-    , "})();"
-    ]
-
-collectReferencedMarkersOfBlock :: Block -> Set Marker
-collectReferencedMarkersOfBlock =
-    collectBlock
-  where
-        collectBlock :: Block -> Set Marker
-        collectBlock = \case
-            BlockProof _start proof _end ->
-                collectProof proof
-            _ ->
-                mempty
-
-        collectProof :: Proof -> Set Marker
-        collectProof = \case
-            Omitted _loc ->
-                mempty
-            Qed _loc justification ->
-                collectJustification justification
-            Contradiction _loc justification ->
-                collectJustification justification
-            ByCase _loc cases ->
-                foldMap collectCase cases
-            ByContradiction _loc proof ->
-                collectProof proof
-            BySetInduction _loc _term proof ->
-                collectProof proof
-            ByOrdInduction _loc proof ->
-                collectProof proof
-            Assume _loc _stmt proof ->
-                collectProof proof
-            FixSymbolic _loc _vars _bound proof ->
-                collectProof proof
-            FixSuchThat _loc _vars _stmt proof ->
-                collectProof proof
-            Calc _loc _maybeQuant calc proof ->
-                collectCalc calc <> collectProof proof
-            TakeVar _loc _vars _bound _stmt justification proof ->
-                collectJustification justification <> collectProof proof
-            TakeNoun _loc _np justification proof ->
-                collectJustification justification <> collectProof proof
-            Have _loc _maybeStmt _stmt justification proof ->
-                collectJustification justification <> collectProof proof
-            Suffices _loc _stmt justification proof ->
-                collectJustification justification <> collectProof proof
-            Subclaim _loc _stmt subproof proof ->
-                collectProof subproof <> collectProof proof
-            Define _loc _var _expr proof ->
-                collectProof proof
-            DefineFunction _loc _fun _arg _value _boundVar _boundExpr proof ->
-                collectProof proof
-            DefineFunctionLocal _loc _fun _arg _target _domVar _codVar _rules proof ->
-                collectProof proof
-
-        collectCase :: Case -> Set Marker
-        collectCase Case{caseProof} =
-            collectProof caseProof
-
-        collectCalc :: Calc -> Set Marker
-        collectCalc = \case
-            Equation _expr steps ->
-                foldMap (collectJustification . snd) steps
-            Biconditionals _formula steps ->
-                foldMap (collectJustification . snd) steps
-
-        collectJustification :: Justification -> Set Marker
-        collectJustification = \case
-            JustificationRef markers ->
-                Set.fromList (toList markers)
-            JustificationSetExt ->
-                mempty
-            JustificationEmpty ->
-                mempty
-            JustificationLocal ->
-                mempty
-
-collectMissingHints :: HintMap -> [Block] -> MissingHintMap
-collectMissingHints hints = foldMap collectBlock
-    where
-        noteMissingHint :: HintCategory -> Marker -> Int -> MissingHintMap
-        noteMissingHint category marker arity =
-            if Map.member (category, marker, arity) hints
-                then mempty
-                else MissingHintMap (Map.singleton category (Set.singleton marker))
-
-        collectBlock :: Block -> MissingHintMap
-        collectBlock = \case
-            BlockAxiom _loc _title _marker axiom ->
-                collectAxiom axiom
-            BlockClaim _kind _loc _title _marker claim ->
-                collectClaim claim
-            BlockProof _start proof _end ->
-                collectProof proof
-            BlockDefn _loc _title _marker defn ->
-                collectDefn defn
-            BlockAbbr _loc _title _marker abbr ->
-                collectAbbreviation abbr
-            BlockData _loc _title _marker datatype ->
-                collectDatatype datatype
-            BlockInductive _loc _title _marker ind ->
-                collectInductive ind
-            BlockSig _loc _title _marker asms sig ->
-                collectAsms asms
-                    <> collectSignature sig
-            BlockStruct _loc _title _marker structDefn ->
-                collectStructDefn structDefn
-
-        collectAxiom :: Axiom -> MissingHintMap
-        collectAxiom (Axiom asms stmt) =
-            collectAsms asms <> collectStmt stmt
-
-        collectClaim :: Claim -> MissingHintMap
-        collectClaim (Claim asms stmt) =
-            collectAsms asms <> collectStmt stmt
-
-        collectDefn :: Defn -> MissingHintMap
-        collectDefn = \case
-            Defn asms defnHead stmt ->
-                collectAsms asms
-                    <> collectDefnHead defnHead
-                    <> collectStmt stmt
-            DefnFun asms _fun maybeTerm resultTerm ->
-                collectAsms asms
-                    <> foldMap collectTerm maybeTerm
-                    <> collectTerm resultTerm
-            DefnOp symb expr ->
-                collectSymbolPattern symb
-                    <> collectExpr expr
-
-        collectDefnHead :: DefnHead -> MissingHintMap
-        collectDefnHead = \case
-            DefnAdj maybeNp _var _adj ->
-                foldMap collectNounPhraseMaybe maybeNp
-            DefnVerb maybeNp _var _verb ->
-                foldMap collectNounPhraseMaybe maybeNp
-            DefnNoun _var noun ->
-                collectVarNoun noun
-            DefnSymbolicPredicate _predi marker vars ->
-                noteMissingHint PredicateHint marker (length vars)
-                    <> foldMap (collectExpr . ExprVar) vars
-            DefnRel _x rel params _y ->
-                noteMissingHint RelationHint (relationSymbolMarker rel) (length params)
-
-        collectAbbreviation :: Abbreviation -> MissingHintMap
-        collectAbbreviation = \case
-            AbbreviationAdj _var _adj stmt ->
-                collectStmt stmt
-            AbbreviationVerb _var _verb stmt ->
-                collectStmt stmt
-            AbbreviationNoun _var _noun stmt ->
-                collectStmt stmt
-            AbbreviationRel _x rel params _y stmt ->
-                noteMissingHint RelationHint (relationSymbolMarker rel) (length params)
-                    <> collectStmt stmt
-            AbbreviationFun _fun bodyTerm ->
-                collectTerm bodyTerm
-            AbbreviationEq symb expr ->
-                collectSymbolPattern symb
-                    <> collectExpr expr
-
-        collectDatatype :: Datatype -> MissingHintMap
-        collectDatatype Datatype{..} =
-            collectExpr datatypeHeadExpr
-                <> foldMap collectDatatypeClause datatypeClauses
-
-        collectDatatypeClause :: DatatypeClause -> MissingHintMap
-        collectDatatypeClause DatatypeClause{..} =
-            collectExpr datatypeClauseConstructorExpr
-                <> collectExpr datatypeClauseTargetExpr
-                <> foldMap (collectExpr . snd) datatypeClausePremises
-
-        collectInductive :: Inductive -> MissingHintMap
-        collectInductive Inductive{..} =
-            collectSymbolPattern inductiveSymbolPattern
-                <> collectExpr inductiveDomain
-                <> foldMap collectIntroRule inductiveIntros
-
-        collectIntroRule :: IntroRule -> MissingHintMap
-        collectIntroRule IntroRule{..} =
-            foldMap collectFormula introConditions
-                <> collectFormula introResult
-
-        collectSignature :: Signature -> MissingHintMap
-        collectSignature = \case
-            SignatureAdj _var adj ->
-                collectVarAdj adj
-            SignatureVerb _var verb ->
-                collectVarVerb verb
-            SignatureNoun _var noun ->
-                collectVarNoun noun
-            SignatureSymbolic symb np ->
-                collectSymbolPattern symb
-                    <> collectNounPhraseMaybe np
-
-        collectStructDefn :: StructDefn -> MissingHintMap
-        collectStructDefn StructDefn{structAssumes} =
-            foldMap (collectStmt . snd) structAssumes
-
-        collectProof :: Proof -> MissingHintMap
-        collectProof = \case
-            Omitted _loc ->
-                mempty
-            Qed{} ->
-                mempty
-            Contradiction{} ->
-                mempty
-            ByCase _loc cases ->
-                foldMap collectCase cases
-            ByContradiction _loc proof ->
-                collectProof proof
-            BySetInduction _loc maybeTerm proof ->
-                foldMap collectTerm maybeTerm
-                    <> collectProof proof
-            ByOrdInduction _loc proof ->
-                collectProof proof
-            Assume _loc stmt proof ->
-                collectStmt stmt
-                    <> collectProof proof
-            FixSymbolic _loc _vars bound proof ->
-                collectBound bound
-                    <> collectProof proof
-            FixSuchThat _loc _vars stmt proof ->
-                collectStmt stmt
-                    <> collectProof proof
-            Calc _loc maybeQuant calc proof ->
-                foldMap collectCalcQuantifier maybeQuant
-                    <> collectCalc calc
-                    <> collectProof proof
-            TakeVar _loc _vars bound stmt _justification proof ->
-                collectBound bound
-                    <> collectStmt stmt
-                    <> collectProof proof
-            TakeNoun _loc np _justification proof ->
-                collectNounPhraseList np
-                    <> collectProof proof
-            Have _loc maybeStmt stmt _justification proof ->
-                foldMap collectStmt maybeStmt
-                    <> collectStmt stmt
-                    <> collectProof proof
-            Suffices _loc stmt _justification proof ->
-                collectStmt stmt
-                    <> collectProof proof
-            Subclaim _loc stmt subproof proof ->
-                collectStmt stmt
-                    <> collectProof subproof
-                    <> collectProof proof
-            Define _loc _var expr proof ->
-                collectExpr expr
-                    <> collectProof proof
-            DefineFunction _loc _fun _arg value _boundVar boundExpr proof ->
-                collectExpr value
-                    <> collectExpr boundExpr
-                    <> collectProof proof
-            DefineFunctionLocal _loc _fun _arg _target _domVar _codVar rules proof ->
-                foldMap collectLocalFunctionRule rules
-                    <> collectProof proof
-
-        collectLocalFunctionRule :: (Expr, Formula) -> MissingHintMap
-        collectLocalFunctionRule (ruleTerm, formula) =
-            collectExpr ruleTerm
-                <> collectFormula formula
-
-        collectCase :: Case -> MissingHintMap
-        collectCase Case{caseOf, caseProof} =
-            collectStmt caseOf
-                <> collectProof caseProof
-
-        collectCalcQuantifier :: CalcQuantifier -> MissingHintMap
-        collectCalcQuantifier (CalcQuantifier _vars bound maybeStmt) =
-            collectBound bound
-                <> foldMap collectStmt maybeStmt
-
-        collectCalc :: Calc -> MissingHintMap
-        collectCalc = \case
-            Equation expr steps ->
-                collectExpr expr
-                    <> foldMap (collectExpr . fst) steps
-            Biconditionals phi steps ->
-                collectFormula phi
-                    <> foldMap (collectFormula . fst) steps
-
-        collectStmt :: Stmt -> MissingHintMap
-        collectStmt = \case
-            StmtFormula phi ->
-                collectFormula phi
-            StmtVerbPhrase terms verbPhrase ->
-                collectTerms terms
-                    <> collectVerbPhrase verbPhrase
-            StmtNoun terms np ->
-                collectTerms terms
-                    <> collectNounPhraseMaybe np
-            StmtStruct stmtTerm _structPhrase ->
-                collectTerm stmtTerm
-            StmtNeg _loc stmt ->
-                collectStmt stmt
-            StmtExists _loc np ->
-                collectNounPhraseList np
-            StmtConnected _conn _loc stmt1 stmt2 ->
-                collectStmt stmt1
-                    <> collectStmt stmt2
-            StmtQuantPhrase _loc qp stmt ->
-                collectQuantPhrase qp
-                    <> collectStmt stmt
-            SymbolicQuantified _loc _quant _vars bound suchThat stmt ->
-                collectBound bound
-                    <> foldMap collectStmt suchThat
-                    <> collectStmt stmt
-
-        collectQuantPhrase :: QuantPhrase -> MissingHintMap
-        collectQuantPhrase (QuantPhrase _quant np) =
-            collectNounPhraseList np
-
-        collectAsm :: Asm -> MissingHintMap
-        collectAsm = \case
-            AsmSuppose stmt ->
-                collectStmt stmt
-            AsmLetNoun _vars np ->
-                collectNounPhraseMaybe np
-            AsmLetIn _vars expr ->
-                collectExpr expr
-            AsmLetThe _var fun ->
-                collectFun fun
-            AsmLetEq _var expr ->
-                collectExpr expr
-            AsmLetStruct{} ->
-                mempty
-
-        collectTerm :: Term -> MissingHintMap
-        collectTerm = \case
-            TermExpr expr ->
-                collectExpr expr
-            TermFun fun ->
-                collectFun fun
-            TermIota _loc _var stmt ->
-                collectStmt stmt
-            TermQuantified _quant _loc np ->
-                collectNounPhraseMaybe np
-
-        collectNounPhraseMaybe :: NounPhrase Maybe -> MissingHintMap
-        collectNounPhraseMaybe (NounPhrase ls noun _maybeName rs maybeSuchThat) =
-            collectAdjLs ls
-                <> collectNoun noun
-                <> collectAdjRs rs
-                <> foldMap collectStmt maybeSuchThat
-
-        collectNounPhraseList :: NounPhrase [] -> MissingHintMap
-        collectNounPhraseList (NounPhrase ls noun _names rs maybeSuchThat) =
-            collectAdjLs ls
-                <> collectNoun noun
-                <> collectAdjRs rs
-                <> foldMap collectStmt maybeSuchThat
-
-        collectAdjL :: AdjLOf Term -> MissingHintMap
-        collectAdjL (AdjL _loc _item args) =
-            collectTerms args
-
-        collectAdjR :: AdjROf Term -> MissingHintMap
-        collectAdjR = \case
-            AdjR _loc _item args ->
-                collectTerms args
-            AttrRThat verbPhrase ->
-                collectVerbPhrase verbPhrase
-
-        collectAdj :: AdjOf Term -> MissingHintMap
-        collectAdj (Adj _loc _item args) =
-            collectTerms args
-
-        collectVarAdj :: AdjOf VarSymbol -> MissingHintMap
-        collectVarAdj _adj =
-            mempty
-
-        collectVerb :: VerbOf Term -> MissingHintMap
-        collectVerb (Verb _loc _item args) =
-            collectTerms args
-
-        collectVarVerb :: VerbOf VarSymbol -> MissingHintMap
-        collectVarVerb _verb =
-            mempty
-
-        collectVerbPhrase :: VerbPhrase -> MissingHintMap
-        collectVerbPhrase = \case
-            VPVerb verb ->
-                collectVerb verb
-            VPAdj adjs ->
-                foldMap collectAdj adjs
-            VPVerbNot verb ->
-                collectVerb verb
-            VPAdjNot adjs ->
-                foldMap collectAdj adjs
-
-        collectNoun :: NounOf Term -> MissingHintMap
-        collectNoun (Noun _loc _item args) =
-            collectTerms args
-
-        collectVarNoun :: NounOf VarSymbol -> MissingHintMap
-        collectVarNoun _noun =
-            mempty
-
-        collectFun :: FunOf Term -> MissingHintMap
-        collectFun Fun{funArgs} =
-            collectTerms funArgs
-
-        collectBound :: Bound -> MissingHintMap
-        collectBound = \case
-            Unbounded ->
-                mempty
-            Bounded _loc _sign rel expr ->
-                collectRelation rel
-                    <> collectExpr expr
-
-        collectFormula :: Formula -> MissingHintMap
-        collectFormula = \case
-            FormulaChain chain ->
-                collectChain chain
-            FormulaPredicate _loc _predi marker exprs ->
-                noteMissingHint PredicateHint marker (length exprs)
-                    <> collectExprs exprs
-            Connected _loc _conn phi psi ->
-                collectFormula phi
-                    <> collectFormula psi
-            FormulaNeg _loc phi ->
-                collectFormula phi
-            FormulaQuantified _loc _quant _vars bound phi ->
-                collectBound bound
-                    <> collectFormula phi
-            PropositionalConstant{} ->
-                mempty
-
-        collectChain :: Chain -> MissingHintMap
-        collectChain = \case
-            ChainBase lhs _sign rel rhs ->
-                collectExprs lhs
-                    <> collectRelation rel
-                    <> collectExprs rhs
-            ChainCons lhs _sign rel chain ->
-                collectExprs lhs
-                    <> collectRelation rel
-                    <> collectChain chain
-
-        collectRelation :: Relation -> MissingHintMap
-        collectRelation = \case
-            Relation _loc symbol relParams ->
-                noteMissingHint RelationHint (relationSymbolMarker symbol) (length relParams)
-                    <> collectExprs relParams
-            RelationExpr _loc expr ->
-                collectExpr expr
-
-        collectExpr :: Expr -> MissingHintMap
-        collectExpr = \case
-            ExprVar{} ->
-                mempty
-            ExprInteger{} ->
-                mempty
-            ExprOp _loc item args ->
-                noteMissingHint OperatorHint (mixfixMarker item) (length args)
-                    <> collectExprs args
-            ExprStructOp _loc symb maybeExpr ->
-                noteMissingHint StructOpHint (structMarker symb) (length (maybeToList maybeExpr))
-                    <> foldMap collectExpr maybeExpr
-            ExprFiniteSet _loc exprs ->
-                collectExprs exprs
-            ExprSep _loc _var boundExpr stmt ->
-                collectExpr boundExpr
-                    <> collectStmt stmt
-            ExprReplace _loc expr bounds maybeStmt ->
-                collectExpr expr
-                    <> foldMap (collectExpr . snd) bounds
-                    <> foldMap collectStmt maybeStmt
-            ExprReplacePred _loc _rangeVar _domVar domExpr stmt ->
-                collectExpr domExpr
-                    <> collectStmt stmt
-
-        collectSymbolPattern :: SymbolPattern -> MissingHintMap
-        collectSymbolPattern (SymbolPattern symbol vars) =
-            noteMissingHint OperatorHint (mixfixMarker symbol) (length vars)
-
-        collectAsms :: [Asm] -> MissingHintMap
-        collectAsms =
-            foldMap collectAsm
-
-        collectTerms :: Foldable t => t Term -> MissingHintMap
-        collectTerms =
-            foldMap collectTerm
-
-        collectAdjLs :: [AdjLOf Term] -> MissingHintMap
-        collectAdjLs =
-            foldMap collectAdjL
-
-        collectAdjRs :: [AdjROf Term] -> MissingHintMap
-        collectAdjRs =
-            foldMap collectAdjR
-
-        collectExprs :: Foldable t => t Expr -> MissingHintMap
-        collectExprs =
-            foldMap collectExpr
-
-formatMissingHintWarning :: MissingHintMap -> Maybe Text
-formatMissingHintWarning missingHints
-    | null parts = Nothing
-    | otherwise = Just ("WARNING: missing render hints: " <> Text.intercalate "; " parts)
-    where
-        missingHintMap = unMissingHintMap missingHints
-
-        parts =
-            [ label <> "(" <> Text.intercalate ", " (markerText <$> Set.toAscList markers) <> ")"
-            | (category, label) <- categoryLabels
-            , Just markers <- [Map.lookup category missingHintMap]
-            , not (Set.null markers)
-            ]
-
-        categoryLabels :: [(HintCategory, Text)]
-        categoryLabels =
-            [ (OperatorHint, "operators")
-            , (RelationHint, "relations")
-            , (PredicateHint, "predicates")
-            , (StructOpHint, "structops")
-            ]
-
-
-parseHints :: Text -> HintMap
-parseHints source = Map.fromList (parseLine <$> zip [1 :: Int ..] relevantLines)
-    where
-        relevantLines = [line | line <- Text.lines source, not (Text.all isSpace line)]
-
-        parseLine :: (Int, Text) -> ((HintCategory, Marker, Int), RenderHint)
-        parseLine (lineNo, line) = case Text.splitOn "\t" line of
-            [categoryText, markerName, arityText, templateText] ->
-                let category = parseCategory lineNo categoryText
-                    marker = Marker markerName
-                    arity = parseArity lineNo arityText
-                    template = parseTemplate lineNo templateText
-                in ((category, marker, arity), RenderHint arity template)
-            _ ->
-                error ("Malformed render hint at line " <> show lineNo <> ": expected exactly 4 tab-separated columns")
-
-parseCategory :: Int -> Text -> HintCategory
-parseCategory lineNo = \case
-    "operator" -> OperatorHint
-    "relation" -> RelationHint
-    "predicate" -> PredicateHint
-    "structop" -> StructOpHint
-    other -> error ("Unknown render hint category at line " <> show lineNo <> ": " <> Text.unpack other)
-
-parseArity :: Int -> Text -> Int
-parseArity lineNo text = case reads (Text.unpack text) of
-    [(n, "")] -> n
-    _ -> error ("Malformed render-hint arity at line " <> show lineNo <> ": " <> Text.unpack text)
-
-parseTemplate :: Int -> Text -> [TemplatePiece]
-parseTemplate lineNo template = reverse (flush mempty (go mempty [] template))
-    where
-        go :: Text -> [TemplatePiece] -> Text -> [TemplatePiece]
-        go literal acc rest = case parseSlot rest of
-            Just (slot, rest') ->
-                go mempty (Slot slot : flush literal acc) rest'
-            Nothing -> case Text.uncons rest of
-                Nothing -> flush literal acc
-                Just (c, rest') -> go (Text.snoc literal c) acc rest'
-
-        flush :: Text -> [TemplatePiece] -> [TemplatePiece]
-        flush literal acc
-            | Text.null literal = acc
-            | otherwise = Literal literal : acc
-
-        parseSlot :: Text -> Maybe (Int, Text)
-        parseSlot text = do
-            text' <- Text.stripPrefix "<x" text
-            (digit, rest) <- Text.uncons text'
-            guard (isDigit digit)
-            rest' <- Text.stripPrefix "/>" rest
-            let slot = digitToInt digit
-            guard (slot > 0 && slot <= 9)
-            pure (slot, rest')
-
-        _unusedLineNo = lineNo
-
-
-renderBlock :: HintMap -> ReferenceContext -> BlockRenderInfo -> Html ()
-renderBlock hints references (_index, block, blockId) = case block of
-    BlockAxiom _loc title marker axiom ->
-        renderCustomBlock blockId "axiom-" "Axiom" (Just marker) title (renderAxiom hints axiom)
-    BlockClaim kind _loc title marker claim ->
-        renderCustomBlock blockId (claimKindElement kind) (claimKindPrefix kind) (Just marker) title (renderClaim hints claim)
-    BlockProof _start proof _end ->
-        renderProofBlock hints references proof
-    BlockDefn _loc title marker defn ->
-        renderCustomBlock blockId "definition-" "Definition" (Just marker) title (renderDefn hints defn)
-    BlockAbbr _loc title marker abbr ->
-        renderCustomBlock blockId "abbreviation-" "Abbreviation" (Just marker) title (renderAbbreviation hints abbr)
-    BlockData _loc title marker datatype ->
-        renderCustomBlock blockId "datatype-" "Datatype" (Just marker) title (renderDatatype hints datatype)
-    BlockInductive _loc title marker ind ->
-        renderCustomBlock blockId "inductive-" "Inductive" (Just marker) title (renderInductive hints marker ind)
-    BlockSig _loc title marker asms sig ->
-        renderCustomBlock blockId "signature-" "Signature" (Just marker) title (renderSignatureBlock hints asms sig)
-    BlockStruct _loc title marker structDefn ->
-        renderCustomBlock blockId "struct-" "Structure" (Just marker) title (renderStructDefn hints structDefn)
-
-renderTocEntry :: (Int, Text, Block) -> Html ()
-renderTocEntry (index, blockId, block) =
-    li_ do
-        a_ [href_ (renderUrlFragment blockId)] do
-            span_ (toHtml (blockPrefixText block))
-            case formatMarker (blockMarkerOf block) of
-                Nothing ->
-                    when (blockNeedsIndexLabel block) do
-                        code_ (toHtml (Text.pack (show index)))
-                Just marker ->
-                    code_ (toHtml marker)
-
-includeInToc :: Block -> Bool
-includeInToc = \case
-    BlockProof{} -> False
-    _ -> True
-
-renderCustomBlock :: Text -> Text -> Text -> Maybe Marker -> Maybe BlockTitle -> Html () -> Html ()
-renderCustomBlock blockId name prefix mmarker mtitle body =
-    term name (id_ blockId : previewTargetAttributes prefix mmarker mtitle) do
-        renderBlockLead prefix mmarker mtitle True
-        body
-
-previewTargetAttributes :: Text -> Maybe Marker -> Maybe BlockTitle -> [Attributes]
-previewTargetAttributes prefix mmarker mtitle =
-    case formatMarker mmarker of
-        Nothing ->
-            []
-        Just marker ->
-            [ makeAttributes "data-preview-kind" prefix
-            , makeAttributes "data-preview-label" marker
-            ]
-            <> case formatBlockTitle mtitle of
-                Nothing ->
-                    []
-                Just title ->
-                    [makeAttributes "data-preview-title" title]
-
-renderProofBlock :: HintMap -> ReferenceContext -> Proof -> Html ()
-renderProofBlock hints references proof
-    | proofStepCount proof >= proofCollapseThreshold =
-        term "proof-" do
-            details_ do
-                summary_ (renderBlockLead "Proof" Nothing Nothing False)
-                renderProof hints references proof
-    | otherwise =
-        term "proof-" do
-            renderBlockLead "Proof" Nothing Nothing True
-            renderProof hints references proof
-
-blockAnchorId :: Int -> Block -> Text
-blockAnchorId index block =
-    case formatMarker (blockMarkerOf block) of
-        Just marker -> marker
-        Nothing -> sanitizeIdFragment (Text.toLower (blockPrefixText block) <> "-" <> Text.pack (show index))
-
-sanitizeIdFragment :: Text -> Text
-sanitizeIdFragment =
-    Text.dropWhile (== '-') . Text.map sanitize . Text.toLower
-    where
-        sanitize c
-            | isAlphaNum c = c
-            | c == '-' || c == '_' = c
-            | otherwise = '-'
-
-blockPrefixText :: Block -> Text
-blockPrefixText = \case
-    BlockAxiom{} -> "Axiom"
-    BlockClaim kind _ _ _ _ -> claimKindPrefix kind
-    BlockProof{} -> "Proof"
-    BlockDefn{} -> "Definition"
-    BlockAbbr{} -> "Abbreviation"
-    BlockData{} -> "Datatype"
-    BlockInductive{} -> "Inductive"
-    BlockSig{} -> "Signature"
-    BlockStruct{} -> "Structure"
-
-blockMarkerOf :: Block -> Maybe Marker
-blockMarkerOf = \case
-    BlockAxiom _ _ marker _ -> Just marker
-    BlockClaim _ _ _ marker _ -> Just marker
-    BlockProof{} -> Nothing
-    BlockDefn _ _ marker _ -> Just marker
-    BlockAbbr _ _ marker _ -> Just marker
-    BlockData _ _ marker _ -> Just marker
-    BlockInductive _ _ marker _ -> Just marker
-    BlockSig _ _ marker _ _ -> Just marker
-    BlockStruct _ _ marker _ -> Just marker
-
-blockTitleOf :: Block -> Maybe BlockTitle
-blockTitleOf = \case
-    BlockAxiom _ title _ _ -> title
-    BlockClaim _ _ title _ _ -> title
-    BlockProof{} -> Nothing
-    BlockDefn _ title _ _ -> title
-    BlockAbbr _ title _ _ -> title
-    BlockData _ title _ _ -> title
-    BlockInductive _ title _ _ -> title
-    BlockSig _ title _ _ _ -> title
-    BlockStruct _ title _ _ -> title
-
-blockNeedsIndexLabel :: Block -> Bool
-blockNeedsIndexLabel block = case (formatMarker (blockMarkerOf block), formatBlockTitle (blockTitleOf block)) of
-    (Nothing, Nothing) -> True
-    _ -> False
-
-renderBlockLead :: Text -> Maybe Marker -> Maybe BlockTitle -> Bool -> Html ()
-renderBlockLead prefix mmarker mtitle withTrailingSpace =
-    term "head-" do
-        toHtml prefix
-        case formatMarker mmarker of
-            Nothing -> skip
-            Just marker ->
-                term "id-" (toHtml marker)
-        case formatBlockTitle mtitle of
-            Nothing ->
-                toHtml ("." <> suffix)
-            Just title -> do
-                toHtml (" (" :: Text)
-                term "title-" (toHtml title)
-                toHtml (")." <> suffix)
-    where
-        suffix :: Text
-        suffix
-            | withTrailingSpace = " "
-            | otherwise = ""
-
-formatMarker :: Maybe Marker -> Maybe Text
-formatMarker = \case
-    Nothing -> Nothing
-    Just marker ->
-        let text = Text.strip (markerText marker)
-        in if Text.null text then Nothing else Just text
-
-formatBlockTitle :: Maybe BlockTitle -> Maybe Text
-formatBlockTitle =
-    fmap capitalizeTitle . nonEmptyTitle
-    where
-        nonEmptyTitle = \case
-            Nothing -> Nothing
-            Just toks ->
-                let text = Text.strip (Text.unwords (tokToText <$> toks))
-                in if Text.null text then Nothing else Just text
-
-capitalizeTitle :: Text -> Text
-capitalizeTitle text = case Text.uncons text of
-    Nothing -> text
-    Just (c, rest) -> Text.cons (toUpper c) rest
-
-claimKindElement :: ClaimKind -> Text
-claimKindElement = \case
-    Proposition -> "proposition-"
-    Theorem -> "theorem-"
-    Lemma -> "lemma-"
-    Corollary -> "corollary-"
-    PlainClaim -> "claim-"
-
-claimKindPrefix :: ClaimKind -> Text
-claimKindPrefix = \case
-    Proposition -> "Proposition"
-    Theorem -> "Theorem"
-    Lemma -> "Lemma"
-    Corollary -> "Corollary"
-    PlainClaim -> "Claim"
-
-
-renderAxiom :: HintMap -> Axiom -> Html ()
-renderAxiom hints (Axiom asms stmt) =
-    renderWithAssumptions hints asms stmt
-
-renderClaim :: HintMap -> Claim -> Html ()
-renderClaim hints (Claim asms stmt) =
-    renderWithAssumptions hints asms stmt
-
-renderWithAssumptions :: HintMap -> [Asm] -> Stmt -> Html ()
-renderWithAssumptions hints asms stmt = do
-    case asms of
-        [] -> renderStmtInline hints stmt
-        _ -> do
-            toHtml ("Suppose " :: Text)
-            renderAsmList hints asms
-            toHtml (". Then " :: Text)
-            renderStmtInline hints stmt
-    toHtml ("." :: Text)
-
-renderDefn :: HintMap -> Defn -> Html ()
-renderDefn hints = \case
-    Defn asms headStmt stmt ->
-        do
-            when (not (null asms)) do
-                toHtml ("If " :: Text)
-                renderAsmList hints asms
-                toHtml (", then " :: Text)
-            renderDefnHead hints headStmt
-            toHtml (" iff " :: Text)
-            renderStmtInline hints stmt
-            toHtml ("." :: Text)
-    DefnFun asms fun maybeSymbol resultTerm ->
-        do
-            when (not (null asms)) do
-                toHtml ("If " :: Text)
-                renderAsmList hints asms
-                toHtml (", then " :: Text)
-            renderFunInline renderVarInline fun
-            case maybeSymbol of
-                Nothing -> skip
-                Just symbolicTerm -> do
-                    toHtml (", " :: Text)
-                    renderTermInline hints symbolicTerm
-            toHtml (" is " :: Text)
-            renderTermInline hints resultTerm
-            toHtml ("." :: Text)
-    DefnOp symb expr ->
-        do
-            inlineMath do
-                renderSymbolPatternMath hints symb
-                moText "="
-                renderExprMathRow hints expr
-            toHtml ("." :: Text)
-
-renderDefnHead :: HintMap -> DefnHead -> Html ()
-renderDefnHead hints = \case
-    DefnAdj maybeNp var adj -> do
-        renderTypedVar hints maybeNp var
-        toHtml (" is " :: Text)
-        renderAdjInline renderVarInline adj
-    DefnVerb maybeNp var verb -> do
-        renderTypedVar hints maybeNp var
-        toHtml (" " :: Text)
-        renderVerbInline False renderVarInline verb
-    DefnNoun var noun -> do
-        renderVarInline var
-        toHtml (" is a " :: Text)
-        renderNounInline False renderVarInline noun
-    DefnSymbolicPredicate predi marker vars ->
-        inlineMath
-            ( renderHintedMathRow
-                hints
-                PredicateHint
-                marker
-                (ExprVar <$> toList vars)
-                (renderPrefixPredicateFallback predi (renderVarMath <$> toList vars))
-            )
-    DefnRel x rel params y ->
-        inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere rel [ExprVar p | p <- params]) [ExprVar y])
-
-renderTypedVar :: HintMap -> Maybe (NounPhrase Maybe) -> VarSymbol -> Html ()
-renderTypedVar hints = \case
-    Nothing -> renderVarInline
-    Just np -> \var -> do
-        renderNounPhraseMaybe hints np
-        toHtml (" " :: Text)
-        renderVarInline var
-
-
-renderAbbreviation :: HintMap -> Abbreviation -> Html ()
-renderAbbreviation hints = \case
-    AbbreviationAdj var adj stmt ->
-        do
-            renderVarInline var
-            toHtml (" is " :: Text)
-            renderAdjInline renderVarInline adj
-            toHtml (" stands for " :: Text)
-            renderStmtInline hints stmt
-            toHtml ("." :: Text)
-    AbbreviationVerb var verb stmt ->
-        do
-            renderVarInline var
-            toHtml (" " :: Text)
-            renderVerbInline False renderVarInline verb
-            toHtml (" stands for " :: Text)
-            renderStmtInline hints stmt
-            toHtml ("." :: Text)
-    AbbreviationNoun var noun stmt ->
-        do
-            renderVarInline var
-            toHtml (" is a " :: Text)
-            renderNounInline False renderVarInline noun
-            toHtml (" stands for " :: Text)
-            renderStmtInline hints stmt
-            toHtml ("." :: Text)
-    AbbreviationRel x rel params y stmt ->
-        do
-            inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere rel [ExprVar p | p <- params]) [ExprVar y])
-            toHtml (" stands for " :: Text)
-            renderStmtInline hints stmt
-            toHtml ("." :: Text)
-    AbbreviationFun fun bodyTerm ->
-        do
-            renderFunInline renderVarInline fun
-            toHtml (" stands for " :: Text)
-            renderTermInline hints bodyTerm
-            toHtml ("." :: Text)
-    AbbreviationEq symb expr ->
-        do
-            renderSymbolPatternInline hints symb
-            toHtml (" stands for " :: Text)
-            inlineMath (renderExprMathRow hints expr)
-            toHtml ("." :: Text)
-
-renderDatatype :: HintMap -> Datatype -> Html ()
-renderDatatype hints Datatype{..} = do
-    toHtml ("Datatype of " :: Text)
-    inlineMath (renderExprMathRow hints datatypeHeadExpr)
-    toHtml ("." :: Text)
-    ul_ do
-        traverse_ renderDatatypeClause (toList datatypeClauses)
-    -- Derived facts require checked semantic context.
-    where
-        renderDatatypeClause :: DatatypeClause -> Html ()
-        renderDatatypeClause DatatypeClause{..} = li_ do
-            inlineMath do
-                renderRelationApplication hints Positive [datatypeClauseConstructorExpr] (Relation Nowhere ElementSymbol []) [datatypeClauseTargetExpr]
-            case datatypeClausePremises of
-                [] ->
-                    toHtml ("." :: Text)
-                premises -> do
-                    toHtml (" for " :: Text)
-                    joinHtml (toHtml (" and " :: Text)) (renderDatatypePremise <$> premises)
-                    toHtml ("." :: Text)
-
-        renderDatatypePremise :: (VarSymbol, Expr) -> Html ()
-        renderDatatypePremise (x, domain) =
-            inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere ElementSymbol []) [domain])
-
-exprVar :: Expr -> Maybe VarSymbol
-exprVar = \case
-    ExprVar x ->
-        Just x
-    _ ->
-        Nothing
-
-substituteExpr :: Map.Map VarSymbol Expr -> Expr -> Expr
-substituteExpr env = \case
-    ExprVar x ->
-        fromMaybe (ExprVar x) (Map.lookup x env)
-    ExprInteger loc n ->
-        ExprInteger loc n
-    ExprOp loc symbol args ->
-        ExprOp loc symbol (substituteExpr env <$> args)
-    ExprStructOp loc symbol expr ->
-        ExprStructOp loc symbol (substituteExpr env <$> expr)
-    ExprFiniteSet loc exprs ->
-        ExprFiniteSet loc (substituteExpr env <$> exprs)
-    ExprSep loc x bound stmt ->
-        ExprSep loc x (substituteExpr env bound) stmt
-    ExprReplace loc expr bounds maybeStmt ->
-        ExprReplace loc (substituteExpr env expr) ((\(x, bound) -> (x, substituteExpr env bound)) <$> bounds) maybeStmt
-    ExprReplacePred loc x y expr stmt ->
-        ExprReplacePred loc x y (substituteExpr env expr) stmt
-
-elementOfFormula :: Expr -> Expr -> Formula
-elementOfFormula left right =
-    FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere ElementSymbol []) (right :| []))
-
-semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula
-semanticSubsetFormula reserved left right =
-    forallIfNeeded [witnessVar]
-        (impliesFormula
-            (elementOfFormula (ExprVar witnessVar) left)
-            (elementOfFormula (ExprVar witnessVar) right))
-    where
-        witnessVar = freshDatatypeVar (reserved <> Set.fromList (exprVars left <> exprVars right)) "x"
-
-equalsFormula :: Expr -> Expr -> Formula
-equalsFormula left right =
-    FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere EqSymbol []) (right :| []))
-
-impliesFormula :: Formula -> Formula -> Formula
-impliesFormula left right =
-    Connected Nowhere Implication left right
-
-formulaConjunction :: [Formula] -> Formula
-formulaConjunction = \case
-    [] ->
-        PropositionalConstant Nowhere IsTop
-    phi : rest ->
-        foldl' (\left right -> Connected Nowhere Conjunction left right) phi rest
-
-formulaDisjunction :: [Formula] -> Formula
-formulaDisjunction = \case
-    [] ->
-        PropositionalConstant Nowhere IsBottom
-    phi : rest ->
-        foldl' (\left right -> Connected Nowhere Disjunction left right) phi rest
-
-forallIfNeeded :: [VarSymbol] -> Formula -> Formula
-forallIfNeeded [] phi = phi
-forallIfNeeded vars phi =
-    FormulaQuantified Nowhere Universally (NonEmpty.fromList vars) Unbounded phi
-
-existsIfNeeded :: [VarSymbol] -> Formula -> Formula
-existsIfNeeded [] phi = phi
-existsIfNeeded vars phi =
-    FormulaQuantified Nowhere Existentially (NonEmpty.fromList vars) Unbounded phi
-
-impliesFrom :: [Formula] -> Formula -> Formula
-impliesFrom [] conclusion = conclusion
-impliesFrom premises conclusion = impliesFormula (formulaConjunction premises) conclusion
-
-freshDatatypeVar :: Set VarSymbol -> Text -> VarSymbol
-freshDatatypeVar used base =
-    List.head
-        [ NamedVar candidate
-        | candidate <- base : [base <> Text.pack (show n) | n <- [(1 :: Int) ..]]
-        , NamedVar candidate `Set.notMember` used
-        ]
-
-renderInductive :: HintMap -> Marker -> Inductive -> Html ()
-renderInductive hints marker Inductive{..} = do
-    toHtml ("Inductive definition of " :: Text)
-    renderSymbolPatternInline hints inductiveSymbolPattern
-    toHtml (" over " :: Text)
-    inlineMath (renderExprMathRow hints inductiveDomain)
-    toHtml ("." :: Text)
-    ul_ do
-        traverse_ renderIntro (toList inductiveIntros)
-    case inductiveDerivedFacts marker Inductive{..} of
-        [] ->
-            skip
-        derivedFacts ->
-            details_ do
-                summary_ (toHtml ("Derived facts" :: Text))
-                ul_ [class_ "inductive-derived-facts"] do
-                    traverse_ (renderInductiveDerivedFact hints) derivedFacts
-    where
-        renderIntro :: IntroRule -> Html ()
-        renderIntro IntroRule{..} = li_ do
-            case introConditions of
-                [] -> skip
-                _ -> do
-                    toHtml ("If " :: Text)
-                    joinHtml (toHtml (" and " :: Text)) (inlineMath . renderFormulaMath hints <$> introConditions)
-                    toHtml (", then " :: Text)
-            inlineMath (renderFormulaMath hints introResult)
-            toHtml ("." :: Text)
-
-renderInductiveDerivedFact :: HintMap -> InductiveDerivedFact -> Html ()
-renderInductiveDerivedFact hints InductiveDerivedFact{inductiveDerivedFactMarker, inductiveDerivedFactFormula} =
-    li_ (id_ (markerText inductiveDerivedFactMarker) : previewTargetAttributes "Inductive Fact" (Just inductiveDerivedFactMarker) Nothing) do
-        term "head-" do
-            code_ (toHtml (markerText inductiveDerivedFactMarker))
-            toHtml (": " :: Text)
-        inlineMath (renderFormulaMath hints inductiveDerivedFactFormula)
-        toHtml ("." :: Text)
-
-data InductiveDerivedFact = InductiveDerivedFact
-    { inductiveDerivedFactMarker :: Marker
-    , inductiveDerivedFactFormula :: Formula
-    }
-
-data InductiveRenderInfo = InductiveRenderInfo
-    { inductiveFactBaseMarker :: Marker
-    , inductiveRenderParams :: [VarSymbol]
-    , inductiveRenderCarrierExpr :: Expr
-    , inductiveRenderDomainExpr :: Expr
-    , inductiveRenderClauses :: NonEmpty InductiveRenderClause
-    }
-
-data InductiveRenderClause = InductiveRenderClause
-    { inductiveRenderClauseVars :: [VarSymbol]
-    , inductiveRenderClauseConditions :: [InductiveRenderCondition]
-    , inductiveRenderClauseResultExpr :: Expr
-    }
-
-data InductiveRenderCondition
-    = InductiveRenderSideCondition Formula
-    | InductiveRenderRecursiveCondition Expr Expr
-
-inductiveDerivedFacts :: Marker -> Inductive -> [InductiveDerivedFact]
-inductiveDerivedFacts marker inductive = case inductiveRenderInfo marker inductive of
-    Nothing ->
-        []
-    Just info ->
-        inductiveIntroFacts info
-            <> [ InductiveDerivedFact (inductiveDomSubsetMarker info) (inductiveDomSubsetFormula info)
-               , InductiveDerivedFact (inductiveCasesMarker info) (inductiveCasesFormula info)
-               , InductiveDerivedFact (inductiveInductMarker info) (inductiveInductFormula info)
-               ]
-
-inductiveRenderInfo :: Marker -> Inductive -> Maybe InductiveRenderInfo
-inductiveRenderInfo marker Inductive{inductiveSymbolPattern = SymbolPattern inductiveSymbol inductiveParams, inductiveDomain, inductiveIntros} = do
-    inductiveRenderClauses <- traverse (inductiveRenderClause inductiveSymbol inductiveParams) inductiveIntros
-    pure InductiveRenderInfo
-        { inductiveFactBaseMarker = marker
-        , inductiveRenderParams = inductiveParams
-        , inductiveRenderCarrierExpr = ExprOp Nowhere inductiveSymbol (ExprVar <$> inductiveParams)
-        , inductiveRenderDomainExpr = inductiveDomain
-        , inductiveRenderClauses
-        }
-    where
-        inductiveRenderClause :: MixfixItem -> [VarSymbol] -> IntroRule -> Maybe InductiveRenderClause
-        inductiveRenderClause symbol params IntroRule{introConditions, introResult} = do
-            inductiveRenderClauseResultExpr <- inductiveRenderResultExpr symbol params introResult
-            inductiveRenderClauseConditions <- traverse (inductiveRenderCondition symbol params) introConditions
-            let paramSet = Set.fromList params
-                inductiveRenderClauseVars =
-                    List.filter (`Set.notMember` paramSet)
-                        (orderedRenderVars (concatMap formulaVars introConditions <> exprVars inductiveRenderClauseResultExpr))
-            pure InductiveRenderClause
-                { inductiveRenderClauseVars
-                , inductiveRenderClauseConditions
-                , inductiveRenderClauseResultExpr
-                }
-
-inductiveRenderResultExpr :: MixfixItem -> [VarSymbol] -> Formula -> Maybe Expr
-inductiveRenderResultExpr symbol params = \case
-    FormulaChain (ChainBase (resultExpr :| []) Positive (Relation _ ElementSymbol []) (carrierExpr :| []))
-        | sameInductiveCarrierExpr symbol params carrierExpr ->
-            Just resultExpr
-    _ ->
-        Nothing
-
-inductiveRenderCondition :: MixfixItem -> [VarSymbol] -> Formula -> Maybe InductiveRenderCondition
-inductiveRenderCondition symbol params phi
-    | not (formulaMentionsFunction symbol phi) =
-        Just (InductiveRenderSideCondition phi)
-    | otherwise = case phi of
-        FormulaChain (ChainBase (recursiveTerm :| []) Positive (Relation _ ElementSymbol []) (recursiveCarrier :| []))
-            | not (exprMentionsFunction symbol recursiveTerm) ->
-                InductiveRenderRecursiveCondition recursiveTerm <$> replaceCarrierExpr symbol params recursiveCarrier
-        _ ->
-            Nothing
-    where
-        replaceCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Maybe Expr
-        replaceCarrierExpr target targetParams =
-            replaceInductiveCarrierExpr target targetParams (ExprVar "__inductive")
-
-inductiveIntroFacts :: InductiveRenderInfo -> [InductiveDerivedFact]
-inductiveIntroFacts info =
-    [ InductiveDerivedFact (inductiveIntroMarker info index) (inductiveIntroFormula info clause)
-    | (index, clause) <- zip [(1 :: Int) ..] (NonEmpty.toList (inductiveRenderClauses info))
-    ]
-
-inductiveIntroMarker :: InductiveRenderInfo -> Int -> Marker
-inductiveIntroMarker info index =
-    Marker (markerText (inductiveFactBaseMarker info) <> "_intro_" <> Text.pack (show index))
-
-inductiveDomSubsetMarker :: InductiveRenderInfo -> Marker
-inductiveDomSubsetMarker info =
-    Marker (markerText (inductiveFactBaseMarker info) <> "_dom_subset")
-
-inductiveCasesMarker :: InductiveRenderInfo -> Marker
-inductiveCasesMarker info =
-    Marker (markerText (inductiveFactBaseMarker info) <> "_cases")
-
-inductiveInductMarker :: InductiveRenderInfo -> Marker
-inductiveInductMarker info =
-    Marker (markerText (inductiveFactBaseMarker info) <> "_induct")
-
-inductiveIntroFormula :: InductiveRenderInfo -> InductiveRenderClause -> Formula
-inductiveIntroFormula info clause =
-    forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> inductiveRenderClauseVars clause))
-        (impliesFrom premises conclusion)
-    where
-        premises = inductiveRenderConditionFormula info <$> inductiveRenderClauseConditions clause
-        conclusion = elementOfFormula (inductiveRenderClauseResultExpr clause) (inductiveRenderCarrierExpr info)
-
-inductiveDomSubsetFormula :: InductiveRenderInfo -> Formula
-inductiveDomSubsetFormula info =
-    forallIfNeeded (inductiveRenderParams info)
-        (semanticSubsetFormula (inductiveUsedVars info) (inductiveRenderCarrierExpr info) (inductiveRenderDomainExpr info))
-
-inductiveCasesFormula :: InductiveRenderInfo -> Formula
-inductiveCasesFormula info =
-    forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> [witnessVar]))
-        (impliesFormula (elementOfFormula (ExprVar witnessVar) (inductiveRenderCarrierExpr info)) (formulaDisjunction disjuncts))
-    where
-        witnessVar = freshDatatypeVar (inductiveUsedVars info) "x"
-        disjuncts = inductiveCaseDisjunct witnessVar <$> NonEmpty.toList (inductiveRenderClauses info)
-        inductiveCaseDisjunct x clause =
-            existsIfNeeded (inductiveRenderClauseVars clause)
-                (formulaConjunction (premises <> [equalsFormula (ExprVar x) (inductiveRenderClauseResultExpr clause)]))
-            where
-                premises = inductiveRenderConditionFormula info <$> inductiveRenderClauseConditions clause
-
-inductiveInductFormula :: InductiveRenderInfo -> Formula
-inductiveInductFormula info =
-    forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> [subsetVar]))
-        (impliesFrom closures conclusion)
-    where
-        subsetVar = freshDatatypeVar (inductiveUsedVars info) "S"
-        closures = inductiveInductionClosure subsetVar <$> NonEmpty.toList (inductiveRenderClauses info)
-        conclusion =
-            semanticSubsetFormula
-                (Set.insert subsetVar (inductiveUsedVars info))
-                (inductiveRenderCarrierExpr info)
-                (ExprVar subsetVar)
-
-inductiveInductionClosure :: VarSymbol -> InductiveRenderClause -> Formula
-inductiveInductionClosure subsetVar clause =
-    forallIfNeeded (inductiveRenderClauseVars clause) (impliesFrom premises conclusion)
-    where
-        premises = inductiveRenderConditionFormulaAt (ExprVar subsetVar) <$> inductiveRenderClauseConditions clause
-        conclusion = elementOfFormula (inductiveRenderClauseResultExpr clause) (ExprVar subsetVar)
-
-inductiveRenderConditionFormula :: InductiveRenderInfo -> InductiveRenderCondition -> Formula
-inductiveRenderConditionFormula info =
-    inductiveRenderConditionFormulaAt (inductiveRenderCarrierExpr info)
-
-inductiveRenderConditionFormulaAt :: Expr -> InductiveRenderCondition -> Formula
-inductiveRenderConditionFormulaAt replacement = \case
-    InductiveRenderSideCondition phi ->
-        phi
-    InductiveRenderRecursiveCondition recursiveTerm recursiveCarrierTemplate ->
-        elementOfFormula recursiveTerm (substituteExpr (Map.singleton "__inductive" replacement) recursiveCarrierTemplate)
-
-inductiveUsedVars :: InductiveRenderInfo -> Set VarSymbol
-inductiveUsedVars info =
-    Set.fromList
-        ( inductiveRenderParams info
-            <> [ var
-               | clause <- NonEmpty.toList (inductiveRenderClauses info)
-               , var <- inductiveRenderClauseVars clause
-               ]
-        )
-
-sameInductiveCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Bool
-sameInductiveCarrierExpr symbol params = \case
-    ExprOp _ symbol' args ->
-        symbol == symbol'
-            && length params == length args
-            && and (zipWith (\param arg -> exprVar arg == Just param) params args)
-    _ ->
-        False
-
-replaceInductiveCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Expr -> Maybe Expr
-replaceInductiveCarrierExpr symbol params replacement = go
-    where
-        go = \case
-            ExprVar x ->
-                Just (ExprVar x)
-            ExprInteger loc n ->
-                Just (ExprInteger loc n)
-            ExprOp loc symbol' args
-                | sameInductiveCarrierExpr symbol params (ExprOp loc symbol' args) ->
-                    Just replacement
-                | symbol == symbol' ->
-                    Nothing
-                | otherwise ->
-                    ExprOp loc symbol' <$> traverse go args
-            ExprStructOp loc structSymbol expr ->
-                ExprStructOp loc structSymbol <$> traverse go expr
-            ExprFiniteSet loc exprs ->
-                ExprFiniteSet loc <$> traverse go exprs
-            ExprSep{} ->
-                Nothing
-            ExprReplace{} ->
-                Nothing
-            ExprReplacePred{} ->
-                Nothing
-
-formulaMentionsFunction :: MixfixItem -> Formula -> Bool
-formulaMentionsFunction symbol = \case
-    FormulaChain chain ->
-        chainMentionsFunction symbol chain
-    FormulaPredicate _loc _predicate _marker exprs ->
-        any (exprMentionsFunction symbol) exprs
-    Connected _loc _conn left right ->
-        formulaMentionsFunction symbol left || formulaMentionsFunction symbol right
-    FormulaNeg _loc phi ->
-        formulaMentionsFunction symbol phi
-    FormulaQuantified _loc _quant _vars _bound phi ->
-        formulaMentionsFunction symbol phi
-    PropositionalConstant{} ->
-        False
-
-chainMentionsFunction :: MixfixItem -> Chain -> Bool
-chainMentionsFunction symbol = \case
-    ChainBase left _sign relation right ->
-        any (exprMentionsFunction symbol) left || relationMentionsFunction symbol relation || any (exprMentionsFunction symbol) right
-    ChainCons left _sign relation rest ->
-        any (exprMentionsFunction symbol) left || relationMentionsFunction symbol relation || chainMentionsFunction symbol rest
-
-relationMentionsFunction :: MixfixItem -> Relation -> Bool
-relationMentionsFunction symbol = \case
-    Relation _loc _relationSymbol exprs ->
-        any (exprMentionsFunction symbol) exprs
-    RelationExpr _loc expr ->
-        exprMentionsFunction symbol expr
-
-exprMentionsFunction :: MixfixItem -> Expr -> Bool
-exprMentionsFunction symbol = \case
-    ExprVar{} ->
-        False
-    ExprInteger{} ->
-        False
-    ExprOp _loc symbol' args ->
-        symbol == symbol' || any (exprMentionsFunction symbol) args
-    ExprStructOp _loc _structSymbol expr ->
-        maybe False (exprMentionsFunction symbol) expr
-    ExprFiniteSet _loc exprs ->
-        any (exprMentionsFunction symbol) exprs
-    ExprSep _loc _var bound _stmt ->
-        exprMentionsFunction symbol bound
-    ExprReplace _loc expr bounds _maybeStmt ->
-        exprMentionsFunction symbol expr || any (exprMentionsFunction symbol . snd) bounds
-    ExprReplacePred _loc _x _y expr _stmt ->
-        exprMentionsFunction symbol expr
-
-formulaVars :: Formula -> [VarSymbol]
-formulaVars = \case
-    FormulaChain chain ->
-        chainVars chain
-    FormulaPredicate _loc _predicate _marker exprs ->
-        concatMap exprVars exprs
-    Connected _loc _conn left right ->
-        formulaVars left <> formulaVars right
-    FormulaNeg _loc phi ->
-        formulaVars phi
-    FormulaQuantified _loc _quant vars _bound phi ->
-        List.filter (`notElem` toList vars) (formulaVars phi)
-    PropositionalConstant{} ->
-        []
-
-chainVars :: Chain -> [VarSymbol]
-chainVars = \case
-    ChainBase left _sign relation right ->
-        concatMap exprVars (toList left) <> relationVars relation <> concatMap exprVars (toList right)
-    ChainCons left _sign relation rest ->
-        concatMap exprVars (toList left) <> relationVars relation <> chainVars rest
-
-relationVars :: Relation -> [VarSymbol]
-relationVars = \case
-    Relation _loc _relationSymbol exprs ->
-        concatMap exprVars exprs
-    RelationExpr _loc expr ->
-        exprVars expr
-
-exprVars :: Expr -> [VarSymbol]
-exprVars = \case
-    ExprVar x ->
-        [x]
-    ExprInteger{} ->
-        []
-    ExprOp _loc _symbol args ->
-        concatMap exprVars args
-    ExprStructOp _loc _structSymbol expr ->
-        maybe [] exprVars expr
-    ExprFiniteSet _loc exprs ->
-        concatMap exprVars exprs
-    ExprSep _loc x bound _stmt ->
-        List.filter (/= x) (exprVars bound)
-    ExprReplace _loc expr bounds _maybeStmt ->
-        let boundVars = fst <$> toList bounds
-            free = exprVars expr <> concatMap (exprVars . snd) (toList bounds)
-        in List.filter (`notElem` boundVars) free
-    ExprReplacePred _loc x y expr _stmt ->
-        List.filter (\var -> var /= x && var /= y) (exprVars expr)
-
-orderedRenderVars :: [VarSymbol] -> [VarSymbol]
-orderedRenderVars =
-    reverse . snd . foldl' step (Set.empty, [])
-    where
-        step (seen, acc) x
-            | x `Set.member` seen = (seen, acc)
-            | otherwise = (Set.insert x seen, x : acc)
-
-renderSignatureBlock :: HintMap -> [Asm] -> Signature -> Html ()
-renderSignatureBlock hints asms sig = do
-    case asms of
-        [] -> skip
-        _ -> do
-            toHtml ("Assumptions: " :: Text)
-            renderAsmList hints asms
-            toHtml ("." :: Text)
-    when (not (null asms)) do
-        p_ do
-            renderSignature hints sig
-            toHtml ("." :: Text)
-    when (null asms) do
-        renderSignature hints sig
-        toHtml ("." :: Text)
-
-renderSignature :: HintMap -> Signature -> Html ()
-renderSignature hints = \case
-    SignatureAdj var adj -> do
-        renderVarInline var
-        toHtml (" can be " :: Text)
-        renderAdjInline renderVarInline adj
-    SignatureVerb var verb -> do
-        renderVarInline var
-        toHtml (" can " :: Text)
-        renderVerbInline False renderVarInline verb
-    SignatureNoun var noun -> do
-        renderVarInline var
-        toHtml (" is a " :: Text)
-        renderNounInline False renderVarInline noun
-    SignatureSymbolic symb np -> do
-        renderSymbolPatternInline hints symb
-        toHtml (" is a " :: Text)
-        renderNounPhraseMaybe hints np
-
-renderStructDefn :: HintMap -> StructDefn -> Html ()
-renderStructDefn hints StructDefn{..} = do
-    toHtml ("Structure phrase: " :: Text)
-    renderStructPhraseInline structPhrase
-    toHtml ("." :: Text)
-    p_ do
-        toHtml ("Label: " :: Text)
-        renderVarInline structLabel
-        toHtml ("." :: Text)
-    when (not (null structParents)) do
-        p_ do
-            toHtml ("Parents: " :: Text)
-            joinHtml (toHtml (", " :: Text)) (renderStructPhraseInline <$> structParents)
-            toHtml ("." :: Text)
-    when (not (null structFixes)) do
-        p_ do
-            toHtml ("Fixes: " :: Text)
-            inlineMath (joinHtml (moText ",") (renderStructSymbolName <$> structFixes))
-            toHtml ("." :: Text)
-    when (not (null structAssumes)) do
-        ul_ do
-            for_ structAssumes \(marker, stmt) -> li_ do
-                toHtml (markerText marker)
-                toHtml (": " :: Text)
-                renderStmtInline hints stmt
-                toHtml ("." :: Text)
-
-
-buildPreviewMap
-    :: HtmlRenderContext
-    -> Set Marker
-    -> AnchorMap
-    -> HtmlRenderIndex
-    -> Either HtmlRenderContextError PreviewMap
-buildPreviewMap
-        context
-        referencedMarkers
-        anchors
-        (HtmlRenderIndex targetIndex) =
-    Map.fromList <$> traverse makePreviewEntry indexedTargets
-  where
-    targets =
-        List.sortOn targetOrdinal
-            [ indexed
-            | marker <- Set.toList referencedMarkers
-            , marker `Map.notMember` anchors
-            , Just indexed@(IndexedReferenceTarget _ source _target) <-
-                [Map.lookup marker targetIndex]
-            , source /= htmlCurrentSource context
-            ]
-    targetOrdinal (IndexedReferenceTarget ordinal _source _target) =
-        ordinal
-    sourceTarget (IndexedReferenceTarget _ordinal source target) =
-        (source, target)
-    indexedTargets =
-        zip [1 :: Int ..] (sourceTarget <$> targets)
-
-    makePreviewEntry (index, (source, target)) = do
-        previewSourceLabel <-
-            htmlSourceLabel context source
-        previewSourceHref <-
-            htmlSourcePageHref context source
-        previewReferenceHref <-
-            htmlSourceFragmentHref
-                context
-                source
-                (targetAnchorId target)
-        let marker = targetMarker target
-            previewMarker = marker
-            previewKind = targetKind target
-            previewTitle = targetTitle target
-            previewId =
-                "reference-preview-" <> Text.pack (show index)
-            previewBody = targetBody target
-        Right (marker, PreviewEntry{..})
-
-renderPreviewStore :: HintMap -> PreviewMap -> Html ()
-renderPreviewStore hints previews =
-    div_ [class_ "reference-preview-store", makeAttributes "aria-hidden" "true"] do
-        traverse_ (renderPreviewEntry hints) (Map.elems previews)
-
-renderPreviewEntry :: HintMap -> PreviewEntry -> Html ()
-renderPreviewEntry hints PreviewEntry{..} =
-    div_ [id_ previewId, class_ "reference-preview-template"] do
-        div_ [class_ "reference-preview-heading"] do
-            toHtml previewKind
-            toHtml (" " :: Text)
-            code_ (toHtml (markerText previewMarker))
-            case previewTitle of
-                Nothing ->
-                    skip
-                Just title -> do
-                    toHtml (" (" :: Text)
-                    toHtml title
-                    toHtml (")" :: Text)
-        div_ [class_ "reference-preview-source"] do
-            toHtml ("from " :: Text)
-            a_ [href_ previewSourceHref] do
-                code_ (toHtml previewSourceLabel)
-        div_ [class_ "reference-preview-body"] do
-            previewBody hints
-
-renderPreviewBlockBody :: HintMap -> Block -> Html ()
-renderPreviewBlockBody hints = \case
-    BlockAxiom _loc _title _marker axiom ->
-        previewStatement (renderAxiom hints axiom)
-    BlockClaim _kind _loc _title _marker claim ->
-        previewStatement (renderClaim hints claim)
-    BlockDefn _loc _title _marker defn ->
-        previewStatement (renderDefn hints defn)
-    BlockAbbr _loc _title _marker abbr ->
-        previewStatement (renderAbbreviation hints abbr)
-    BlockData _loc _title _marker datatype ->
-        renderDatatype hints datatype
-    BlockInductive _loc _title marker ind ->
-        renderInductive hints marker ind
-    BlockSig _loc _title _marker asms sig ->
-        renderSignatureBlock hints asms sig
-    BlockStruct _loc _title _marker structDefn ->
-        renderStructDefn hints structDefn
-    BlockProof{} ->
-        skip
-
-previewStatement :: Html () -> Html ()
-previewStatement =
-    p_ [class_ "reference-preview-statement"]
-
-referenceTargetsOfBlockRenderInfo :: BlockRenderInfo -> [ReferenceTarget]
-referenceTargetsOfBlockRenderInfo (_index, block, blockId) =
-    maybeToList blockTarget <> inductiveTargets
-    where
-        blockTarget = do
-            marker <- blockMarkerOf block
-            pure ReferenceTarget
-                { targetMarker = marker
-                , targetAnchorId = blockId
-                , targetKind = blockPrefixText block
-                , targetTitle = formatBlockTitle (blockTitleOf block)
-                , targetBody = \hints -> renderPreviewBlockBody hints block
-                }
-
-        inductiveTargets = case block of
-            BlockInductive _loc _title marker inductive ->
-                [ ReferenceTarget
-                    { targetMarker = inductiveDerivedFactMarker
-                    , targetAnchorId = markerText inductiveDerivedFactMarker
-                    , targetKind = "Inductive Fact"
-                    , targetTitle = Nothing
-                    , targetBody = \hints -> previewStatement (inlineMath (renderFormulaMath hints inductiveDerivedFactFormula))
-                    }
-                | InductiveDerivedFact{inductiveDerivedFactMarker, inductiveDerivedFactFormula} <- inductiveDerivedFacts marker inductive
-                ]
-            _ ->
-                []
-
-
-renderProof :: HintMap -> ReferenceContext -> Proof -> Html ()
-renderProof hints references = \case
-    Omitted _loc ->
-        p_ "Omitted."
-    Qed mloc justification ->
-        renderProofTerminal mloc justification
-    Contradiction _loc justification ->
-        p_ do
-            toHtml ("Contradiction" :: Text)
-            renderJustificationSuffix references justification
-            toHtml ("." :: Text)
-    ByCase _loc cases -> do
-        p_ "Proof by cases."
-        term "proof-" (traverse_ (renderCase hints references) cases)
-    ByContradiction _loc proof -> do
-        p_ "Proof by contradiction."
-        term "proof-" (renderProof hints references proof)
-    BySetInduction _loc maybeTerm proof -> do
-        p_ do
-            toHtml ("Proof by set induction" :: Text)
-            case maybeTerm of
-                Nothing -> skip
-                Just targetTerm -> do
-                    toHtml (" on " :: Text)
-                    renderTermInline hints targetTerm
-            toHtml ("." :: Text)
-        term "proof-" (renderProof hints references proof)
-    ByOrdInduction _loc proof -> do
-        p_ "Proof by ordinal induction."
-        term "proof-" (renderProof hints references proof)
-    Assume _loc stmt proof -> do
-        p_ do
-            toHtml ("Assume " :: Text)
-            renderStmtInline hints stmt
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    FixSymbolic _loc vars bound proof -> do
-        p_ do
-            toHtml ("Fix " :: Text)
-            renderVarListInline vars
-            renderBoundInline hints vars bound
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    FixSuchThat _loc vars stmt proof -> do
-        p_ do
-            toHtml ("Fix " :: Text)
-            renderVarListInline vars
-            toHtml (" such that " :: Text)
-            renderStmtInline hints stmt
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    Calc _loc maybeQuant calc proof -> do
-        renderCalc hints references maybeQuant calc
-        renderProofContinuation hints references proof
-    TakeVar _loc vars bound stmt justification proof -> do
-        p_ do
-            toHtml ("Take " :: Text)
-            renderVarListInline vars
-            renderBoundInline hints vars bound
-            toHtml (" such that " :: Text)
-            renderStmtInline hints stmt
-            renderJustificationSuffix references justification
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    TakeNoun _loc np justification proof -> do
-        p_ do
-            toHtml ("Take " :: Text)
-            renderNounPhraseList hints np
-            renderJustificationSuffix references justification
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    Have _loc maybeStmt stmt justification proof -> do
-        p_ do
-            case maybeStmt of
-                Nothing
-                    | isImplicitProofEnd proof ->
-                        skip
-                    | otherwise ->
-                        toHtml ("We have " :: Text)
-                Just premise -> do
-                    toHtml ("Since " :: Text)
-                    renderStmtInline hints premise
-                    toHtml (", we have " :: Text)
-            renderStmtInline hints stmt
-            renderJustificationSuffix references justification
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    Suffices _loc stmt justification proof -> do
-        p_ do
-            toHtml ("It suffices to show that " :: Text)
-            renderStmtInline hints stmt
-            renderJustificationSuffix references justification
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    Subclaim _loc stmt subproof proof -> do
-        p_ do
-            toHtml ("Show " :: Text)
-            renderStmtInline hints stmt
-            toHtml ("." :: Text)
-        term "proof-" (renderProof hints references subproof)
-        renderProofContinuation hints references proof
-    Define _loc var expr proof -> do
-        p_ do
-            toHtml ("Let " :: Text)
-            renderVarEqInline hints var expr
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    DefineFunction _loc fun arg value boundVar boundExpr proof -> do
-        p_ do
-            toHtml ("Let " :: Text)
-            renderFunctionEqInline hints fun arg value
-            toHtml (" for " :: Text)
-            renderVarInline boundVar
-            toHtml (" in " :: Text)
-            inlineMath (renderExprMathRow hints boundExpr)
-            toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-    DefineFunctionLocal _loc fun arg _target domVar codVar rules proof -> do
-        p_ do
-            toHtml ("Let " :: Text)
-            renderFunctionCallInline fun arg
-            toHtml (" be locally defined from " :: Text)
-            renderVarInline domVar
-            toHtml (" to " :: Text)
-            renderVarInline codVar
-            toHtml ("." :: Text)
-        ul_ do
-            for_ (toList rules) \(ruleTerm, formula) -> li_ do
-                inlineMath (renderExprMathRow hints ruleTerm)
-                toHtml (" if " :: Text)
-                inlineMath (renderFormulaMath hints formula)
-                toHtml ("." :: Text)
-        renderProofContinuation hints references proof
-
-    where
-        renderProofTerminal :: Maybe Location -> Justification -> Html ()
-        renderProofTerminal mloc justification = case (mloc, justification) of
-            (Nothing, JustificationEmpty) ->
-                skip
-            (Just _, JustificationEmpty) ->
-                p_ "Trivial."
-            _ ->
-                p_ do
-                    toHtml ("Follows" :: Text)
-                    renderJustificationSuffix references justification
-                    toHtml ("." :: Text)
-
-renderProofContinuation :: HintMap -> ReferenceContext -> Proof -> Html ()
-renderProofContinuation hints references proof =
-    unless (isImplicitProofEnd proof) (renderProof hints references proof)
-
-isImplicitProofEnd :: Proof -> Bool
-isImplicitProofEnd = \case
-    Qed Nothing JustificationEmpty -> True
-    _ -> False
-
-proofStepCount :: Proof -> Int
-proofStepCount = \case
-    Omitted _loc -> 1
-    Qed{} -> 1
-    Contradiction{} -> 1
-    ByCase _loc cases -> 1 + sum (caseStepCount <$> cases)
-    ByContradiction _loc proof -> 1 + proofStepCount proof
-    BySetInduction _loc _maybeTerm proof -> 1 + proofStepCount proof
-    ByOrdInduction _loc proof -> 1 + proofStepCount proof
-    Assume _loc _stmt proof -> 1 + proofStepCount proof
-    FixSymbolic _loc _vars _bound proof -> 1 + proofStepCount proof
-    FixSuchThat _loc _vars _stmt proof -> 1 + proofStepCount proof
-    Calc _loc _maybeQuant calc proof -> 1 + calcStepCount calc + proofStepCount proof
-    TakeVar _loc _vars _bound _stmt _justification proof -> 1 + proofStepCount proof
-    TakeNoun _loc _np _justification proof -> 1 + proofStepCount proof
-    Have _loc _maybeStmt _stmt _justification proof -> 1 + proofStepCount proof
-    Suffices _loc _stmt _justification proof -> 1 + proofStepCount proof
-    Subclaim _loc _stmt subproof proof -> 1 + proofStepCount subproof + proofStepCount proof
-    Define _loc _var _expr proof -> 1 + proofStepCount proof
-    DefineFunction _loc _fun _arg _value _boundVar _boundExpr proof -> 1 + proofStepCount proof
-    DefineFunctionLocal _loc _fun _arg _target _domVar _codVar rules proof ->
-        1 + length rules + proofStepCount proof
-
-caseStepCount :: Case -> Int
-caseStepCount Case{caseProof} = 1 + proofStepCount caseProof
-
-calcStepCount :: Calc -> Int
-calcStepCount = \case
-    Equation _ steps -> length steps
-    Biconditionals _ steps -> length steps
-
-renderCase :: HintMap -> ReferenceContext -> Case -> Html ()
-renderCase hints references Case{..} =
-    term "proof-" do
-        p_ do
-            toHtml ("Case " :: Text)
-            renderStmtInline hints caseOf
-            toHtml ("." :: Text)
-        renderProof hints references caseProof
-
-renderCalc :: HintMap -> ReferenceContext -> Maybe CalcQuantifier -> Calc -> Html ()
-renderCalc hints references maybeQuant calc = do
-    p_ do
-        toHtml ("Calculation" :: Text)
-        case maybeQuant of
-            Nothing -> skip
-            Just quant -> do
-                toHtml (" for " :: Text)
-                renderCalcQuantifierInline hints quant
-        toHtml ("." :: Text)
-    blockMath (renderCalcMath hints calc)
-    let justifications = calcJustifications calc
-    when (not (null justifications)) do
-        ul_ do
-            traverse_ renderStepJustification justifications
-    where
-        renderStepJustification :: (Int, Justification) -> Html ()
-        renderStepJustification (_idx, JustificationEmpty) = skip
-        renderStepJustification (idx, jst) = li_ do
-            toHtml ("Step " <> Text.pack (show idx) <> ": " :: Text)
-            renderJustification references jst
-            toHtml ("." :: Text)
-
-renderCalcQuantifierInline :: HintMap -> CalcQuantifier -> Html ()
-renderCalcQuantifierInline hints (CalcQuantifier vars bound maybeStmt) = do
-    renderVarListInline vars
-    renderBoundInline hints vars bound
-    case maybeStmt of
-        Nothing -> skip
-        Just stmt -> do
-            toHtml (" such that " :: Text)
-            renderStmtInline hints stmt
-
-renderCalcMath :: HintMap -> Calc -> Html ()
-renderCalcMath hints = \case
-    Equation expr steps -> do
-        renderExprMathRow hints expr
-        for_ (toList steps) \(nextExpr, _jst) -> do
-            moText "="
-            renderExprMathRow hints nextExpr
-    Biconditionals phi steps -> do
-        renderFormulaMath hints phi
-        for_ (toList steps) \(nextPhi, _jst) -> do
-            moText "⇔"
-            renderFormulaMath hints nextPhi
-
-calcJustifications :: Calc -> [(Int, Justification)]
-calcJustifications = \case
-    Equation _ steps ->
-        zip [1..] (snd <$> toList steps)
-    Biconditionals _ steps ->
-        zip [1..] (snd <$> toList steps)
-
-
-renderStmtInline :: HintMap -> Stmt -> Html ()
-renderStmtInline hints = \case
-    StmtFormula phi ->
-        inlineMath (renderFormulaMath hints phi)
-    StmtVerbPhrase ts vp -> do
-        renderTermList hints ts
-        toHtml (" " :: Text)
-        renderVerbPhraseInline hints (length ts > 1) vp
-    StmtNoun ts np -> do
-        renderTermList hints ts
-        toHtml (if length ts > 1 then " are a " else " is a " :: Text)
-        renderNounPhraseMaybe hints np
-    StmtStruct t structPhrase -> do
-        renderTermInline hints t
-        toHtml (" is a " :: Text)
-        renderStructPhraseInline structPhrase
-    StmtNeg _loc stmt -> do
-        toHtml ("it is not the case that " :: Text)
-        renderStmtInline hints stmt
-    StmtExists _loc np -> do
-        toHtml ("there exists " :: Text)
-        renderNounPhraseList hints np
-    StmtConnected conn _loc stmt1 stmt2 -> do
-        renderConnectedStmtInline hints conn stmt1 stmt2
-    StmtQuantPhrase _loc qp stmt -> do
-        renderQuantPhraseInline hints qp
-        toHtml (" " :: Text)
-        renderStmtInline hints stmt
-    SymbolicQuantified _loc quant vars bound suchThat stmt -> do
-        toHtml (quantifierWord quant)
-        toHtml (" " :: Text)
-        renderBoundSubjectInline hints vars bound
-        renderQuantifiedTailInline hints quant suchThat stmt
-
-renderQuantPhraseInline :: HintMap -> QuantPhrase -> Html ()
-renderQuantPhraseInline hints (QuantPhrase quant np) = do
-    toHtml (quantifierWord quant)
-    toHtml (" " :: Text)
-    renderNounPhraseList hints np
-
-quantifierWord :: Quantifier -> Text
-quantifierWord = \case
-    Universally -> "for every"
-    Existentially -> "there exists"
-    Nonexistentially -> "there exists no"
-
-connectiveWord :: Connective -> Text
-connectiveWord = \case
-    Conjunction -> "and"
-    Disjunction -> "or"
-    Implication -> "implies"
-    Equivalence -> "iff"
-    ExclusiveOr -> "xor"
-    NegatedDisjunction -> "nor"
-
-renderConnectedStmtInline :: HintMap -> Connective -> Stmt -> Stmt -> Html ()
-renderConnectedStmtInline hints conn stmt1 stmt2 = case conn of
-    ExclusiveOr -> do
-        toHtml ("either " :: Text)
-        renderStmtInline hints stmt1
-        toHtml (" or " :: Text)
-        renderStmtInline hints stmt2
-    NegatedDisjunction -> do
-        toHtml ("neither " :: Text)
-        renderStmtInline hints stmt1
-        toHtml (" nor " :: Text)
-        renderStmtInline hints stmt2
-    _ -> do
-        renderStmtInline hints stmt1
-        toHtml (" " :: Text)
-        toHtml (connectiveWord conn)
-        toHtml (" " :: Text)
-        renderStmtInline hints stmt2
-
-renderQuantifiedTailInline :: HintMap -> Quantifier -> Maybe Stmt -> Stmt -> Html ()
-renderQuantifiedTailInline hints quant suchThat stmt =
-    case quant of
-        Universally -> do
-            for_ suchThat \suchStmt -> do
-                toHtml (" such that " :: Text)
-                renderStmtInline hints suchStmt
-            toHtml (" we have " :: Text)
-            renderStmtInline hints stmt
-        Existentially ->
-            renderExistentialTailInline hints suchThat stmt
-        Nonexistentially ->
-            renderExistentialTailInline hints suchThat stmt
-
-renderExistentialTailInline :: HintMap -> Maybe Stmt -> Stmt -> Html ()
-renderExistentialTailInline hints suchThat stmt = do
-    toHtml (" such that " :: Text)
-    case suchThat of
-        Nothing ->
-            renderStmtInline hints stmt
-        Just suchStmt -> do
-            renderStmtInline hints suchStmt
-            toHtml (" and " :: Text)
-            renderStmtInline hints stmt
-
-
-renderAsmList :: HintMap -> [Asm] -> Html ()
-renderAsmList hints asms =
-    joinHtml (toHtml ("; " :: Text)) (renderAsm hints <$> asms)
-
-renderAsm :: HintMap -> Asm -> Html ()
-renderAsm hints = \case
-    AsmSuppose stmt ->
-        renderStmtInline hints stmt
-    AsmLetNoun vars np -> do
-        renderVarListInline vars
-        toHtml (" be " :: Text)
-        renderNounPhraseMaybe hints np
-    AsmLetIn vars expr -> do
-        renderVarListInline vars
-        toHtml (" be in " :: Text)
-        inlineMath (renderExprMathRow hints expr)
-    AsmLetThe var fun -> do
-        renderVarInline var
-        toHtml (" be " :: Text)
-        renderFunInline renderTermInline' fun
-            where renderTermInline' = renderTermInline hints
-    AsmLetEq var expr -> do
-        renderVarEqInline hints var expr
-    AsmLetStruct var structPhrase -> do
-        renderVarInline var
-        toHtml (" be a " :: Text)
-        renderStructPhraseInline structPhrase
-
-
-renderTermInline :: HintMap -> Term -> Html ()
-renderTermInline hints = \case
-    TermExpr expr ->
-        inlineMath (renderExprMathRow hints expr)
-    TermFun fun -> do
-        toHtml ("the " :: Text)
-        renderFunInline (renderTermInline hints) fun
-    TermIota _loc var stmt -> do
-        toHtml ("the " :: Text)
-        renderVarInline var
-        toHtml (" such that " :: Text)
-        renderStmtInline hints stmt
-    TermQuantified quant _loc np -> do
-        toHtml (termQuantifierWord quant)
-        toHtml (" " :: Text)
-        renderNounPhraseMaybe hints np
-
-termQuantifierWord :: Quantifier -> Text
-termQuantifierWord = \case
-    Universally -> "every"
-    Existentially -> "some"
-    Nonexistentially -> "no"
-
-renderTermList :: HintMap -> NonEmpty Term -> Html ()
-renderTermList hints =
-    joinHtml (toHtml (" and " :: Text)) . fmap (renderTermInline hints) . toList
-
-renderNounPhraseMaybe :: HintMap -> NounPhrase Maybe -> Html ()
-renderNounPhraseMaybe hints (NounPhrase ls noun maybeName rs maybeSuchThat) = do
-    renderAdjListInline renderTermInline' ls
-    renderNounInline False renderTermInline' noun
-    case maybeName of
-        Nothing -> skip
-        Just name -> do
-            toHtml (" " :: Text)
-            renderVarInline name
-    renderAdjRListInline hints rs
-    case maybeSuchThat of
-        Nothing -> skip
-        Just stmt -> do
-            toHtml (" such that " :: Text)
-            renderStmtInline hints stmt
-    where
-        renderTermInline' = renderTermInline hints
-
-renderNounPhraseList :: HintMap -> NounPhrase [] -> Html ()
-renderNounPhraseList hints (NounPhrase ls noun names rs maybeSuchThat) = do
-    renderAdjListInline renderTermInline' ls
-    renderNounInline (length names > 1) renderTermInline' noun
-    when (not (null names)) do
-        toHtml (" " :: Text)
-        renderVarListInline (NonEmpty.fromList names)
-    renderAdjRListInline hints rs
-    case maybeSuchThat of
-        Nothing -> skip
-        Just stmt -> do
-            toHtml (" such that " :: Text)
-            renderStmtInline hints stmt
-    where
-        renderTermInline' = renderTermInline hints
-
-renderAdjListInline :: (a -> Html ()) -> [AdjLOf a] -> Html ()
-renderAdjListInline renderArg adjs =
-    unless (null adjs) do
-        joinHtml (toHtml (" " :: Text)) (renderAdjLInline renderArg <$> adjs)
-        toHtml (" " :: Text)
-
-renderAdjRListInline :: HintMap -> [AdjROf Term] -> Html ()
-renderAdjRListInline hints adjs =
-    unless (null adjs) do
-        toHtml (" " :: Text)
-        joinHtml (toHtml (" and " :: Text)) (renderAdjRInline hints <$> adjs)
-
-renderAdjLInline :: (a -> Html ()) -> AdjLOf a -> Html ()
-renderAdjLInline renderArg (AdjL _loc item args) =
-    renderLexicalItemInline renderArg item args
-
-renderAdjRInline :: HintMap -> AdjROf Term -> Html ()
-renderAdjRInline hints = \case
-    AdjR _loc item args ->
-        renderLexicalItemInline (renderTermInline hints) item args
-    AttrRThat verbPhrase -> do
-        toHtml ("that " :: Text)
-        renderVerbPhraseInline hints False verbPhrase
-
-renderAdjInline :: (a -> Html ()) -> AdjOf a -> Html ()
-renderAdjInline renderArg (Adj _loc item args) =
-    renderLexicalItemInline renderArg item args
-
-renderVerbInline :: Bool -> (a -> Html ()) -> VerbOf a -> Html ()
-renderVerbInline isPlural renderArg (Verb _loc item args) =
-    renderLexicalItemSgPlInline isPlural renderArg item args
-
-renderVerbPhraseInline :: HintMap -> Bool -> VerbPhrase -> Html ()
-renderVerbPhraseInline hints isPlural = \case
-    VPVerb verb ->
-        renderVerbInline isPlural (renderTermInline hints) verb
-    VPAdj adjs -> do
-        toHtml (if isPlural then "are " else "is " :: Text)
-        joinHtml (toHtml (" and " :: Text)) (renderAdjInline (renderTermInline hints) <$> toList adjs)
-    VPVerbNot verb -> do
-        toHtml (if isPlural then "do not " else "does not " :: Text)
-        renderVerbInline True (renderTermInline hints) verb
-    VPAdjNot adjs -> do
-        toHtml (if isPlural then "are not " else "is not " :: Text)
-        joinHtml (toHtml (" and " :: Text)) (renderAdjInline (renderTermInline hints) <$> toList adjs)
-
-renderNounInline :: Bool -> (a -> Html ()) -> NounOf a -> Html ()
-renderNounInline isPlural renderArg (Noun _loc item args) =
-    renderLexicalItemSgPlInline isPlural renderArg item args
-
-renderFunInline :: (a -> Html ()) -> FunOf a -> Html ()
-renderFunInline renderArg Fun{phrase, funArgs} =
-    renderLexicalItemSgPlInline False renderArg phrase funArgs
-
-renderStructPhraseInline :: StructPhrase -> Html ()
-renderStructPhraseInline item =
-    renderLexicalItemSgPlInline False renderTermInlinePlaceholder item []
-
-renderTermInlinePlaceholder :: a -> Html ()
-renderTermInlinePlaceholder _ = toHtml ("?" :: Text)
-
-renderLexicalItemInline :: (a -> Html ()) -> LexicalItem -> [a] -> Html ()
-renderLexicalItemInline renderArg item args =
-    renderPatternInline renderArg (lexicalItemPhrase item) args
-
-renderLexicalItemSgPlInline :: Bool -> (a -> Html ()) -> LexicalItemSgPl -> [a] -> Html ()
-renderLexicalItemSgPlInline isPlural renderArg item args =
-    renderPatternInline renderArg phrase args
-    where
-        phrase = if isPlural then pl (lexicalItemSgPlPhrase item) else sg (lexicalItemSgPlPhrase item)
-
-renderPatternInline :: (a -> Html ()) -> [Maybe Token] -> [a] -> Html ()
-renderPatternInline renderArg patternParts args =
-    joinHtml (toHtml (" " :: Text)) (go patternParts args)
-    where
-        go [] [] = []
-        go [] (_ : _) = error "renderPatternInline: too many arguments"
-        go (Nothing : rest) (arg : restArgs) = renderArg arg : go rest restArgs
-        go (Nothing : _) [] = error "renderPatternInline: not enough arguments"
-        go (Just tok : rest) restArgs = tokenTextHtml tok : go rest restArgs
-
-renderStmtMath :: HintMap -> Stmt -> Html ()
-renderStmtMath hints =
-    renderStmtMathFragments . stmtMathFragments hints
-
-renderStmtMathFragments :: StmtMathFragments -> Html ()
-renderStmtMathFragments =
-    go ""
-    where
-        go :: Text -> StmtMathFragments -> Html ()
-        go pending = \case
-            [] ->
-                flush pending
-            StmtMathProse text : rest ->
-                go (pending <> text) rest
-            StmtMathNode node : rest -> do
-                flush pending
-                node
-                go "" rest
-
-        flush :: Text -> Html ()
-        flush text =
-            let renderedText = preserveBoundarySpaces text
-            in unless (Text.null renderedText) (mtextText renderedText)
-
-        preserveBoundarySpaces :: Text -> Text
-        preserveBoundarySpaces text =
-            Text.replicate leadingCount nbsp
-                <> middleText
-                <> Text.replicate trailingCount nbsp
-            where
-                leadingCount = Text.length (Text.takeWhile (== ' ') text)
-                textAfterLeading = Text.drop leadingCount text
-                trailingCount = Text.length (Text.takeWhileEnd (== ' ') textAfterLeading)
-                middleText = Text.dropEnd trailingCount textAfterLeading
-                nbsp = Text.singleton '\160'
-
-stmtMathProse :: Text -> StmtMathFragments
-stmtMathProse text
-    | Text.null text = []
-    | otherwise = [StmtMathProse text]
-
-stmtMathNode :: Html () -> StmtMathFragments
-stmtMathNode html =
-    [StmtMathNode html]
-
-joinStmtMathFragments :: StmtMathFragments -> [StmtMathFragments] -> StmtMathFragments
-joinStmtMathFragments _ [] = []
-joinStmtMathFragments separator (first : rest) =
-    first <> foldMap (separator <>) rest
-
-stmtMathFragments :: HintMap -> Stmt -> StmtMathFragments
-stmtMathFragments hints = \case
-    StmtFormula phi ->
-        stmtMathNode (renderFormulaMath hints phi)
-    StmtVerbPhrase ts vp -> do
-        termListMathFragments hints ts
-            <> stmtMathProse " "
-            <> verbPhraseMathFragments hints (length ts > 1) vp
-    StmtNoun ts np -> do
-        termListMathFragments hints ts
-            <> stmtMathProse (if length ts > 1 then " are a " else " is a ")
-            <> nounPhraseMaybeMathFragments hints np
-    StmtStruct t structPhrase -> do
-        termMathFragments hints t
-            <> stmtMathProse " is a "
-            <> structPhraseMathFragments structPhrase
-    StmtNeg _loc stmt -> do
-        stmtMathProse "it is not the case that "
-            <> stmtMathFragments hints stmt
-    StmtExists _loc np -> do
-        stmtMathProse "there exists "
-            <> nounPhraseListMathFragments hints np
-    StmtConnected conn _loc stmt1 stmt2 -> do
-        connectedStmtMathFragments hints conn stmt1 stmt2
-    StmtQuantPhrase _loc qp stmt -> do
-        quantPhraseMathFragments hints qp
-            <> stmtMathProse " "
-            <> stmtMathFragments hints stmt
-    SymbolicQuantified _loc quant vars bound suchThat stmt -> do
-        stmtMathProse (quantifierWord quant <> " ")
-            <> boundSubjectMathFragments hints vars bound
-            <> quantifiedTailMathFragments hints quant suchThat stmt
-
-quantPhraseMathFragments :: HintMap -> QuantPhrase -> StmtMathFragments
-quantPhraseMathFragments hints (QuantPhrase quant np) =
-    stmtMathProse (quantifierWord quant <> " ")
-        <> nounPhraseListMathFragments hints np
-
-connectedStmtMathFragments :: HintMap -> Connective -> Stmt -> Stmt -> StmtMathFragments
-connectedStmtMathFragments hints conn stmt1 stmt2 = case conn of
-    ExclusiveOr ->
-        stmtMathProse "either "
-            <> stmtMathFragments hints stmt1
-            <> stmtMathProse " or "
-            <> stmtMathFragments hints stmt2
-    NegatedDisjunction ->
-        stmtMathProse "neither "
-            <> stmtMathFragments hints stmt1
-            <> stmtMathProse " nor "
-            <> stmtMathFragments hints stmt2
-    _ ->
-        stmtMathFragments hints stmt1
-            <> stmtMathProse (" " <> connectiveWord conn <> " ")
-            <> stmtMathFragments hints stmt2
-
-quantifiedTailMathFragments :: HintMap -> Quantifier -> Maybe Stmt -> Stmt -> StmtMathFragments
-quantifiedTailMathFragments hints quant suchThat stmt =
-    case quant of
-        Universally ->
-            foldMap
-                (\suchStmt -> stmtMathProse " such that " <> stmtMathFragments hints suchStmt)
-                suchThat
-                <> stmtMathProse " we have "
-                <> stmtMathFragments hints stmt
-        Existentially ->
-            existentialTailMathFragments hints suchThat stmt
-        Nonexistentially ->
-            existentialTailMathFragments hints suchThat stmt
-
-existentialTailMathFragments :: HintMap -> Maybe Stmt -> Stmt -> StmtMathFragments
-existentialTailMathFragments hints suchThat stmt =
-    stmtMathProse " such that "
-        <> case suchThat of
-            Nothing ->
-                stmtMathFragments hints stmt
-            Just suchStmt ->
-                stmtMathFragments hints suchStmt
-                    <> stmtMathProse " and "
-                    <> stmtMathFragments hints stmt
-
-termMathFragments :: HintMap -> Term -> StmtMathFragments
-termMathFragments hints = \case
-    TermExpr expr ->
-        stmtMathNode (renderExprMathRow hints expr)
-    TermFun fun -> do
-        stmtMathProse "the "
-            <> funMathFragments (termMathFragments hints) fun
-    TermIota _loc var stmt -> do
-        stmtMathProse "the "
-            <> stmtMathNode (renderVarMath var)
-            <> stmtMathProse " such that "
-            <> stmtMathFragments hints stmt
-    TermQuantified quant _loc np -> do
-        stmtMathProse (termQuantifierWord quant <> " ")
-            <> nounPhraseMaybeMathFragments hints np
-
-termListMathFragments :: HintMap -> NonEmpty Term -> StmtMathFragments
-termListMathFragments hints =
-    joinStmtMathFragments (stmtMathProse " and ") . fmap (termMathFragments hints) . toList
-
-nounPhraseMaybeMathFragments :: HintMap -> NounPhrase Maybe -> StmtMathFragments
-nounPhraseMaybeMathFragments hints (NounPhrase ls noun maybeName rs maybeSuchThat) =
-    adjListMathFragments renderTermMath' ls
-        <> nounMathFragments False renderTermMath' noun
-        <> foldMap (\name -> stmtMathProse " " <> stmtMathNode (renderVarMath name)) maybeName
-        <> adjRListMathFragments hints rs
-        <> foldMap (\stmt -> stmtMathProse " such that " <> stmtMathFragments hints stmt) maybeSuchThat
-    where
-        renderTermMath' = termMathFragments hints
-
-nounPhraseListMathFragments :: HintMap -> NounPhrase [] -> StmtMathFragments
-nounPhraseListMathFragments hints (NounPhrase ls noun names rs maybeSuchThat) =
-    adjListMathFragments renderTermMath' ls
-        <> nounMathFragments (length names > 1) renderTermMath' noun
-        <> if null names
-            then []
-            else stmtMathProse " " <> stmtMathNode (renderVarListMath (NonEmpty.fromList names))
-        <> adjRListMathFragments hints rs
-        <> foldMap (\stmt -> stmtMathProse " such that " <> stmtMathFragments hints stmt) maybeSuchThat
-    where
-        renderTermMath' = termMathFragments hints
-
-adjListMathFragments :: (a -> StmtMathFragments) -> [AdjLOf a] -> StmtMathFragments
-adjListMathFragments renderArg adjs =
-    if null adjs
-        then []
-        else joinStmtMathFragments (stmtMathProse " ") (renderAdjLMathFragments renderArg <$> adjs)
-            <> stmtMathProse " "
-
-adjRListMathFragments :: HintMap -> [AdjROf Term] -> StmtMathFragments
-adjRListMathFragments hints adjs =
-    if null adjs
-        then []
-        else stmtMathProse " "
-            <> joinStmtMathFragments (stmtMathProse " and ") (renderAdjRMathFragments hints <$> adjs)
-
-renderAdjLMathFragments :: (a -> StmtMathFragments) -> AdjLOf a -> StmtMathFragments
-renderAdjLMathFragments renderArg (AdjL _loc item args) =
-    lexicalItemStmtMathFragments renderArg item args
-
-renderAdjRMathFragments :: HintMap -> AdjROf Term -> StmtMathFragments
-renderAdjRMathFragments hints = \case
-    AdjR _loc item args ->
-        lexicalItemStmtMathFragments (termMathFragments hints) item args
-    AttrRThat verbPhrase ->
-        stmtMathProse "that "
-            <> verbPhraseMathFragments hints False verbPhrase
-
-adjMathFragments :: (a -> StmtMathFragments) -> AdjOf a -> StmtMathFragments
-adjMathFragments renderArg (Adj _loc item args) =
-    lexicalItemStmtMathFragments renderArg item args
-
-verbMathFragments :: Bool -> (a -> StmtMathFragments) -> VerbOf a -> StmtMathFragments
-verbMathFragments isPlural renderArg (Verb _loc item args) =
-    lexicalItemSgPlStmtMathFragments isPlural renderArg item args
-
-verbPhraseMathFragments :: HintMap -> Bool -> VerbPhrase -> StmtMathFragments
-verbPhraseMathFragments hints isPlural = \case
-    VPVerb verb ->
-        verbMathFragments isPlural (termMathFragments hints) verb
-    VPAdj adjs ->
-        stmtMathProse (if isPlural then "are " else "is ")
-            <> joinStmtMathFragments (stmtMathProse " and ") (adjMathFragments (termMathFragments hints) <$> toList adjs)
-    VPVerbNot verb ->
-        stmtMathProse (if isPlural then "do not " else "does not ")
-            <> verbMathFragments True (termMathFragments hints) verb
-    VPAdjNot adjs ->
-        stmtMathProse (if isPlural then "are not " else "is not ")
-            <> joinStmtMathFragments (stmtMathProse " and ") (adjMathFragments (termMathFragments hints) <$> toList adjs)
-
-nounMathFragments :: Bool -> (a -> StmtMathFragments) -> NounOf a -> StmtMathFragments
-nounMathFragments isPlural renderArg (Noun _loc item args) =
-    lexicalItemSgPlStmtMathFragments isPlural renderArg item args
-
-funMathFragments :: (a -> StmtMathFragments) -> FunOf a -> StmtMathFragments
-funMathFragments renderArg Fun{phrase, funArgs} =
-    lexicalItemSgPlStmtMathFragments False renderArg phrase funArgs
-
-structPhraseMathFragments :: StructPhrase -> StmtMathFragments
-structPhraseMathFragments item =
-    lexicalItemSgPlStmtMathFragments False termMathPlaceholderFragments item []
-
-termMathPlaceholderFragments :: a -> StmtMathFragments
-termMathPlaceholderFragments _ =
-    stmtMathProse "?"
-
-lexicalItemStmtMathFragments :: (a -> StmtMathFragments) -> LexicalItem -> [a] -> StmtMathFragments
-lexicalItemStmtMathFragments renderArg item args =
-    patternStmtMathFragments renderArg (lexicalItemPhrase item) args
-
-lexicalItemSgPlStmtMathFragments :: Bool -> (a -> StmtMathFragments) -> LexicalItemSgPl -> [a] -> StmtMathFragments
-lexicalItemSgPlStmtMathFragments isPlural renderArg item args =
-    patternStmtMathFragments renderArg phrase args
-    where
-        phrase = if isPlural then pl (lexicalItemSgPlPhrase item) else sg (lexicalItemSgPlPhrase item)
-
-patternStmtMathFragments :: (a -> StmtMathFragments) -> [Maybe Token] -> [a] -> StmtMathFragments
-patternStmtMathFragments renderArg patternParts args =
-    joinStmtMathFragments (stmtMathProse " ") (go patternParts args)
-    where
-        go [] [] = []
-        go [] (_ : _) = error "renderPatternStmtMath: too many arguments"
-        go (Nothing : rest) (arg : restArgs) = renderArg arg : go rest restArgs
-        go (Nothing : _) [] = error "renderPatternStmtMath: not enough arguments"
-        go (Just tok : rest) restArgs = renderStmtToken tok : go rest restArgs
-
-        renderStmtToken :: Token -> StmtMathFragments
-        renderStmtToken = \case
-            Word w -> stmtMathProse w
-            tok -> stmtMathNode (renderMathToken tok)
-
-
-renderFormulaMath :: HintMap -> Formula -> Html ()
-renderFormulaMath hints = \case
-    FormulaChain chain ->
-        renderChainMathRow hints chain
-    FormulaPredicate _loc predi marker exprs ->
-        renderHintedMathRow hints PredicateHint marker (toList exprs) (renderPrefixPredicateFallback predi (renderExprMath hints <$> toList exprs))
-    Connected _loc conn phi psi -> do
-        renderFormulaMath hints phi
-        moText (connectiveSymbol conn)
-        renderFormulaMath hints psi
-    FormulaNeg _loc phi -> do
-        moText "¬"
-        renderFormulaMath hints phi
-    FormulaQuantified _loc quant vars bound phi -> do
-        moText (quantifierSymbol quant)
-        renderVarListMath vars
-        renderBoundMath hints vars bound
-        moText "."
-        renderFormulaMath hints phi
-    PropositionalConstant _loc pc ->
-        moText (propositionalConstantSymbol pc)
-
-connectiveSymbol :: Connective -> Text
-connectiveSymbol = \case
-    Conjunction -> "∧"
-    Disjunction -> "∨"
-    Implication -> "⇒"
-    Equivalence -> "⇔"
-    ExclusiveOr -> "⊕"
-    NegatedDisjunction -> "↓"
-
-quantifierSymbol :: Quantifier -> Text
-quantifierSymbol = \case
-    Universally -> "∀"
-    Existentially -> "∃"
-    Nonexistentially -> "∄"
-
-propositionalConstantSymbol :: PropositionalConstant -> Text
-propositionalConstantSymbol = \case
-    IsBottom -> "⊥"
-    IsTop -> "⊤"
-
-renderChainMathRow :: HintMap -> Chain -> Html ()
-renderChainMathRow hints chain =
-    joinHtml (moText "∧") (renderLink <$> splatChain chain)
-    where
-        renderLink (lhs, sign, rel, rhs) =
-            renderRelationApplication hints sign (toList lhs) rel (toList rhs)
-
-        splatChain :: Chain -> [(NonEmpty Expr, Sign, Relation, NonEmpty Expr)]
-        splatChain = \case
-            ChainBase es sign rel es' ->
-                [(es, sign, rel, es')]
-            ChainCons es sign rel ch'@(ChainBase es' _ _ _) ->
-                (es, sign, rel, es') : splatChain ch'
-            ChainCons es sign rel ch'@(ChainCons es' _ _ _) ->
-                (es, sign, rel, es') : splatChain ch'
-
-renderBoundMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
-renderBoundMath hints vars = \case
-    Unbounded -> skip
-    Bounded _loc sign rel expr -> do
-        moText ","
-        renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr]
-
-renderRelationApplication :: HintMap -> Sign -> [Expr] -> Relation -> [Expr] -> Html ()
-renderRelationApplication hints sign lhs rel rhs = case (sign, rel) of
-    (Negative, Relation _loc symbol [])
-        | Just negated <- negatedRelationSymbol (relationSymbolToken symbol) -> do
-            renderExprListMath hints lhs
-            moText negated
-            renderExprListMath hints rhs
-    _ ->
-        applySign sign (renderRelationCore hints lhs rel rhs)
-
-applySign :: Sign -> Html () -> Html ()
-applySign sign html = case sign of
-    Positive -> html
-    Negative -> do
-        mo_ "¬"
-        html
-
-renderRelationCore :: HintMap -> [Expr] -> Relation -> [Expr] -> Html ()
-renderRelationCore hints lhs rel rhs = case rel of
-    Relation _loc symbol relParams -> do
-        renderExprListMath hints lhs
-        renderRelationSymbolCore hints symbol relParams
-        renderExprListMath hints rhs
-    RelationExpr _loc expr -> do
-        renderExprListMath hints lhs
-        renderExprMath hints expr
-        renderExprListMath hints rhs
-
-renderRelationSymbolCore :: HintMap -> RelationSymbol -> [Expr] -> Html ()
-renderRelationSymbolCore hints symbol relParams =
-    renderHintedMathRow
-        hints
-        RelationHint
-        (relationSymbolMarker symbol)
-        relParams
-        (renderRelationFallback hints symbol relParams)
-
-renderRelationFallback :: HintMap -> RelationSymbol -> [Expr] -> Html ()
-renderRelationFallback hints symbol relParams =
-    merror_ (renderRelationFallbackCore hints symbol relParams)
-
-renderRelationFallbackCore :: HintMap -> RelationSymbol -> [Expr] -> Html ()
-renderRelationFallbackCore hints symbol relParams
-    | null relParams = renderRelationToken (relationSymbolToken symbol)
-    | otherwise = msub_ do
-        renderRelationToken (relationSymbolToken symbol)
-        mrow_ (renderExprListMath hints relParams)
-
-renderRelationToken :: Token -> Html ()
-renderRelationToken = \case
-    Command "in" -> moText "∈"
-    Command "ni" -> moText "∋"
-    Command "notin" -> moText "∉"
-    Command "meets" -> moText "⋈"
-    Command "notmeets" -> moText "⋈̸"
-    Command "subset" -> moText "⊂"
-    Command "subseteq" -> moText "⊆"
-    Command "supset" -> moText "⊃"
-    Command "supseteq" -> moText "⊇"
-    Command "neq" -> moText "≠"
-    tok -> renderMathToken tok
-
-negatedRelationSymbol :: Token -> Maybe Text
-negatedRelationSymbol = \case
-    Command "in" -> Just "∉"
-    Command "ni" -> Just "∌"
-    Command "subset" -> Just "⊄"
-    Command "subseteq" -> Just "⊈"
-    Command "supset" -> Just "⊅"
-    Command "supseteq" -> Just "⊉"
-    Command "meets" -> Just "⋈̸"
-    Symbol "=" -> Just "≠"
-    Symbol "<" -> Just "≮"
-    Symbol ">" -> Just "≯"
-    Symbol "≤" -> Just "≰"
-    Symbol "≥" -> Just "≱"
-    _ -> Nothing
-
-
-renderExprMath :: HintMap -> Expr -> Html ()
-renderExprMath hints expr = case expr of
-    ExprVar var ->
-        renderVarMath var
-    ExprInteger _loc n ->
-        mnText (Text.pack (show n))
-    ExprOp _loc item args ->
-        renderHintedMath hints OperatorHint (mixfixMarker item) args (renderPatternFallback (mixfixPattern item) (renderExprMath hints <$> args))
-    ExprStructOp _loc symb maybeExpr ->
-        let marker = structMarker symb
-            args = maybeToList maybeExpr
-        in renderHintedMath hints StructOpHint marker args (renderStructFallback symb (renderExprMath hints <$> args))
-    ExprFiniteSet{} ->
-        mrow_ (renderExprMathRow hints expr)
-    ExprSep{} ->
-        mrow_ (renderExprMathRow hints expr)
-    ExprReplace{} ->
-        mrow_ (renderExprMathRow hints expr)
-    ExprReplacePred{} ->
-        mrow_ (renderExprMathRow hints expr)
-
-renderExprMathRow :: HintMap -> Expr -> Html ()
-renderExprMathRow hints = \case
-    ExprVar var ->
-        renderVarMath var
-    ExprInteger _loc n ->
-        mnText (Text.pack (show n))
-    ExprOp _loc item args ->
-        renderHintedMathRow hints OperatorHint (mixfixMarker item) args (renderPatternFallback (mixfixPattern item) (renderExprMath hints <$> args))
-    ExprStructOp _loc symb maybeExpr ->
-        let marker = structMarker symb
-            args = maybeToList maybeExpr
-        in renderHintedMathRow hints StructOpHint marker args (renderStructFallback symb (renderExprMath hints <$> args))
-    ExprFiniteSet _loc exprs ->
-        renderFiniteSetMath hints (toList exprs)
-    ExprSep _loc var bound stmt -> do
-        moText "{"
-        renderVarMath var
-        moText "∈"
-        renderExprMathRow hints bound
-        moText "|"
-        renderStmtMath hints stmt
-        moText "}"
-    ExprReplace _loc expr bounds maybeStmt -> do
-        moText "{"
-        renderExprMathRow hints expr
-        moText "|"
-        renderReplaceBoundsMath hints (toList bounds)
-        for_ maybeStmt \stmt -> do
-            moText "|"
-            renderStmtMath hints stmt
-        moText "}"
-    ExprReplacePred _loc rangeVar domVar domExpr stmt -> do
-        moText "{"
-        renderVarMath rangeVar
-        moText "|"
-        moText "∃"
-        renderVarMath domVar
-        moText "∈"
-        renderExprMathRow hints domExpr
-        moText "."
-        renderStmtMath hints stmt
-        moText "}"
-
-renderReplaceBoundsMath :: HintMap -> [(VarSymbol, Expr)] -> Html ()
-renderReplaceBoundsMath hints =
-    joinHtml (moText ",") . fmap renderBound
-    where
-        renderBound (var, expr) = do
-            renderVarMath var
-            moText "∈"
-            renderExprMathRow hints expr
-
-renderExprListMath :: HintMap -> [Expr] -> Html ()
-renderExprListMath hints =
-    joinHtml (moText ",") . fmap (renderExprMath hints)
-
-renderFiniteSetMath :: HintMap -> [Expr] -> Html ()
-renderFiniteSetMath hints exprs =
-    do
-        moText "{"
-        renderExprListMath hints exprs
-        moText "}"
-
-renderHintedMath :: HintMap -> HintCategory -> Marker -> [Expr] -> Html () -> Html ()
-renderHintedMath hints category marker args fallback =
-    case Map.lookup (category, marker, length args) hints of
-        Nothing ->
-            fallback
-        Just RenderHint{..}
-            | renderHintArity /= length args ->
-                error ("Render hint arity mismatch for " <> show category <> " " <> show marker <> ": expected " <> show renderHintArity <> ", got " <> show (length args))
-            | otherwise ->
-                renderTemplateAsNode renderHintTemplate
-    where
-        renderedArgs = renderExprMath hints <$> args
-
-        renderTemplateAsNode :: [TemplatePiece] -> Html ()
-        renderTemplateAsNode = \case
-            [piece] ->
-                renderPiece piece
-            pieces ->
-                mrow_ (traverse_ renderPiece pieces)
-
-        renderPiece :: TemplatePiece -> Html ()
-        renderPiece = \case
-            Literal text -> toHtmlRaw text
-            Slot ix -> case nth (ix - 1) renderedArgs of
-                Just html -> html
-                Nothing -> error ("Render hint slot out of bounds for " <> show marker <> ": <x" <> show ix <> "/>")
-
-renderHintedMathRow :: HintMap -> HintCategory -> Marker -> [Expr] -> Html () -> Html ()
-renderHintedMathRow hints category marker args fallback =
-    case Map.lookup (category, marker, length args) hints of
-        Nothing ->
-            fallback
-        Just RenderHint{..}
-            | renderHintArity /= length args ->
-                error ("Render hint arity mismatch for " <> show category <> " " <> show marker <> ": expected " <> show renderHintArity <> ", got " <> show (length args))
-            | otherwise ->
-                traverse_ renderPiece renderHintTemplate
-    where
-        renderedArgs = renderExprMath hints <$> args
-
-        renderPiece :: TemplatePiece -> Html ()
-        renderPiece = \case
-            Literal text -> toHtmlRaw text
-            Slot ix -> case nth (ix - 1) renderedArgs of
-                Just html -> html
-                Nothing -> error ("Render hint slot out of bounds for " <> show marker <> ": <x" <> show ix <> "/>")
-
-renderPatternFallback :: Pattern -> [Html ()] -> Html ()
-renderPatternFallback patternParts renderedArgs =
-    merror_ (renderPatternMath patternParts renderedArgs)
-
-renderPatternMath :: Pattern -> [Html ()] -> Html ()
-renderPatternMath patternParts renderedArgs =
-    traverse_ id (go patternParts renderedArgs)
-    where
-        go End [] = []
-        go End (_ : _) = error "renderPatternMath: too many arguments"
-        go (HoleCons rest) (arg : args) = arg : go rest args
-        go (HoleCons _) [] = error "renderPatternMath: not enough arguments"
-        go (TokenCons tok rest) args = renderMathToken tok : go rest args
-
-renderPrefixPredicateFallback :: PrefixPredicate -> [Html ()] -> Html ()
-renderPrefixPredicateFallback (PrefixPredicate command _arity) renderedArgs =
-        merror_ do
-        miText command
-        when (not (null renderedArgs)) do
-            moText "("
-            joinHtml (moText ",") renderedArgs
-            moText ")"
-
-renderStructFallback :: StructSymbol -> [Html ()] -> Html ()
-renderStructFallback symb renderedArgs =
-    merror_ do
-        renderStructSymbolName symb
-        when (not (null renderedArgs)) do
-            moText "("
-            joinHtml (moText ",") renderedArgs
-            moText ")"
-
-renderStructSymbolName :: StructSymbol -> Html ()
-renderStructSymbolName (StructSymbol name) = miText name
-
-structMarker :: StructSymbol -> Marker
-structMarker (StructSymbol name) = Marker name
-
-renderMathToken :: Token -> Html ()
-renderMathToken = \case
-    Word w -> miText w
-    Variable v -> renderNamedVariableMath v
-    Symbol s -> moText s
-    Integer n -> mnText (Text.pack (show n))
-    Command cmd -> miText cmd
-    Label m -> mtextText ("label:" <> m)
-    Ref ms -> mtextText ("ref:" <> Text.intercalate "," (toList ms))
-    BeginEnv env -> mtextText ("begin:" <> env)
-    EndEnv env -> mtextText ("end:" <> env)
-    ParenL -> moText "("
-    ParenR -> moText ")"
-    BracketL -> moText "["
-    BracketR -> moText "]"
-    VisibleBraceL -> moText "{"
-    VisibleBraceR -> moText "}"
-    InvisibleBraceL -> moText "("
-    InvisibleBraceR -> moText ")"
-
-
-inlineMath :: Html () -> Html ()
-inlineMath inner = math_ inner
-
-blockMath :: Html () -> Html ()
-blockMath inner = math_ [displayblock_] inner
-
-renderVarInline :: VarSymbol -> Html ()
-renderVarInline = inlineMath . renderVarMath
-
-renderVarMath :: VarSymbol -> Html ()
-renderVarMath = \case
-    NamedVarAt _loc name ->
-        renderNamedVariableMath name
-    FreshVarAt _loc n ->
-        miText ("_" <> Text.pack (show n))
-
-renderNamedVariableMath :: Text -> Html ()
-renderNamedVariableMath rawName =
-    case displayVariable rawName of
-        VariableDisplay baseText Nothing ->
-            miText baseText
-        VariableDisplay baseText (Just (VariableTicks tickCount)) ->
-            msup_ do
-                miText baseText
-                renderPrimeSuperscript tickCount
-        VariableDisplay baseText (Just (VariableSubscript subscriptText)) ->
-            msub_ do
-                miText baseText
-                renderVariableSubscriptMath subscriptText
-
-renderPrimeSuperscript :: Int -> Html ()
-renderPrimeSuperscript tickCount
-    | tickCount <= 1 =
-        moText "′"
-    | otherwise =
-        mrow_ (foldMap (const (moText "′")) [1 .. tickCount])
-
-renderVariableSubscriptMath :: Text -> Html ()
-renderVariableSubscriptMath subscriptText
-    | Text.all isDigit subscriptText =
-        mnText subscriptText
-    | otherwise =
-        miText subscriptText
-
-renderVarEqInline :: HintMap -> VarSymbol -> Expr -> Html ()
-renderVarEqInline hints var expr =
-    inlineMath do
-        renderVarMath var
-        moText "="
-        renderExprMathRow hints expr
-
-renderFunctionCallInline :: VarSymbol -> VarSymbol -> Html ()
-renderFunctionCallInline fun arg =
-    inlineMath (renderFunctionCallMath fun arg)
-
-renderFunctionEqInline :: HintMap -> VarSymbol -> VarSymbol -> Expr -> Html ()
-renderFunctionEqInline hints fun arg expr =
-    inlineMath do
-        renderFunctionCallMath fun arg
-        moText "="
-        renderExprMathRow hints expr
-
-renderFunctionCallMath :: VarSymbol -> VarSymbol -> Html ()
-renderFunctionCallMath fun arg = do
-    renderVarMath fun
-    moText "("
-    renderVarMath arg
-    moText ")"
-
-renderVarListInline :: NonEmpty VarSymbol -> Html ()
-renderVarListInline vars =
-    inlineMath (renderVarListMath vars)
-
-renderVarListMath :: NonEmpty VarSymbol -> Html ()
-renderVarListMath vars =
-    joinHtml (moText ",") (renderVarMath <$> toList vars)
-
-renderBoundInline :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
-renderBoundInline hints vars = \case
-    Unbounded -> skip
-    bound -> do
-        toHtml (" with " :: Text)
-        inlineMath (renderBoundPhraseMath hints vars bound)
-
-renderBoundSubjectInline :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
-renderBoundSubjectInline hints vars = \case
-    Unbounded ->
-        renderVarListInline vars
-    bound ->
-        inlineMath (renderBoundSubjectMath hints vars bound)
-
-renderBoundPhraseMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
-renderBoundPhraseMath hints vars = \case
-    Unbounded -> mrow_ skip
-    Bounded _loc sign rel expr ->
-        renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr]
-
-renderBoundSubjectMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
-renderBoundSubjectMath hints vars = \case
-    Unbounded ->
-        renderVarListMath vars
-    Bounded _loc sign rel expr ->
-        renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr]
-
-boundSubjectMathFragments :: HintMap -> NonEmpty VarSymbol -> Bound -> StmtMathFragments
-boundSubjectMathFragments hints vars = \case
-    Unbounded ->
-        stmtMathNode (renderVarListMath vars)
-    bound ->
-        stmtMathNode (renderBoundSubjectMath hints vars bound)
-
-renderSymbolPatternInline :: HintMap -> SymbolPattern -> Html ()
-renderSymbolPatternInline hints =
-    inlineMath . renderSymbolPatternMath hints
-
-renderSymbolPatternMath :: HintMap -> SymbolPattern -> Html ()
-renderSymbolPatternMath hints (SymbolPattern symbol vars) =
-    renderHintedMathRow hints OperatorHint (mixfixMarker symbol) (ExprVar <$> vars) (renderPatternFallback (mixfixPattern symbol) (renderVarMath <$> vars))
-
-renderJustification :: ReferenceContext -> Justification -> Html ()
-renderJustification references = \case
-    JustificationRef markers -> do
-        toHtml ("by " :: Text)
-        renderMarkerReferences references (toList markers)
-    JustificationSetExt ->
-        toHtml ("by set extensionality" :: Text)
-    JustificationEmpty ->
-        skip
-    JustificationLocal ->
-        toHtml ("by local assumptions" :: Text)
-
-renderJustificationSuffix :: ReferenceContext -> Justification -> Html ()
-renderJustificationSuffix _ JustificationEmpty = skip
-renderJustificationSuffix references justification = do
-    toHtml (" " :: Text)
-    renderJustification references justification
-
-renderMarkerReferences :: ReferenceContext -> [Marker] -> Html ()
-renderMarkerReferences references markers
-    | length markers >= referenceGroupThreshold =
-        renderMarkerReferenceGroup references markers
-    | otherwise =
-        joinHtml (toHtml (", " :: Text)) (renderMarkerReference references <$> markers)
-
-renderMarkerReferenceGroup :: ReferenceContext -> [Marker] -> Html ()
-renderMarkerReferenceGroup references markers =
-    span_ groupAttributes do
-        toHtml ("[...]" :: Text)
-        span_ [class_ "reference-preview-group-items", makeAttributes "hidden" "hidden"] do
-            traverse_ (renderMarkerReferenceGroupItem references) markers
-    where
-        referenceCountLabel = Text.pack (show (length markers)) <> " references"
-
-        groupAttributes =
-            [ class_ "ref-badge has-preview ref-badge-group"
-            , makeAttributes "data-preview-group" "true"
-            , makeAttributes "data-reference-label" referenceCountLabel
-            , makeAttributes "aria-describedby" "reference-preview-popup"
-            , makeAttributes "tabindex" "0"
-            , makeAttributes "role" "button"
-            , makeAttributes "aria-label" ("Show " <> referenceCountLabel)
-            ]
-
-renderMarkerReferenceGroupItem :: ReferenceContext -> Marker -> Html ()
-renderMarkerReferenceGroupItem ReferenceContext{..} marker =
-    span_ itemAttributes skip
-    where
-        label = markerText marker
-        baseAttributes =
-            [ class_ "reference-preview-group-item"
-            , makeAttributes "data-reference-label" label
-            ]
-
-        itemAttributes =
-            baseAttributes <> case Map.lookup marker referenceAnchors of
-                Just anchor ->
-                    [ makeAttributes
-                        "data-preview-link"
-                        (renderUrlFragment anchor)
-                    , makeAttributes "data-preview-target-id" anchor
-                    ]
-                Nothing ->
-                    case Map.lookup marker referencePreviews of
-                        Nothing ->
-                            []
-                        Just preview ->
-                            [ makeAttributes
-                                "data-preview-link"
-                                (previewReferenceHref preview)
-                            , makeAttributes "data-preview-id" (previewId preview)
-                            ]
-
-renderMarkerReference :: ReferenceContext -> Marker -> Html ()
-renderMarkerReference ReferenceContext{..} marker =
-    case Map.lookup marker referenceAnchors of
-        Just anchor ->
-            a_
-                ( href_ (renderUrlFragment anchor)
-                    : referenceAttributes
-                        (Just (currentPreviewAttributes anchor))
-                )
-                (toHtml label)
-        Nothing ->
-            case Map.lookup marker referencePreviews of
-                Nothing ->
-                    span_ (referenceAttributes Nothing) (toHtml label)
-                Just preview ->
-                    a_
-                        ( href_ (previewReferenceHref preview)
-                        : referenceAttributes (Just (importedPreviewAttributes preview))
-                        )
-                        (toHtml label)
-    where
-        label = markerText marker
-
-        referenceAttributes preview =
-            [ class_ (if hasPreview preview then "ref-badge has-preview" else "ref-badge")
-            , makeAttributes "data-reference-label" label
-            ]
-            <> foldMap id preview
-
-        hasPreview =
-            \case
-                Nothing -> False
-                Just _ -> True
-
-        currentPreviewAttributes anchor =
-            [ makeAttributes "data-preview-target-id" anchor
-            , makeAttributes "aria-describedby" "reference-preview-popup"
-            ]
-
-        importedPreviewAttributes entry =
-            [ makeAttributes "data-preview-id" (previewId entry)
-            , makeAttributes "aria-describedby" "reference-preview-popup"
-            ]
-
-
-markerText :: Marker -> Text
-markerText (Marker text) = text
-
-tokenTextHtml :: Token -> Html ()
-tokenTextHtml = toHtml . tokToText
-
-joinHtml :: Html () -> [Html ()] -> Html ()
-joinHtml _ [] = mempty
-joinHtml separator (x : xs) = x <> foldMap (separator <>) xs
-
-miText :: Text -> Html ()
-miText = mi_ . toHtml
-
-moText :: Text -> Html ()
-moText = mo_ . toHtml
-
-mnText :: Text -> Html ()
-mnText = mn_ . toHtml
-
-mtextText :: Text -> Html ()
-mtextText = mtext_ . toHtml
diff --git a/source/Render/Html/Context.hs b/source/Render/Html/Context.hs
deleted file mode 100644
index 151edd5..0000000
--- a/source/Render/Html/Context.hs
+++ /dev/null
@@ -1,171 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Browser-facing routing authority for one rendered HTML page.
-module Render.Html.Context
-    ( HtmlRenderEnvironment
-    , htmlRenderEnvironment
-    , HtmlRenderContext
-    , HtmlRenderContextError(..)
-    , htmlRenderContext
-    , htmlRenderContextFromEnvironment
-    , htmlCurrentSource
-    , htmlCurrentPageUrl
-    , htmlCurrentPageLabel
-    , htmlRouteNamespaces
-    , htmlSourceUrl
-    , htmlSourceLabel
-    , htmlSourcePageHref
-    , htmlSourceFragmentHref
-    , htmlSupportScriptHref
-    ) where
-
-import Base
-import Felix.Source
-import Render.Html.Layout
-
-import Control.Exception (Exception)
-import Data.Map.Strict qualified as Map
-import Data.Text qualified as Text
-
-
-data HtmlRenderContextError
-    = HtmlCurrentSourceNotRouted !ResolvedSource
-    | HtmlReferencedSourceNotRouted !ResolvedSource
-    deriving stock (Show, Eq)
-
-instance Exception HtmlRenderContextError
-
-data HtmlRenderContext = HtmlRenderContext
-    { contextCurrentSource :: !ResolvedSource
-    , contextCurrentPageUrl :: !UrlPath
-    , contextEnvironment :: !HtmlRenderEnvironment
-    }
-    deriving stock (Show, Eq)
-
-data HtmlRenderEnvironment = HtmlRenderEnvironment
-    { environmentSourceUrls :: !(Map ResolvedSource UrlPath)
-    , environmentRouteNamespaces :: !(Map SourceMountId UrlPath)
-    , environmentSupportScriptUrl :: !UrlPath
-    }
-    deriving stock (Show, Eq)
-
-htmlRenderEnvironment :: HtmlLayout -> HtmlRenderEnvironment
-htmlRenderEnvironment layout =
-    HtmlRenderEnvironment
-        { environmentSourceUrls =
-            Map.fromList
-                [ (source, routeUrlPath route)
-                | (source, route) <- htmlPageRoutes layout
-                ]
-        , environmentRouteNamespaces =
-            htmlMountUrlPrefixes layout
-        , environmentSupportScriptUrl =
-            routeUrlPath (htmlSupportScriptRoute layout)
-        }
-
-htmlRenderContext
-    :: HtmlLayout
-    -> ResolvedSource
-    -> Either HtmlRenderContextError HtmlRenderContext
-htmlRenderContext layout =
-    htmlRenderContextFromEnvironment
-        (htmlRenderEnvironment layout)
-
-htmlRenderContextFromEnvironment
-    :: HtmlRenderEnvironment
-    -> ResolvedSource
-    -> Either HtmlRenderContextError HtmlRenderContext
-htmlRenderContextFromEnvironment environment currentSource = do
-    currentPageUrl <-
-        maybe
-            (Left (HtmlCurrentSourceNotRouted currentSource))
-            Right
-            (Map.lookup
-                currentSource
-                (environmentSourceUrls environment))
-    Right
-        HtmlRenderContext
-            { contextCurrentSource = currentSource
-            , contextCurrentPageUrl = currentPageUrl
-            , contextEnvironment = environment
-            }
-
-htmlCurrentSource :: HtmlRenderContext -> ResolvedSource
-htmlCurrentSource =
-    contextCurrentSource
-
-htmlCurrentPageUrl :: HtmlRenderContext -> UrlPath
-htmlCurrentPageUrl =
-    contextCurrentPageUrl
-
-htmlCurrentPageLabel :: HtmlRenderContext -> Text
-htmlCurrentPageLabel context =
-    resolvedSourceLabel (contextCurrentSource context)
-
-htmlRouteNamespaces
-    :: HtmlRenderContext
-    -> Map SourceMountId UrlPath
-htmlRouteNamespaces =
-    environmentRouteNamespaces . contextEnvironment
-
-htmlSourceUrl
-    :: HtmlRenderContext
-    -> ResolvedSource
-    -> Either HtmlRenderContextError UrlPath
-htmlSourceUrl HtmlRenderContext{contextEnvironment} source =
-    maybe
-        (Left (HtmlReferencedSourceNotRouted source))
-        Right
-        (Map.lookup source (environmentSourceUrls contextEnvironment))
-
-htmlSourceLabel
-    :: HtmlRenderContext
-    -> ResolvedSource
-    -> Either HtmlRenderContextError Text
-htmlSourceLabel context source = do
-    _url <- htmlSourceUrl context source
-    Right (resolvedSourceLabel source)
-
-htmlSourcePageHref
-    :: HtmlRenderContext
-    -> ResolvedSource
-    -> Either HtmlRenderContextError Text
-htmlSourcePageHref context source =
-    renderRelativeUrlPath
-        (contextCurrentPageUrl context)
-        <$> htmlSourceUrl context source
-
-htmlSourceFragmentHref
-    :: HtmlRenderContext
-    -> ResolvedSource
-    -> Text
-    -> Either HtmlRenderContextError Text
-htmlSourceFragmentHref context source fragment = do
-    target <- htmlSourceUrl context source
-    let encodedFragment =
-            renderUrlFragment fragment
-    Right
-        (if target == contextCurrentPageUrl context
-            then encodedFragment
-            else
-                renderRelativeUrlPath
-                    (contextCurrentPageUrl context)
-                    target
-                    <> encodedFragment)
-
-htmlSupportScriptHref :: HtmlRenderContext -> Text
-htmlSupportScriptHref context =
-    renderRelativeUrlPath
-        (contextCurrentPageUrl context)
-        (environmentSupportScriptUrl
-            (contextEnvironment context))
-
-resolvedSourceLabel :: ResolvedSource -> Text
-resolvedSourceLabel source =
-    sourceMountIdText (resolvedSourceMount source)
-        <> ":"
-        <> Text.pack
-            (safeRelativePathFilePath
-                (resolvedSourceRelativePath source))
diff --git a/source/Render/Html/Export.hs b/source/Render/Html/Export.hs
deleted file mode 100644
index 2c747d8..0000000
--- a/source/Render/Html/Export.hs
+++ /dev/null
@@ -1,277 +0,0 @@
-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Prepare a complete HTML export from retained parsed presentation.
-module Render.Html.Export
-    ( HtmlPresentation
-    , htmlPresentationFromParsedWorkspace
-    , HtmlExportError(..)
-    , renderHtmlExportError
-    , prepareHtmlExport
-    , prepareHtmlExportWithLayout
-    , prepareHtmlExportWithLayoutFromRendererRoots
-    ) where
-
-import Base
-import Felix.Parse
-import Felix.Source
-import Render.Html qualified as Html
-import Render.Html.Context
-import Render.Html.Layout
-import Render.Html.Output
-import Syntax.Abstract (Block)
-
-import Control.Exception (Exception, IOException, displayException)
-import Control.Exception qualified as Exception
-import Data.Bifunctor (first)
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Text qualified as Text
-import Data.Text.Encoding qualified as TextEncoding
-import Data.Text.Encoding.Error (UnicodeException)
-import Data.Text.IO qualified as TextIO
-import System.Directory (doesFileExist)
-import System.FilePath.Posix ((</>))
-
-
--- | The strict, invocation-local subset of parsed presentation needed by the
--- renderer. Construction forces the complete module sequence and every page
--- shell, severing references to parser payloads, syntax interfaces, and
--- canonical cache payloads.
-data HtmlPresentation = HtmlPresentation
-    !(NonEmpty HtmlSourcePresentation)
-
-data HtmlSourcePresentation = HtmlSourcePresentation
-    !ResolvedSource
-    ![Block]
-
-htmlPresentationFromParsedWorkspace
-    :: ParsedSourceWorkspace
-    -> HtmlPresentation
-htmlPresentationFromParsedWorkspace workspace =
-    HtmlPresentation
-        (strictMapNonEmpty project parsedModules)
-  where
-    parsedModules =
-        parsedWorkspaceImportedBeforeImporter workspace
-    project parsedModule =
-        HtmlSourcePresentation
-            (parsedModuleResolved parsedModule)
-            (parsedModuleBlocks parsedModule)
-
-strictMapNonEmpty :: (a -> b) -> NonEmpty a -> NonEmpty b
-strictMapNonEmpty f (value :| values) =
-    let !firstPage = f value
-        !rest = strictMapList f values
-    in firstPage :| rest
-
-strictMapList :: (a -> b) -> [a] -> [b]
-strictMapList _ [] =
-    []
-strictMapList f (value : values) =
-    let !next = f value
-        !rest = strictMapList f values
-    in next : rest
-
-data HtmlExportError
-    = HtmlRendererDataNotFound !FilePath ![FilePath]
-    | HtmlRendererDataLookupFailed !FilePath !Text
-    | HtmlRendererDataReadFailed !FilePath !Text
-    | HtmlExportLayoutError !HtmlLayoutError
-    | HtmlExportContextError !HtmlRenderContextError
-    deriving stock (Show)
-
-instance Exception HtmlExportError
-
-renderHtmlExportError :: HtmlExportError -> Text
-renderHtmlExportError = \case
-    HtmlRendererDataNotFound requested searched ->
-        "renderer data " <> quotePath requested <> " was not found; searched "
-            <> Text.intercalate ", " (quotePath <$> searched)
-    HtmlRendererDataLookupFailed path reason ->
-        "could not locate renderer data " <> quotePath path <> ": " <> reason
-    HtmlRendererDataReadFailed path reason ->
-        "could not read renderer data " <> quotePath path <> ": " <> reason
-    HtmlExportLayoutError failure ->
-        renderHtmlLayoutError failure
-    HtmlExportContextError failure ->
-        case failure of
-            HtmlCurrentSourceNotRouted source ->
-                "current source has no HTML route: " <> sourceLabel source
-            HtmlReferencedSourceNotRouted source ->
-                "referenced source has no HTML route: " <> sourceLabel source
-  where
-    sourceLabel source =
-        sourceMountIdText (resolvedSourceMount source)
-            <> ":"
-            <> Text.pack
-                (safeRelativePathFilePath
-                    (resolvedSourceRelativePath source))
-
-    quotePath = Text.pack . show
-
-prepareHtmlExport
-    :: [(SourceMountId, [Text])]
-    -> HtmlPresentation
-    -> Text
-    -> Either HtmlExportError [PreparedHtmlArtifact]
-prepareHtmlExport
-        mountPrefixes
-        (HtmlPresentation presentation)
-        hints = do
-    let sources =
-            sourceOf <$> NonEmpty.toList presentation
-    layout <-
-        first
-            HtmlExportLayoutError
-            (layoutHtmlSources mountPrefixes sources)
-    prepareRenderedExport hints layout presentation
-  where
-    sourceOf (HtmlSourcePresentation source _blocks) =
-        source
-
-prepareHtmlExportWithLayout
-    :: HtmlLayout
-    -> HtmlPresentation
-    -> Text
-    -> Either HtmlExportError [PreparedHtmlArtifact]
-prepareHtmlExportWithLayout
-        layout
-        (HtmlPresentation presentation)
-        hints =
-    prepareRenderedExport hints layout presentation
-
-prepareHtmlExportWithLayoutFromRendererRoots
-    :: [FilePath]
-    -> HtmlLayout
-    -> HtmlPresentation
-    -> IO (Either HtmlExportError [PreparedHtmlArtifact])
-prepareHtmlExportWithLayoutFromRendererRoots roots layout presentation = do
-    hintsResult <- findAndReadRendererFile roots "lexicon.tsv"
-    pure do
-        hints <- hintsResult
-        prepareHtmlExportWithLayout layout presentation hints
-
--- Renderer data follows the established current-directory,
--- configured-library, and debug-directory lookup policy.
-findAndReadRendererFile
-    :: [FilePath]
-    -> FilePath
-    -> IO (Either HtmlExportError Text)
-findAndReadRendererFile roots path =
-    selectRendererData path ((</> path) <$> roots) >>= \case
-        Left failure -> pure (Left failure)
-        Right selectedPath -> do
-            readResult <- tryRendererRead (TextIO.readFile selectedPath)
-            pure case readResult of
-                Left reason ->
-                    Left (HtmlRendererDataReadFailed selectedPath reason)
-                Right contents -> Right contents
-
-selectRendererData
-    :: FilePath
-    -> [FilePath]
-    -> IO (Either HtmlExportError FilePath)
-selectRendererData requested candidates = go candidates
-  where
-    go = \case
-        [] -> pure (Left (HtmlRendererDataNotFound requested candidates))
-        candidate : remaining ->
-            tryRendererIO (doesFileExist candidate) >>= \case
-                Left failure ->
-                    pure
-                        (Left
-                            (HtmlRendererDataLookupFailed
-                                candidate
-                                (Text.pack (displayException failure))))
-                Right True -> pure (Right candidate)
-                Right False -> go remaining
-
-tryRendererIO :: IO value -> IO (Either IOException value)
-tryRendererIO = Exception.try
-
-tryRendererRead :: IO value -> IO (Either Text value)
-tryRendererRead action =
-    Exception.catch
-        (Exception.catch (Right <$> action) renderIOException)
-        renderUnicodeException
-  where
-    renderIOException :: IOException -> IO (Either Text value)
-    renderIOException = pure . Left . Text.pack . displayException
-
-    renderUnicodeException
-        :: UnicodeException
-        -> IO (Either Text value)
-    renderUnicodeException = pure . Left . Text.pack . displayException
-
-prepareRenderedExport
-    :: Text
-    -> HtmlLayout
-    -> NonEmpty HtmlSourcePresentation
-    -> Either HtmlExportError [PreparedHtmlArtifact]
-prepareRenderedExport hints layout presentation = do
-    let sourceBlocks =
-            (\(HtmlSourcePresentation source blocks) ->
-                (source, blocks))
-                <$> presentation
-        (unforcedRenderIndex, pages) =
-            Html.buildRenderIndex sourceBlocks
-        !renderIndex = unforcedRenderIndex
-        renderEnvironment =
-            htmlRenderEnvironment layout
-    pageArtifacts <-
-        traverse
-            (prepareSourceArtifact
-                renderEnvironment
-                layout
-                hints
-                renderIndex)
-            pages
-    let supportRoute =
-            htmlSupportScriptRoute layout
-        supportArtifact =
-            preparedHtmlArtifact
-                (routeDestination supportRoute)
-                (Right
-                    (TextEncoding.encodeUtf8
-                        Html.supportScriptAssetContents))
-        -- Page artifacts retain imported-before-importer source order.  The
-        -- singleton support asset is published deterministically afterward.
-    Right (NonEmpty.toList pageArtifacts <> [supportArtifact])
-
-prepareSourceArtifact
-    :: HtmlRenderEnvironment
-    -> HtmlLayout
-    -> Text
-    -> Html.HtmlRenderIndex
-    -> Html.HtmlPagePresentation
-    -> Either
-        HtmlExportError
-        PreparedHtmlArtifact
-prepareSourceArtifact renderEnvironment layout hints renderIndex page = do
-    let source = Html.htmlPagePresentationSource page
-    context <-
-        first
-            HtmlExportContextError
-            (htmlRenderContextFromEnvironment
-                renderEnvironment
-                source)
-    route <-
-        maybe
-            (Left
-                (HtmlExportContextError
-                    (HtmlCurrentSourceNotRouted source)))
-            Right
-            (htmlPageRoute layout source)
-    Right
-        (preparedHtmlArtifact
-            (routeDestination route)
-            (first renderHtmlExportError
-                (TextEncoding.encodeUtf8
-                    <$> first
-                        HtmlExportContextError
-                        (Html.renderDocument
-                            context
-                            hints
-                            renderIndex
-                            page))))
diff --git a/source/Render/Html/Layout.hs b/source/Render/Html/Layout.hs
deleted file mode 100644
index c26b6b5..0000000
--- a/source/Render/Html/Layout.hs
+++ /dev/null
@@ -1,602 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Pure browser and destination routing for a resolved source graph.
-module Render.Html.Layout
-    ( UrlSegment
-    , UrlSegmentError(..)
-    , urlSegment
-    , renderUrlSegment
-    , UrlPath
-    , urlPath
-    , renderUrlPath
-    , renderRelativeUrlPath
-    , renderUrlFragment
-    , HtmlRoute
-    , routeDestination
-    , routeUrlPath
-    , HtmlRouteOwner(..)
-    , HtmlUrlRouteCollision(..)
-    , HtmlDestinationRouteCollision(..)
-    , HtmlLayoutError(..)
-    , renderHtmlLayoutError
-    , HtmlLayout
-    , htmlPageRoutes
-    , htmlPageRoute
-    , htmlSupportScriptRoute
-    , htmlMountUrlPrefixes
-    , layoutHtmlSources
-    , layoutHtmlSourceGraph
-    ) where
-
-import Base
-import Felix.Source
-import Felix.Source.Graph
-
-import Control.Exception (Exception)
-import Data.Bifunctor (first)
-import Data.ByteString qualified as ByteString
-import Data.Char (chr)
-import Data.List qualified as List
-import Data.Map.Strict qualified as Map
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import Data.Text.Encoding qualified as TextEncoding
-import Data.Word (Word8)
-import System.FilePath.Posix qualified as Posix
-
-
--- | One canonical percent-encoded URL path segment.
-newtype UrlSegment = UrlSegment Text
-    deriving stock (Show, Eq, Ord)
-
-data UrlSegmentError
-    = EmptyUrlSegment
-    | DotUrlSegment !Text
-    | UrlSegmentContainsSeparator !Text
-    | UrlSegmentContainsNull !Text
-    deriving stock (Show, Eq)
-
-urlSegment :: Text -> Either UrlSegmentError UrlSegment
-urlSegment decoded
-    | Text.null decoded =
-        Left EmptyUrlSegment
-    | decoded == "." || decoded == ".." =
-        Left (DotUrlSegment decoded)
-    | "/" `Text.isInfixOf` decoded =
-        Left (UrlSegmentContainsSeparator decoded)
-    | "\0" `Text.isInfixOf` decoded =
-        Left (UrlSegmentContainsNull decoded)
-    | otherwise =
-        Right (UrlSegment (percentEncodeUtf8 decoded))
-
-renderUrlSegment :: UrlSegment -> Text
-renderUrlSegment (UrlSegment encoded) =
-    encoded
-
-
--- | A root-relative URL path. Its segments are already encoded.
-newtype UrlPath = UrlPath [UrlSegment]
-    deriving stock (Show, Eq, Ord)
-
-urlPath :: [Text] -> Either UrlSegmentError UrlPath
-urlPath =
-    fmap UrlPath . traverse urlSegment
-
-renderUrlPath :: UrlPath -> Text
-renderUrlPath (UrlPath segments) =
-    "/" <> Text.intercalate "/" (renderUrlSegment <$> segments)
-
--- | Render a target path relative to the directory of a current page.
-renderRelativeUrlPath :: UrlPath -> UrlPath -> Text
-renderRelativeUrlPath
-    (UrlPath currentPageSegments)
-    (UrlPath targetSegments) =
-        case relativeSegments of
-            [] ->
-                "."
-            _ ->
-                Text.intercalate "/" relativeSegments
-  where
-    currentDirectorySegments =
-        case reverse currentPageSegments of
-            [] ->
-                []
-            _page : directoryReversed ->
-                reverse directoryReversed
-    (remainingCurrent, remainingTarget) =
-        dropCommonPrefix currentDirectorySegments targetSegments
-    relativeSegments =
-        replicate (length remainingCurrent) ".."
-            <> (renderUrlSegment <$> remainingTarget)
-
--- | Render an exact source marker as an encoded URL fragment.
-renderUrlFragment :: Text -> Text
-renderUrlFragment marker =
-    "#" <> percentEncodeUtf8 marker
-
-
-data HtmlRoute = HtmlRoute
-    { routeDestination :: !SafeRelativePath
-    , routeUrlPath :: !UrlPath
-    }
-    deriving stock (Show, Eq)
-
-data HtmlRouteOwner
-    = HtmlPage !ResolvedSource
-    | HtmlSupportScript
-    deriving stock (Show, Eq, Ord)
-
-data HtmlUrlRouteCollision = HtmlUrlRouteCollision
-    !UrlPath
-    !(NonEmpty HtmlRouteOwner)
-    deriving stock (Show, Eq)
-
-data HtmlDestinationRouteCollision = HtmlDestinationRouteCollision
-        !SafeRelativePath
-        !(NonEmpty HtmlRouteOwner)
-    | NestedHtmlDestinationRouteCollision
-        !SafeRelativePath
-        !HtmlRouteOwner
-        !SafeRelativePath
-        !HtmlRouteOwner
-    deriving stock (Show, Eq)
-
-data HtmlLayoutError
-    = DuplicateHtmlMountId !SourceMountId
-    | InvalidHtmlMountPrefixSegment
-        !SourceMountId
-        !Text
-        !UrlSegmentError
-    | DuplicateHtmlMountPrefix
-        ![Text]
-        !(NonEmpty SourceMountId)
-    | MissingHtmlMountPrefix !SourceMountId
-    | InvalidHtmlRouteSegment
-        !HtmlRouteOwner
-        !Text
-        !UrlSegmentError
-    | InvalidHtmlRouteDestination
-        !HtmlRouteOwner
-        !FilePath
-        !RelativePathError
-    | CollidingHtmlRoutes
-        ![HtmlUrlRouteCollision]
-        ![HtmlDestinationRouteCollision]
-    deriving stock (Show, Eq)
-
-instance Exception HtmlLayoutError
-
-renderHtmlLayoutError :: HtmlLayoutError -> Text
-renderHtmlLayoutError = \case
-    DuplicateHtmlMountId mount ->
-        "HTML mount is configured more than once: "
-            <> quoteText (sourceMountIdText mount)
-    InvalidHtmlMountPrefixSegment mount segment _problem ->
-        "HTML mount " <> quoteText (sourceMountIdText mount)
-            <> " has invalid route segment " <> quoteText segment
-    DuplicateHtmlMountPrefix prefix mounts ->
-        "HTML route prefix " <> quoteText (Text.intercalate "/" prefix)
-            <> " is shared by mounts "
-            <> Text.intercalate ", "
-                (quoteText . sourceMountIdText <$> toList mounts)
-    MissingHtmlMountPrefix mount ->
-        "no HTML route prefix is configured for mount "
-            <> quoteText (sourceMountIdText mount)
-    InvalidHtmlRouteSegment owner segment _problem ->
-        renderOwner owner <> " has invalid route segment " <> quoteText segment
-    InvalidHtmlRouteDestination owner path _problem ->
-        renderOwner owner <> " has invalid HTML destination " <> quotePath path
-    CollidingHtmlRoutes urlCollisions destinationCollisions ->
-        "HTML routes collide: "
-            <> Text.intercalate "; "
-                ( (renderUrlCollision <$> urlCollisions)
-                    <> (renderDestinationCollision <$> destinationCollisions)
-                )
-  where
-    renderUrlCollision (HtmlUrlRouteCollision path owners) =
-        "URL " <> quoteText (renderUrlPath path)
-            <> " is owned by "
-            <> Text.intercalate ", " (renderOwner <$> toList owners)
-
-    renderDestinationCollision
-            (HtmlDestinationRouteCollision path owners) =
-        "destination "
-            <> quotePath (safeRelativePathFilePath path)
-            <> " is owned by "
-            <> Text.intercalate ", " (renderOwner <$> toList owners)
-    renderDestinationCollision
-            (NestedHtmlDestinationRouteCollision
-                ancestor ancestorOwner descendant descendantOwner) =
-        "destination " <> quotePath (safeRelativePathFilePath ancestor)
-            <> " for " <> renderOwner ancestorOwner
-            <> " is an ancestor of "
-            <> quotePath (safeRelativePathFilePath descendant)
-            <> " for " <> renderOwner descendantOwner
-
-renderOwner :: HtmlRouteOwner -> Text
-renderOwner = \case
-    HtmlPage source ->
-        "page "
-            <> quoteText
-                (sourceMountIdText (resolvedSourceMount source)
-                    <> ":"
-                    <> Text.pack
-                        (safeRelativePathFilePath
-                            (resolvedSourceRelativePath source)))
-    HtmlSupportScript ->
-        "support script"
-
-quotePath :: FilePath -> Text
-quotePath = Text.pack . show
-
-quoteText :: Text -> Text
-quoteText = Text.pack . show
-
-data HtmlLayout = HtmlLayout
-    !(Map ResolvedSource HtmlRoute)
-    !HtmlRoute
-    !(Map SourceMountId UrlPath)
-    deriving stock (Show, Eq)
-
-htmlPageRoutes :: HtmlLayout -> [(ResolvedSource, HtmlRoute)]
-htmlPageRoutes (HtmlLayout routes _supportScript _mountPrefixes) =
-    Map.toAscList routes
-
-htmlPageRoute :: HtmlLayout -> ResolvedSource -> Maybe HtmlRoute
-htmlPageRoute (HtmlLayout routes _supportScript _mountPrefixes) source =
-    Map.lookup source routes
-
-htmlSupportScriptRoute :: HtmlLayout -> HtmlRoute
-htmlSupportScriptRoute (HtmlLayout _routes supportScript _mountPrefixes) =
-    supportScript
-
-htmlMountUrlPrefixes :: HtmlLayout -> Map SourceMountId UrlPath
-htmlMountUrlPrefixes (HtmlLayout _routes _supportScript mountPrefixes) =
-    mountPrefixes
-
-
-data ValidatedMountPrefix = ValidatedMountPrefix
-    ![Text]
-    ![UrlSegment]
-
-layoutHtmlSourceGraph
-    :: [(SourceMountId, [Text])]
-    -> ResolvedSourceGraph
-    -> Either HtmlLayoutError HtmlLayout
-layoutHtmlSourceGraph specifications graph =
-    layoutHtmlSources
-        specifications
-        (sourceNodeResolved <$> sourceGraphNodes graph)
-
-layoutHtmlSources
-    :: [(SourceMountId, [Text])]
-    -> [ResolvedSource]
-    -> Either HtmlLayoutError HtmlLayout
-layoutHtmlSources specifications inputSources = do
-    prefixes <- validateMountPrefixes specifications
-    let sources =
-            List.sort
-                inputSources
-        usedMounts =
-            Set.fromList (resolvedSourceMount <$> sources)
-        missingMounts =
-            usedMounts `Set.difference` Map.keysSet prefixes
-    case Set.lookupMin missingMounts of
-        Just missing ->
-            Left (MissingHtmlMountPrefix missing)
-        Nothing -> do
-            pageEntries <-
-                traverse
-                    (makePageRoute prefixes)
-                    sources
-            encodedSupportScript <-
-                encodeRouteSegments
-                    HtmlSupportScript
-                    supportScriptAssetComponents
-            supportScript <-
-                makeRoute
-                    HtmlSupportScript
-                    supportScriptAssetComponents
-                    encodedSupportScript
-            let ownedRoutes =
-                    (HtmlSupportScript, supportScript)
-                        : [ (HtmlPage source, route)
-                          | (source, route) <- pageEntries
-                          ]
-                urlCollisions =
-                    collectUrlCollisions ownedRoutes
-                destinationCollisions =
-                    collectDestinationCollisions ownedRoutes
-                        <> collectNestedDestinationCollisions ownedRoutes
-            if null urlCollisions && null destinationCollisions
-                then
-                    Right
-                        (HtmlLayout
-                            (Map.fromList pageEntries)
-                            supportScript
-                            (Map.map
-                                (\(ValidatedMountPrefix _decoded encoded) ->
-                                    UrlPath encoded)
-                                prefixes))
-                else
-                    Left
-                        (CollidingHtmlRoutes
-                            urlCollisions
-                            destinationCollisions)
-
-validateMountPrefixes
-    :: [(SourceMountId, [Text])]
-    -> Either HtmlLayoutError (Map SourceMountId ValidatedMountPrefix)
-validateMountPrefixes specifications =
-    case duplicateValues (fst <$> specifications) of
-        duplicate : _ ->
-            Left (DuplicateHtmlMountId duplicate)
-        [] -> do
-            validated <- traverse validatePrefix (List.sort specifications)
-            case duplicatePrefixGroups validated of
-                duplicate : _ ->
-                    Left duplicate
-                [] ->
-                    Right
-                        (Map.fromList
-                            [ (mount, prefix)
-                            | (mount, _decoded, prefix) <- validated
-                            ])
-  where
-    validatePrefix (mount, decoded) = do
-        encoded <- traverse
-            (\segment ->
-                first
-                    (InvalidHtmlMountPrefixSegment mount segment)
-                    (urlSegment segment))
-            decoded
-        Right
-            ( mount
-            , decoded
-            , ValidatedMountPrefix decoded encoded
-            )
-
-duplicatePrefixGroups
-    :: [(SourceMountId, [Text], ValidatedMountPrefix)]
-    -> [HtmlLayoutError]
-duplicatePrefixGroups validated =
-    [ DuplicateHtmlMountPrefix prefix (firstMount :| otherMounts)
-    | (prefix, mounts) <-
-        Map.toAscList
-            (Map.fromListWith (<>)
-                [ (decoded, [mount])
-                | (mount, decoded, _prefix) <- validated
-                ])
-    , firstMount : secondMount : remainingMounts <-
-        [List.sort mounts]
-    , let otherMounts = secondMount : remainingMounts
-    ]
-
-duplicateValues :: Ord a => [a] -> [a]
-duplicateValues values =
-    [ value
-    | (value, multiplicity) <-
-        Map.toAscList
-            (Map.fromListWith (+)
-                [(value, 1 :: Int) | value <- values])
-    , multiplicity > 1
-    ]
-
-makePageRoute
-    :: Map SourceMountId ValidatedMountPrefix
-    -> ResolvedSource
-    -> Either HtmlLayoutError (ResolvedSource, HtmlRoute)
-makePageRoute prefixes source = do
-    prefix <- case Map.lookup (resolvedSourceMount source) prefixes of
-        Nothing ->
-            Left
-                (MissingHtmlMountPrefix
-                    (resolvedSourceMount source))
-        Just found ->
-            Right found
-    let sourceComponents =
-            Text.splitOn
-                "/"
-                (Text.pack
-                    (safeRelativePathFilePath
-                        (resolvedSourceRelativePath source)))
-        destinationComponents =
-            replaceFinalComponent
-                (\component ->
-                    dropFinalExtension component <> ".html")
-                sourceComponents
-        urlComponents =
-            replaceFinalComponent
-                dropFinalExtension
-                sourceComponents
-        ValidatedMountPrefix decodedPrefix encodedPrefix =
-            prefix
-        owner = HtmlPage source
-    encodedPageComponents <-
-        encodeRouteSegments owner urlComponents
-    route <-
-        makeRoute
-            owner
-            (decodedPrefix <> destinationComponents)
-            (encodedPrefix <> encodedPageComponents)
-    Right (source, route)
-
-replaceFinalComponent :: (a -> a) -> [a] -> [a]
-replaceFinalComponent transform components =
-    case reverse components of
-        [] ->
-            []
-        final : precedingReversed ->
-            reverse precedingReversed <> [transform final]
-
-dropFinalExtension :: Text -> Text
-dropFinalExtension component =
-    case Text.breakOnEnd "." component of
-        ("", _suffix) ->
-            component
-        (".", _suffix) ->
-            component
-        (prefix, _suffix) ->
-            Text.dropEnd 1 prefix
-
-makeRoute
-    :: HtmlRouteOwner
-    -> [Text]
-    -> [UrlSegment]
-    -> Either HtmlLayoutError HtmlRoute
-makeRoute owner destinationComponents encodedUrlComponents = do
-    let destinationSpelling =
-            List.intercalate
-                "/"
-                (Text.unpack <$> destinationComponents)
-    destination <-
-        first
-            (InvalidHtmlRouteDestination
-                owner
-                destinationSpelling)
-            (safeRelativePath destinationSpelling)
-    Right
-        HtmlRoute
-            { routeDestination = destination
-            , routeUrlPath = UrlPath encodedUrlComponents
-            }
-
-encodeRouteSegments
-    :: HtmlRouteOwner
-    -> [Text]
-    -> Either HtmlLayoutError [UrlSegment]
-encodeRouteSegments owner =
-    traverse
-        (\decoded ->
-            first
-                (InvalidHtmlRouteSegment owner decoded)
-                (urlSegment decoded))
-
-collectUrlCollisions
-    :: [(HtmlRouteOwner, HtmlRoute)]
-    -> [HtmlUrlRouteCollision]
-collectUrlCollisions ownedRoutes =
-    [ HtmlUrlRouteCollision path owners
-    | (path, collidingOwners) <-
-        Map.toAscList
-            (Map.fromListWith (<>)
-                [ (routeUrlPath route, [owner])
-                | (owner, route) <- ownedRoutes
-                ])
-    , owners <-
-        collisionOwners collidingOwners
-    ]
-
-collectDestinationCollisions
-    :: [(HtmlRouteOwner, HtmlRoute)]
-    -> [HtmlDestinationRouteCollision]
-collectDestinationCollisions ownedRoutes =
-    [ HtmlDestinationRouteCollision destination owners
-    | (destination, collidingOwners) <-
-        Map.toAscList
-            (Map.fromListWith (<>)
-                [ (routeDestination route, [owner])
-                | (owner, route) <- ownedRoutes
-                ])
-    , owners <-
-        collisionOwners collidingOwners
-    ]
-
-collectNestedDestinationCollisions
-    :: [(HtmlRouteOwner, HtmlRoute)]
-    -> [HtmlDestinationRouteCollision]
-collectNestedDestinationCollisions ownedRoutes =
-    take 1
-        [ NestedHtmlDestinationRouteCollision
-            ancestor
-            ancestorOwner
-            descendant
-            descendantOwner
-        | ( (ancestorComponents, ancestor, ancestorOwner)
-            , (descendantComponents, descendant, descendantOwner)
-            ) <- zip destinations (drop 1 destinations)
-        , strictComponentPrefix ancestorComponents descendantComponents
-        ]
-  where
-    destinations =
-        List.sort
-            [ ( relativePathComponents destination
-              , destination
-              , owner
-              )
-            | (owner, route) <- ownedRoutes
-            , let destination = routeDestination route
-            ]
-
-relativePathComponents :: SafeRelativePath -> [FilePath]
-relativePathComponents =
-    Posix.splitDirectories . safeRelativePathFilePath
-
-strictComponentPrefix :: [FilePath] -> [FilePath] -> Bool
-strictComponentPrefix possibleAncestor possibleDescendant =
-    length possibleAncestor < length possibleDescendant
-        && possibleAncestor `List.isPrefixOf` possibleDescendant
-
-collisionOwners :: [HtmlRouteOwner] -> [NonEmpty HtmlRouteOwner]
-collisionOwners owners =
-    case List.sort owners of
-        firstOwner : secondOwner : rest ->
-            [firstOwner :| (secondOwner : rest)]
-        _ ->
-            []
-
-dropCommonPrefix :: Eq a => [a] -> [a] -> ([a], [a])
-dropCommonPrefix (left : lefts) (right : rights)
-    | left == right =
-        dropCommonPrefix lefts rights
-dropCommonPrefix left right =
-    (left, right)
-
-
-supportScriptAssetComponents :: [Text]
-supportScriptAssetComponents =
-    ["_static", "naproche-html.js"]
-
-percentEncodeUtf8 :: Text -> Text
-percentEncodeUtf8 =
-    Text.pack
-        . concatMap encodeByte
-        . ByteString.unpack
-        . TextEncoding.encodeUtf8
-
-encodeByte :: Word8 -> String
-encodeByte byte
-    | isUnreservedAscii byte =
-        [chr (fromIntegral byte)]
-    | otherwise =
-        [ '%'
-        , hexadecimalDigit (byte `div` 16)
-        , hexadecimalDigit (byte `mod` 16)
-        ]
-
-isUnreservedAscii :: Word8 -> Bool
-isUnreservedAscii byte =
-    isAsciiUpper byte
-        || isAsciiLower byte
-        || isAsciiDigit byte
-        || byte `elem` fmap (fromIntegral . fromEnum) ("-._~" :: String)
-
-isAsciiUpper :: Word8 -> Bool
-isAsciiUpper byte =
-    byte >= 65 && byte <= 90
-
-isAsciiLower :: Word8 -> Bool
-isAsciiLower byte =
-    byte >= 97 && byte <= 122
-
-isAsciiDigit :: Word8 -> Bool
-isAsciiDigit byte =
-    byte >= 48 && byte <= 57
-
-hexadecimalDigit :: Word8 -> Char
-hexadecimalDigit value
-    | value < 10 =
-        chr (fromIntegral value + fromEnum '0')
-    | otherwise =
-        chr (fromIntegral value - 10 + fromEnum 'A')
diff --git a/source/Render/Html/Output.hs b/source/Render/Html/Output.hs
deleted file mode 100644
index 685c83a..0000000
--- a/source/Render/Html/Output.hs
+++ /dev/null
@@ -1,471 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Confined filesystem authority for HTML output.
---
--- The output root is assumed to be user-owned and not concurrently changed by
--- a hostile actor between planning and writing. Existing parent symlinks are
--- accepted only when they resolve inside the canonical root. Final-target
--- symlinks are rejected without following them; regular generated files may be
--- replaced. This policy prevents stable-tree escapes, not TOCTOU attacks.
-module Render.Html.Output
-    ( PreparedHtmlArtifact
-    , preparedHtmlArtifact
-    , preparedHtmlArtifactDestination
-    , HtmlRoutePlan
-    , htmlRoutePlanDestinations
-    , planHtmlRoutes
-    , HtmlOutputPlan
-    , HtmlOutputError(..)
-    , renderHtmlOutputError
-    , planHtmlOutput
-    , planHtmlOutputAgainst
-    , HtmlPublicationError(..)
-    , renderHtmlPublicationError
-    , writeHtmlOutput
-    ) where
-
-import Base
-import Felix.Output.Atomic (writeBytesAtomically)
-import Felix.Source
-    ( SafeRelativePath
-    , safeRelativePathFilePath
-    )
-
-import Control.Exception (Exception, IOException, displayException)
-import Control.Exception qualified as Exception
-import Control.Monad (unless, when)
-import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
-import Data.ByteString (ByteString)
-import Data.List qualified as List
-import Data.Map.Strict qualified as Map
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import System.Directory qualified as Directory
-import System.FilePath.Posix qualified as Posix
-import System.Posix.Files qualified as PosixFiles
-
-
--- | One lazily rendered artifact.  The destination is available for complete
--- preflight without demanding the strict bytes or a renderer failure.
-data PreparedHtmlArtifact = PreparedHtmlArtifact
-    !SafeRelativePath
-    (Either Text ByteString)
-
-preparedHtmlArtifact
-    :: SafeRelativePath
-    -> Either Text ByteString
-    -> PreparedHtmlArtifact
-preparedHtmlArtifact =
-    PreparedHtmlArtifact
-
-preparedHtmlArtifactDestination
-    :: PreparedHtmlArtifact
-    -> SafeRelativePath
-preparedHtmlArtifactDestination
-        (PreparedHtmlArtifact destination _rendered) =
-    destination
-
-
--- Constructors and absolute paths stay private to this module.
-newtype HtmlRoutePlan = HtmlRoutePlan
-    [(SafeRelativePath, FilePath)]
-
-htmlRoutePlanDestinations
-    :: HtmlRoutePlan
-    -> [(SafeRelativePath, FilePath)]
-htmlRoutePlanDestinations (HtmlRoutePlan routes) =
-    routes
-
-newtype HtmlOutputPlan = HtmlOutputPlan
-    [PlannedHtmlArtifact]
-
-data PlannedHtmlArtifact = PlannedHtmlArtifact
-    !SafeRelativePath
-    !FilePath
-    (Either Text ByteString)
-
-data HtmlOutputError
-    = EmptyPreparedHtmlOutput
-    | DuplicatePreparedHtmlDestination !SafeRelativePath
-    | HtmlOutputRouteMismatch
-        ![SafeRelativePath]
-        ![SafeRelativePath]
-    | EmptyHtmlOutputRoot
-    | HtmlOutputPathInspectionFailed !FilePath !Text
-    | HtmlOutputRootNotDirectory !FilePath
-    | HtmlOutputParentNotDirectory !FilePath
-    | HtmlOutputParentEscapesRoot !FilePath !FilePath
-    | HtmlOutputTargetIsSymbolicLink !FilePath
-    | HtmlOutputTargetNotRegularFile !FilePath
-    deriving stock (Show, Eq)
-
-renderHtmlOutputError :: HtmlOutputError -> Text
-renderHtmlOutputError = \case
-    EmptyPreparedHtmlOutput ->
-        "HTML output contains no artifacts"
-    DuplicatePreparedHtmlDestination relative ->
-        "HTML output contains destination more than once: "
-            <> quoteRelative relative
-    HtmlOutputRouteMismatch planned prepared ->
-        "prepared HTML destinations do not match the reserved routes; planned "
-            <> renderRelatives planned <> ", prepared " <> renderRelatives prepared
-    EmptyHtmlOutputRoot ->
-        "HTML output root is empty"
-    HtmlOutputPathInspectionFailed path reason ->
-        "could not inspect HTML output path " <> quotePath path <> ": " <> reason
-    HtmlOutputRootNotDirectory path ->
-        "HTML output root is not a directory: " <> quotePath path
-    HtmlOutputParentNotDirectory path ->
-        "HTML output parent is not a directory: " <> quotePath path
-    HtmlOutputParentEscapesRoot root parent ->
-        "HTML output parent " <> quotePath parent
-            <> " resolves outside root " <> quotePath root
-    HtmlOutputTargetIsSymbolicLink path ->
-        "HTML output target is a symbolic link: " <> quotePath path
-    HtmlOutputTargetNotRegularFile path ->
-        "HTML output target is not a regular file: " <> quotePath path
-  where
-    renderRelatives = Text.intercalate ", " . fmap quoteRelative
-
-quoteRelative :: SafeRelativePath -> Text
-quoteRelative = quotePath . safeRelativePathFilePath
-
-quotePath :: FilePath -> Text
-quotePath = Text.pack . show
-
-instance Exception HtmlOutputError
-
--- | Validate every destination without changing the filesystem.
-planHtmlOutput
-    :: FilePath
-    -> [PreparedHtmlArtifact]
-    -> IO (Either HtmlOutputError HtmlOutputPlan)
-planHtmlOutput outputRoot artifacts = do
-    routes <- planHtmlRoutes
-        outputRoot
-        (preparedHtmlArtifactDestination <$> artifacts)
-    pure (routes >>= (`planHtmlOutputAgainst` artifacts))
-
-planHtmlRoutes
-    :: FilePath
-    -> [SafeRelativePath]
-    -> IO (Either HtmlOutputError HtmlRoutePlan)
-planHtmlRoutes outputRoot destinations =
-    runExceptT do
-        when (null destinations)
-            (throwE EmptyPreparedHtmlOutput)
-        case duplicateDestinations destinations of
-            duplicate : _ ->
-                throwE
-                    (DuplicatePreparedHtmlDestination duplicate)
-            [] ->
-                pure ()
-        when (null outputRoot) (throwE EmptyHtmlOutputRoot)
-        absoluteRoot <-
-            inspectPath
-                outputRoot
-                (Directory.makeAbsolute outputRoot)
-        rootIsLink <- inspectSymbolicLink absoluteRoot
-        rootExists <-
-            inspectPath
-                absoluteRoot
-                (Directory.doesPathExist absoluteRoot)
-        rootIsDirectory <-
-            inspectPath
-                absoluteRoot
-                (Directory.doesDirectoryExist absoluteRoot)
-        when
-            ((rootIsLink || rootExists) && not rootIsDirectory)
-            (throwE (HtmlOutputRootNotDirectory absoluteRoot))
-        canonicalRoot <-
-            inspectPath
-                absoluteRoot
-                (Directory.canonicalizePath absoluteRoot)
-        planned <- for (List.sort destinations)
-            \relative -> do
-                let components =
-                        Posix.splitDirectories
-                            (safeRelativePathFilePath relative)
-                    destination =
-                        confinedDestination
-                            absoluteRoot
-                            components
-                preflightDestination
-                    canonicalRoot
-                    absoluteRoot
-                    components
-                    destination
-                pure
-                    ( relative
-                    , destination
-                    )
-        pure (HtmlRoutePlan planned)
-
-planHtmlOutputAgainst
-    :: HtmlRoutePlan
-    -> [PreparedHtmlArtifact]
-    -> Either HtmlOutputError HtmlOutputPlan
-planHtmlOutputAgainst
-        (HtmlRoutePlan routes)
-        artifacts
-    | null artifacts =
-        Left EmptyPreparedHtmlOutput
-    | duplicate : _ <- duplicateDestinations preparedDestinations =
-        Left (DuplicatePreparedHtmlDestination duplicate)
-    | Set.fromList plannedDestinations
-        /= Set.fromList preparedDestinations =
-        Left
-            (HtmlOutputRouteMismatch
-                plannedDestinations
-                preparedDestinations)
-    | otherwise = HtmlOutputPlan <$> traverse attach artifacts
-  where
-    plannedDestinations = fst <$> routes
-    preparedDestinations =
-        preparedHtmlArtifactDestination <$> artifacts
-    routeDestinations = Map.fromList routes
-
-    attach (PreparedHtmlArtifact relative rendered) =
-        case Map.lookup relative routeDestinations of
-            Nothing ->
-                Left
-                    (HtmlOutputRouteMismatch
-                        plannedDestinations
-                        preparedDestinations)
-            Just destination ->
-                Right
-                    (PlannedHtmlArtifact
-                        relative
-                        destination
-                        rendered)
-
-duplicateDestinations
-    :: [SafeRelativePath]
-    -> [SafeRelativePath]
-duplicateDestinations destinations =
-    [ destination
-    | (destination, multiplicity) <-
-        Map.toAscList
-            (Map.fromListWith (+)
-                [ (destination, 1 :: Int)
-                | destination <- destinations
-                ])
-    , multiplicity > 1
-    ]
-
-
-data HtmlPublicationError = IncompleteHtmlPublication
-    { committedHtmlDestinations :: ![SafeRelativePath]
-    , failedHtmlDestination :: !SafeRelativePath
-    , htmlPublicationFailure :: !Text
-    }
-    deriving stock (Show, Eq)
-
-instance Exception HtmlPublicationError
-
-renderHtmlPublicationError :: HtmlPublicationError -> [Text]
-renderHtmlPublicationError failure =
-    [ "HTML publication failed at "
-        <> quoteRelative (failedHtmlDestination failure)
-        <> ": " <> htmlPublicationFailure failure
-    ]
-        <> case committedHtmlDestinations failure of
-            [] -> []
-            committed ->
-                [ "HTML files published before the failure: "
-                    <> Text.intercalate ", "
-                        (quoteRelative <$> committed)
-                ]
-
--- | Render, stage, and atomically replace each completely preflighted artifact
--- in the supplied source order.  No later artifact is rendered or staged
--- before the preceding destination has been replaced.
-writeHtmlOutput
-    :: HtmlOutputPlan
-    -> IO (Either HtmlPublicationError ())
-writeHtmlOutput (HtmlOutputPlan planned) =
-    publishAll [] planned
-
-publishAll
-    :: [SafeRelativePath]
-    -> [PlannedHtmlArtifact]
-    -> IO (Either HtmlPublicationError ())
-publishAll _committed [] =
-    pure (Right ())
-publishAll
-        committedReversed
-        (PlannedHtmlArtifact relative destination rendered : remaining) =
-    case rendered of
-        Left failure ->
-            pure
-                (Left
-                    (IncompleteHtmlPublication
-                        { committedHtmlDestinations =
-                            reverse committedReversed
-                        , failedHtmlDestination = relative
-                        , htmlPublicationFailure = failure
-                        }))
-        Right bytes -> do
-            result <-
-                tryIOException
-                    (stageAndReplace destination bytes)
-            case result of
-                Left err ->
-                    pure
-                        (Left
-                            (publicationError
-                                (reverse committedReversed)
-                                relative
-                                err))
-                Right () ->
-                    publishAll
-                        (relative : committedReversed)
-                        remaining
-
-stageAndReplace
-    :: FilePath
-    -> ByteString
-    -> IO ()
-stageAndReplace destination bytes = do
-    let directory = Posix.takeDirectory destination
-    Directory.createDirectoryIfMissing True directory
-    writeBytesAtomically destination bytes
-
-publicationError
-    :: [SafeRelativePath]
-    -> SafeRelativePath
-    -> IOException
-    -> HtmlPublicationError
-publicationError committed failed err =
-    IncompleteHtmlPublication
-        { committedHtmlDestinations = committed
-        , failedHtmlDestination = failed
-        , htmlPublicationFailure =
-            Text.pack (displayException err)
-        }
-
-tryIOException :: IO a -> IO (Either IOException a)
-tryIOException =
-    Exception.try
-
-
-preflightDestination
-    :: FilePath
-    -> FilePath
-    -> [FilePath]
-    -> FilePath
-    -> ExceptT HtmlOutputError IO ()
-preflightDestination canonicalRoot outputRoot components destination = do
-    traverse_
-        (preflightParent canonicalRoot)
-        (destinationParents outputRoot components)
-    preflightTarget destination
-
-destinationParents :: FilePath -> [FilePath] -> [FilePath]
-destinationParents root components =
-    take
-        (length components)
-        (scanl (Posix.</>) root components)
-
-confinedDestination :: FilePath -> [FilePath] -> FilePath
-confinedDestination =
-    foldl' (Posix.</>)
-
-preflightParent
-    :: FilePath
-    -> FilePath
-    -> ExceptT HtmlOutputError IO ()
-preflightParent canonicalRoot parent = do
-    parentIsLink <- inspectSymbolicLink parent
-    parentExists <-
-        inspectPath parent (Directory.doesPathExist parent)
-    parentIsDirectory <-
-        inspectPath parent (Directory.doesDirectoryExist parent)
-    when (parentIsLink || parentExists) do
-        unless
-            parentIsDirectory
-            (throwE (HtmlOutputParentNotDirectory parent))
-        canonicalParent <-
-            inspectPath
-                parent
-                (Directory.canonicalizePath parent)
-        unless
-            (isComponentwiseChild canonicalRoot canonicalParent)
-            (throwE
-                (HtmlOutputParentEscapesRoot
-                    parent
-                    canonicalParent))
-
-preflightTarget
-    :: FilePath
-    -> ExceptT HtmlOutputError IO ()
-preflightTarget target = do
-    statusResult <-
-        liftIO
-            (tryIOError
-                (PosixFiles.getSymbolicLinkStatus target))
-    case statusResult of
-        Left err
-            | isDoesNotExistError err ->
-                pure ()
-            | otherwise ->
-                throwE
-                    (HtmlOutputPathInspectionFailed
-                        target
-                        (Text.pack (displayException err)))
-        Right status
-            | PosixFiles.isSymbolicLink status ->
-                throwE
-                    (HtmlOutputTargetIsSymbolicLink target)
-            | PosixFiles.isRegularFile status ->
-                pure ()
-            | otherwise ->
-                throwE
-                    (HtmlOutputTargetNotRegularFile target)
-
-isComponentwiseChild :: FilePath -> FilePath -> Bool
-isComponentwiseChild root child =
-    canonicalComponents root
-        `List.isPrefixOf`
-            canonicalComponents child
-
-canonicalComponents :: FilePath -> [FilePath]
-canonicalComponents =
-    Posix.splitDirectories
-        . Posix.dropTrailingPathSeparator
-
-inspectSymbolicLink
-    :: FilePath
-    -> ExceptT HtmlOutputError IO Bool
-inspectSymbolicLink path = do
-    result <-
-        liftIO
-            (tryIOError
-                (Directory.pathIsSymbolicLink path))
-    case result of
-        Right isLink ->
-            pure isLink
-        Left err
-            | isDoesNotExistError err ->
-                pure False
-            | otherwise ->
-                throwE
-                    (HtmlOutputPathInspectionFailed
-                        path
-                        (Text.pack (displayException err)))
-
-inspectPath
-    :: FilePath
-    -> IO a
-    -> ExceptT HtmlOutputError IO a
-inspectPath path action = do
-    result <- liftIO (tryIOError action)
-    case result of
-        Right value ->
-            pure value
-        Left err ->
-            throwE
-                (HtmlOutputPathInspectionFailed
-                    path
-                    (Text.pack (displayException err)))