diff --git a/Main.lean b/Main.lean
index 89b32eabc..59cc3c39e 100644
--- a/Main.lean
+++ b/Main.lean
@@ -11,27 +11,24 @@ import Manual.ExtractExamples
 open Verso.Genre.Manual
 open Verso.Genre.Manual.InlineLean
 
-open Verso.Output.Html in
-def plausible := {{
+def plausible := html%{
     <script async src="https://plausible.io/js/pa-RTua_4FfKHhfAvAc3liZd.js"></script>
-    <script>{{.raw r#"
+    <script>{.raw r#"
       window.plausible=window.plausible||function(){(plausible.q=plausible.q||[]).push(arguments)},plausible.init=plausible.init||function(i){plausible.o=i||{}};
       plausible.init()
-    "#}}</script>
-  }}
+    "#}</script>
+  }
 
-open Verso.Output.Html in
-def staticJs := {{
+def staticJs := html%{
     <script src="static/metadata.js"></script>
     <script src="static/print.js"></script>
-    {{ if false then -- Flip this bit to test live links locally
-        {{ <script>"window.metadata = {'latest': true};"</script> }}
+    { if false then -- Flip this bit to test live links locally
+        html%{<script>{"window.metadata = {'latest': true};"}</script>}
       else
-        .empty }}
-  }}
+        .empty }
+  }
 
-open Verso.Output.Html in
-def staticCss := {{
+def staticCss := html%{
     <link rel="stylesheet" href="static/colors.css" />
     <link rel="stylesheet" href="static/theme.css" />
     <link rel="stylesheet" href="static/print.css" />
@@ -39,7 +36,7 @@ def staticCss := {{
     <link rel="stylesheet" href="static/fonts/source-code-pro/source-code-pro.css" />
     <link rel="stylesheet" href="static/fonts/source-sans/source-sans-3.css" />
     <link rel="stylesheet" href="static/fonts/noto-sans-mono/noto-sans-mono.css" />
-  }}
+  }
 
 def main :=
   manualMain (%doc Manual) (config := config) (extraSteps := [extractExamples])
diff --git a/Manual/BasicTypes/Fin.lean b/Manual/BasicTypes/Fin.lean
index c48eb23d1..0abe63929 100644
--- a/Manual/BasicTypes/Fin.lean
+++ b/Manual/BasicTypes/Fin.lean
@@ -157,7 +157,7 @@ Heterogeneous operators such as {lean}`Fin.natAdd` do not have corresponding het
 
 ## Bitwise Operations
 
-Typically, bitwise operations on {name}`Fin` should be accessed using Lean's overloaded bitwise operators, particularly via the instances {inst}`ShiftLeft (Fin n)`, {inst}`ShiftRight (Fin n)`, {inst}`AndOp (Fin n)`, {inst}`OrOp (Fin n)`, {inst}`Xor (Fin n)`
+Typically, bitwise operations on {name}`Fin` should be accessed using Lean's overloaded bitwise operators, particularly via the instances {inst}`ShiftLeft (Fin n)`, {inst}`ShiftRight (Fin n)`, {inst}`AndOp (Fin n)`, {inst}`OrOp (Fin n)`, {inst}`XorOp (Fin n)`
 
 {docstring Fin.shiftLeft}
 
diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean
index 88932a9bb..c6f5e7958 100644
--- a/Manual/ErrorExplanations.lean
+++ b/Manual/ErrorExplanations.lean
@@ -33,11 +33,11 @@ inline_extension Inline.errorExplanationShortName (errorName : Name) where
   extraCss := [".error-explanation-short-name { hyphenate-character: ''; }"]
   toTeX := none
   toHtml := some fun _go _id info _content =>
-    open Verso.Output Html in do
+    open Verso.Output in do
     let .ok (some errorName) := fromJson? (α := Option String) info
       | reportError "Invalid data for explanation name element"
         pure .empty
-    let html := {{ <code class="error-explanation-short-name">{{errorName}}</code> }}
+    let html := html%{<code class="error-explanation-short-name">{errorName}</code>}
     return html
 
 
diff --git a/Manual/IO/Async.lean b/Manual/IO/Async.lean
index f1a2984c9..282b9d4e4 100644
--- a/Manual/IO/Async.lean
+++ b/Manual/IO/Async.lean
@@ -1198,6 +1198,8 @@ done
 :::leanSection
 ```lean -show
 open Std.Async.IO
+open Std (Channel Broadcast)
+variable {α : Type} [Inhabited α]
 ```
 The type classes {name}`AsyncRead`, {name}`AsyncWrite`, and {name}`AsyncStream` provide buffered asynchronous I/O.
 The main {name}`AsyncRead` instances are {inst}`AsyncRead (Channel α) α`, {inst}`AsyncRead (CloseableChannel α) (Option α)`, and {inst}`AsyncRead (Broadcast.Receiver α) (Option α)`.
diff --git a/Manual/Interaction/FormatRepr.lean b/Manual/Interaction/FormatRepr.lean
index 46687d341..815391b52 100644
--- a/Manual/Interaction/FormatRepr.lean
+++ b/Manual/Interaction/FormatRepr.lean
@@ -551,6 +551,11 @@ This precedence can be used to decide whether to insert parentheses: if the prec
 tag := "repr-instance-howto"
 %%%
 
+:::leanSection
+```lean -show
+open Std (HashSet)
+variable {α : Type} [BEq α] [Hashable α] [Repr α]
+```
 Lean can produce an appropriate {name}`Repr` instance for most types automatically using {ref "deriving-instances"}[instance deriving].
 In some cases, however, it's necessary to write an instance by hand:
 
@@ -565,6 +570,7 @@ In some cases, however, it's necessary to write an instance by hand:
 
 * The derived {name}`Repr` instance for structures uses {tech}[structure instance] notation.
   A hand-written instance can use the constructor's name explicitly or use {tech}[anonymous constructor syntax].
+:::
 
 ```lean -show -keep
 /-- info: Std.HashSet.ofList [0, 3, 5] -/
diff --git a/Manual/MVCGen.lean b/Manual/MVCGen.lean
index dbb5b113b..d3c11a0a5 100644
--- a/Manual/MVCGen.lean
+++ b/Manual/MVCGen.lean
@@ -24,7 +24,6 @@ set_option linter.unusedVariables false
 set_option linter.typography.quotes true
 set_option linter.typography.dashes true
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 open Manual (comment)
@@ -131,7 +130,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -395,8 +393,8 @@ The function must be {deftech (key := "mvcgen conjunctive")}_conjunctive_, which
 ```lean -show
 variable {σ : List (Type u)} {ps : PostShape} {x y : PredTrans ps α} {Q : Assertion ps}
 ```
-The {inst}`LE PredTrans` instance is defined in terms of their logical strength; one transformer is stronger than another if the result of applying it always entails the result of applying the other.
-In other words, {lean}`∀ Q, y Q ⊢ₛ x Q`, then {lean}`x ≤ y`.
+The {inst}`LE (PredTrans ps α)` instance is defined in terms of logical strength; one transformer is stronger than another if the result of applying it always entails the result of applying the other.
+In other words, {lean}`∀ Q, y.apply Q ⊢ₛ x.apply Q`, then {lean}`x ≤ y`.
 This means that stronger predicate transformers are considered greater than weaker ones.
 :::
 
@@ -448,7 +446,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -609,7 +606,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -723,7 +719,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -761,7 +756,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -906,7 +900,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
diff --git a/Manual/Meta.lean b/Manual/Meta.lean
index 1fefe87f4..57c957185 100644
--- a/Manual/Meta.lean
+++ b/Manual/Meta.lean
@@ -170,9 +170,8 @@ div.TODO::before {
 }
 "#]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ goB _ _ content => do
-      pure {{<div class="TODO">{{← content.mapM goB}}</div>}}
+      pure html%{<div class="TODO">{← content.mapM goB}</div>}
 
 @[inline_extension TODO]
 def TODO.inlineDescr : InlineDescr where
@@ -195,9 +194,8 @@ span.TODO {
 }
 "#]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun go _ _ content => do
-      pure {{<span class="TODO">{{← content.mapM go}}</span>}}
+      pure html%{<span class="TODO">{← content.mapM go}</span>}
 
 def Block.warn : Block where
   name := `Manual.warn
@@ -219,16 +217,15 @@ def warn.descr : BlockDescr where
 .namedocs.warn > .text { border-top: none; }
 "#]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ goB _ _ content => do
-      pure {{
+      pure html%{
         <div class="namedocs warn">
-          <span class="label">"Warning"</span>
+          <span class="label">Warning</span>
           <div class="text">
-            {{← content.mapM goB}}
+            {← content.mapM goB}
           </div>
         </div>
-      }}
+      }
 
 def Inline.noVale : Inline where
   name := `Manual.noVale
@@ -254,8 +251,8 @@ meta def noVale : RoleExpander
 def noVale.descr : InlineDescr where
   traverse _ _ _ := pure none
   toTeX := none
-  toHtml := some <| fun go _ _ content => open Verso.Output.Html in do
-    pure {{<span class="no-vale">{{← content.mapM go}}</span>}}
+  toHtml := some <| fun go _ _ content => do
+    pure html%{<span class="no-vale">{← content.mapM go}</span>}
 
 structure PlannedConfig where
   issue : Option Nat
@@ -310,7 +307,6 @@ div.planned .label {
 }
 "#]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ goB _ data content => do
       let issue : Option Nat ←
         match FromJson.fromJson? (α := Option Nat × Option (Nat × String)) data with
@@ -318,21 +314,21 @@ div.planned .label {
         | .error e =>
           reportError s!"Failed to deserialize issue number from {data}: {e}"
           pure none
-      pure {{
+      pure html%{
         <div class="planned">
-          <div class="label">"Planned Content"</div>
-          {{← content.mapM goB}}
-          {{if let some issue := issue then {{
+          <div class="label">Planned Content</div>
+          {← content.mapM goB}
+          {if let some issue := issue then html%{
             <p>
-              "Tracked at issue "
-                <a href=s!"https://github.com/leanprover/reference-manual/issues/{issue}">
-                  s!"#{issue}"
+              {"Tracked at issue "}
+                <a href={s!"https://github.com/leanprover/reference-manual/issues/{issue}"}>
+                  {s!"#{issue}"}
                 </a>
             </p>
-            }} else .empty
-          }}
+            } else .empty
+          }
         </div>
-      }}
+      }
 
 @[role_expander versionString]
 meta def versionString : RoleExpander
@@ -410,8 +406,8 @@ meta def ckw : RoleExpander
 def ckw.descr : InlineDescr where
   traverse _ _ _ := pure none
   toTeX := none
-  toHtml := some fun goI _ _ content => open Verso.Output.Html in do
-    return {{<span class="c-keyword">{{← content.mapM goI}}</span>}}
+  toHtml := some fun goI _ _ content => do
+    return html%{<span class="c-keyword">{← content.mapM goI}</span>}
   extraCss :=
     [".c-keyword code { font-weight: 600; }"]
 
@@ -443,30 +439,29 @@ def ffi.descr : BlockDescr where
     pure none
   toHtml := some <| fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let .ok (_name, ffiType, signature) := FromJson.fromJson? (α := String × FFIDocType × String) info
         | do reportError "Failed to deserialize FFI doc data"; pure .empty
-      let sig : Html := {{<pre>{{signature}}</pre>}}
+      let sig : Html := html%{<pre>{signature}</pre>}
 
       let xref ← HtmlT.state
       let idAttr := xref.htmlId id
 
-      return {{
-        <div class="namedocs" {{idAttr}}>
-          <span class="label">"FFI " {{ffiType.describe}}</span>
-          <pre class="signature">{{sig}}</pre>
+      return html%{
+        <div class="namedocs" {...idAttr}>
+          <span class="label">FFI {ffiType.describe}</span>
+          <pre class="signature">{sig}</pre>
           <div class="text">
-            {{← contents.mapM goB}}
+            {← contents.mapM goB}
           </div>
         </div>
-      }}
+      }
   toTeX := some <| fun _goI goB _ _ contents =>
     contents.mapM goB -- TODO
 
-open Verso.Output.Html in
 inline_extension Inline.multiCode where
   traverse _ _ _ := pure none
-  toHtml := some <| fun goI _id _data contents => do return {{<span class="multi-code">{{← contents.mapM goI}}</span>}}
+  toHtml := some <| fun goI _id _data contents => do return html%{<span class="multi-code">{← contents.mapM goI}</span>}
   toTeX := none
 
 @[role]
diff --git a/Manual/Meta/ConfigFile.lean b/Manual/Meta/ConfigFile.lean
index 9450a22b4..ea7119474 100644
--- a/Manual/Meta/ConfigFile.lean
+++ b/Manual/Meta/ConfigFile.lean
@@ -47,7 +47,6 @@ inline_extension Inline.configFile (filename : String) where
     pure none
 
   toHtml :=
-    open Verso.Output.Html in
     open Verso.Doc.Html in
     some fun _ id data _ => do
       let .str filename := data
@@ -55,7 +54,7 @@ inline_extension Inline.configFile (filename : String) where
           pure .empty
       let xref ← HtmlT.state
       let idAttr := xref.htmlId id
-      return {{<code {{idAttr}}>{{filename}}</code>}}
+      return html%{<code {...idAttr}>{filename}</code>}
 
   toTeX := none
 
diff --git a/Manual/Meta/CustomStyle.lean b/Manual/Meta/CustomStyle.lean
index 45c7e25c4..383c73acc 100644
--- a/Manual/Meta/CustomStyle.lean
+++ b/Manual/Meta/CustomStyle.lean
@@ -23,16 +23,15 @@ block_extension Block.customCSS (css : String) where
   traverse _ _ _ := pure none
   toTeX := none
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ _ data _ => do
       match FromJson.fromJson? data with
       | .error err =>
         reportError <| "Couldn't deserialize CSS while rendering HTML: " ++ err
         pure .empty
       | .ok (css : String) =>
-        pure {{
-          <style>{{css}}</style>
-        }}
+        pure html%{
+          <style>{css}</style>
+        }
 
 @[code_block]
 meta def customCSS : CodeBlockExpanderOf Unit
diff --git a/Manual/Meta/ElanCmd.lean b/Manual/Meta/ElanCmd.lean
index 0ab56374d..8c33ea670 100644
--- a/Manual/Meta/ElanCmd.lean
+++ b/Manual/Meta/ElanCmd.lean
@@ -157,7 +157,7 @@ def elanCommand.descr : BlockDescr := withHighlighting {
 
   toHtml := some <| fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let Json.arr #[ Json.str name, aliases, spec] := info
         | do reportError s!"Failed to deserialize data while making HTML for Elan command, got {info}"; pure .empty
       let .ok (aliases : List String) := FromJson.fromJson? aliases
@@ -175,34 +175,34 @@ def elanCommand.descr : BlockDescr := withHighlighting {
       let aliasHtml : Html :=
         match aliases with
         | [] => .empty
-        | _::more => {{
+        | _::more => html%{
             <p>
-              <strong>{{if more.isEmpty then "Alias:" else "Aliases:"}}</strong>
-              " "
-              {{aliases.map (fun (a : String) => {{<code>s!"elan {a}"</code>}}) |>.intersperse {{", "}}}}
+              <strong>{if more.isEmpty then "Alias:" else "Aliases:"}</strong>
+              {" "}
+              {aliases.map (fun (a : String) => html%{<code>{s!"elan {a}"}</code>}) |>.intersperse (.text ", ")}
             </p>
-          }}
-
-      return {{
-        <div class="namedocs" {{idAttr}}>
-          {{permalink id xref false}}
-          <span class="label">"Elan command"</span>
-          <pre class="signature hl lean block" data-lean-context={{name.replace " "  "~~"}}>
-            {{← (Highlighted.seq #[elanTok, .text " ", nameTok, .text " ", spec]).toHtml (g := Verso.Genre.Manual)}}
+          }
+
+      return html%{
+        <div class="namedocs" {...idAttr}>
+          {permalink id xref false}
+          <span class="label">Elan command</span>
+          <pre class="signature hl lean block" data-lean-context={name.replace " "  "~~"}>
+            {← (Highlighted.seq #[elanTok, .text " ", nameTok, .text " ", spec]).toHtml (g := Verso.Genre.Manual)}
           </pre>
           <div class="text">
-            {{aliasHtml}}
-            {{← contents.mapM goB}}
+            {aliasHtml}
+            {← contents.mapM goB}
           </div>
         </div>
-      }}
+      }
   toTeX := none
   extraCss := [docstringStyle]
 
-  localContentItem _ info _ := open Verso.Output.Html in do
+  localContentItem _ info _ := do
     if let Json.arr #[ Json.str name, _, _] := info then
       let str := s!"elan {name}"
-      pure #[(str, {{<code>{{str}}</code>}})]
+      pure #[(str, html%{<code>{str}</code>})]
     else throw s!"Expected a three-element array with a string first, got {info}"
 }
 
@@ -228,7 +228,6 @@ def elanMeta.descr : InlineDescr := withHighlighting {
         pure <| .seq #[← go b, .raw "\n"]
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ data _ => do
       let (mName, ctx) :=
         match data with
@@ -275,7 +274,6 @@ a.elan-command:hover {
 "#
 ]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goI _ data is => do
       let (name) :=
         match data with
@@ -286,7 +284,7 @@ a.elan-command:hover {
         if let some dest := (← read).traverseState.getDomainObject? elanCommandDomain n then
           for id in dest.ids do
             if let some dest := (← read).traverseState.externalTags[id]? then
-              return {{<a href={{dest.link}} class="elan-command"><code>s!"elan {n}"</code></a>}}
+              return html%{<a href={dest.link} class="elan-command"><code>{s!"elan {n}"}</code></a>}
 
       reportError s!"No name/dest for elan command {name}"
       is.mapM goI
@@ -316,7 +314,6 @@ def elanArgs.descr : InlineDescr := withHighlighting {
   toTeX := none
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ data _ => do
       if let .arr #[hl, name] := data then
         match fromJson? (α := Highlighted) hl with
diff --git a/Manual/Meta/ElanOpt.lean b/Manual/Meta/ElanOpt.lean
index 182c919b8..5f20b5891 100644
--- a/Manual/Meta/ElanOpt.lean
+++ b/Manual/Meta/ElanOpt.lean
@@ -114,7 +114,6 @@ def elanOptDef.descr : InlineDescr where
   toTeX := none
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goB id data content => do
       let .arr #[.str name, _jsonKind, metadata] := data
         | reportError s!"Failed to deserialize metadata for Elan option def: {data}"; content.mapM goB
@@ -125,13 +124,13 @@ def elanOptDef.descr : InlineDescr where
         | reportError s!"Failed to deserialize argument metadata for Elan option def: {metadata}"; content.mapM goB
 
       if let some mv := metadata then
-        pure {{<code {{idAttr}} class="elan-opt">{{name}}" "{{mv}}</code>}}
+        pure html%{<code {...idAttr} class="elan-opt">{name}{" "}{mv}</code>}
       else
-        pure {{<code {{idAttr}} class="elan-opt">{{name}}</code>}}
+        pure html%{<code {...idAttr} class="elan-opt">{name}</code>}
 
-  localContentItem _ info _ := open Verso.Output.Html in do
+  localContentItem _ info _ := do
     if let .arr #[.str name, _jsonKind, _meta] := info then
-      pure #[(name, {{<code>{{name}}</code>}})]
+      pure #[(name, html%{<code>{name}</code>})]
     else throw s!"Expected three-element array with string first, got {info}"
 
 
@@ -158,7 +157,6 @@ def elanOpt.descr : InlineDescr where
   extraCss := [elanOptCss]
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goB _id data content => do
       let .arr #[.str name, .str original] := data
         | reportError s!"Failed to deserialize metadata for Elan option ref: {data}"; content.mapM goB
@@ -166,6 +164,6 @@ def elanOpt.descr : InlineDescr where
       if let some obj := (← read).traverseState.getDomainObject? elanOptDomain name then
         for id in obj.ids do
           if let some dest := (← read).traverseState.externalTags[id]? then
-            return {{<code class="elan-opt"><a href={{dest.link}} class="elan-command">{{name}}</a>{{original.drop name.length |>.copy}}</code>}}
+            return html%{<code class="elan-opt"><a href={dest.link} class="elan-command">{name}</a>{original.drop name.length |>.copy}</code>}
 
-      pure {{<code class="elan-opt">{{original}}</code>}}
+      pure html%{<code class="elan-opt">{original}</code>}
diff --git a/Manual/Meta/Env.lean b/Manual/Meta/Env.lean
index eb8a6e73f..e05e44e60 100644
--- a/Manual/Meta/Env.lean
+++ b/Manual/Meta/Env.lean
@@ -86,7 +86,6 @@ r#"
 ]
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ data _ => do
       let (var, isDef) ←
         match data with
@@ -98,18 +97,18 @@ r#"
           if let some dest := (← read).traverseState.externalTags[id]? then
             if isDef then
               -- TODO find an inline permalink widget that doesn't mess up text flow
-              return {{
-                  <code class="env-var" id={{dest.htmlId.toString}}>s!"{var}"</code>
-              }}
+              return html%{
+                  <code class="env-var" id={dest.htmlId.toString}>{s!"{var}"}</code>
+              }
             else
               let url := dest.link
-              return {{<code class="env-var"><a href={{url}}>s!"{var}"</a></code>}}
+              return html%{<code class="env-var"><a href={url}>{s!"{var}"}</a></code>}
 
-      return {{<code class="env-var">s!"{var}"</code>}}
+      return html%{<code class="env-var">{s!"{var}"}</code>}
 
-  localContentItem _ info _ := open Verso.Output.Html in do
+  localContentItem _ info _ := do
     if let .arr #[.str var, .bool isDef] := info then
       if isDef then
-        pure #[(var, {{<code>{{var}}</code>}}), (s!"{var} (Environment Variable)", {{<code>{{var}}</code>" (Environment Variable)"}})]
+        pure #[(var, html%{<code>{var}</code>}), (s!"{var} (Environment Variable)", html%{<code>{var}</code>{" (Environment Variable)"}})]
       else pure #[]
     else throw s!"Expected a two-element array with a string and a Boolean, got {info}"
diff --git a/Manual/Meta/ErrorExplanation/Example.lean b/Manual/Meta/ErrorExplanation/Example.lean
index c3f9ebe43..d74949995 100644
--- a/Manual/Meta/ErrorExplanation/Example.lean
+++ b/Manual/Meta/ErrorExplanation/Example.lean
@@ -107,7 +107,7 @@ window.addEventListener('DOMContentLoaded', () => {
   "#]
   toHtml := some fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
     let .ok titles := FromJson.fromJson? (α := Array String) info
       | reportError "Invalid titles JSON for example block"
         pure .empty
@@ -121,15 +121,15 @@ window.addEventListener('DOMContentLoaded', () => {
     let buttons ← titles.mapIdxM fun i (title : String) => do
       let (tabIndex, selected) := if i == 0 then ("0", "true") else ("-1", "false")
       let idxStr := toString i
-      return {{
+      return html%{
         <button type="button" role="tab"
-            aria-selected={{selected}}
-            tabindex={{tabIndex}}
-            id={{s!"{htmlId.toString}-button-{idxStr}"}}
-            aria-controls={{s!"{htmlId.toString}-panel-{idxStr}"}}>
-          {{title}}
+            aria-selected={selected}
+            tabindex={tabIndex}
+            id={s!"{htmlId.toString}-button-{idxStr}"}
+            aria-controls={s!"{htmlId.toString}-panel-{idxStr}"}>
+          {title}
         </button>
-      }}
+      }
     let panels ← contents.mapIdxM fun i b => do
       let className := "error-example-tabpanel" ++ if i == 0 then "" else " error-example-tabpanel-hidden"
       let idxStr := toString i
@@ -138,24 +138,24 @@ window.addEventListener('DOMContentLoaded', () => {
       -- z-index issues
       let panelContents ← withReader (fun ctx => { ctx with codeOptions := { ctx.codeOptions with inlineProofStates := false } } )
         (goB b)
-      return {{
+      return html%{
         <div role="tabpanel"
-            class={{className}}
-            id={{s!"{htmlId.toString}-panel-{idxStr}"}}
-            aria-labelledby={{s!"{htmlId.toString}-button-{i}"}}>
-          {{ panelContents }}
+            class={className}
+            id={s!"{htmlId.toString}-panel-{idxStr}"}
+            aria-labelledby={s!"{htmlId.toString}-button-{i}"}>
+          {panelContents}
         </div>
-      }}
-    pure {{
+      }
+    pure html%{
       <div class="error-example-container">
         <div class="error-example-tab-list" role="tablist" aria-label="Code Samples">
-          {{buttons}}
+          {buttons}
         </div>
         <div class="error-example-tab-view">
-          {{panels}}
+          {panels}
         </div>
       </div>
-    }}
+    }
 
 
 variable [Monad m] [MonadError m]
diff --git a/Manual/Meta/ErrorExplanation/Header.lean b/Manual/Meta/ErrorExplanation/Header.lean
index 6e6f65484..f7fe323fa 100644
--- a/Manual/Meta/ErrorExplanation/Header.lean
+++ b/Manual/Meta/ErrorExplanation/Header.lean
@@ -65,33 +65,33 @@ block_extension Block.errorExplanationHeader (metadata : ErrorExplanationExtende
   "]
   toHtml := some fun _goI _goB _id info _contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
     let .ok metadata := FromJson.fromJson? (α := ErrorExplanationExtendedMetadata) info
       | reportError "Failed to parse info for error explanation metadata block:\n{metadata}"
         pure .empty
     let deprecatedWarning :=
       if metadata.removedVersion?.isSome then
-        {{ <div class="error-explanation-removed-warning">
-             <p><strong>"Note: "</strong> "This diagnostic is no longer produced."</p>
-           </div> }}
+        html%{<div class="error-explanation-removed-warning">
+             <p><strong>Note: </strong>This diagnostic is no longer produced.</p>
+           </div>}
       else
         .empty
     let sevText := if metadata.severity matches .warning then "Warning" else "Error"
     let entries := #[("Severity", sevText), ("Since", metadata.sinceVersion)]
       ++ (metadata.removedVersion?.map fun v => #[("Removed", v)]).getD #[]
     let entries := entries.map fun (label, data) =>
-      {{ <span class="error-explanation-metadatum">
-           <strong>{{Html.text label}}": "</strong>
-           {{Html.text data}}
-          </span> }}
-    return {{
+      html%{<span class="error-explanation-metadatum">
+           <strong>{Html.text label}: </strong>
+           {Html.text data}
+          </span>}
+    return html%{
       <div class="error-explanation-metadata">
-        {{deprecatedWarning}}
-        <p>"Error code: "<code>{{metadata.name.toString}}</code></p>
-        <p><em>{{metadata.summary}}</em></p>
-        <p>{{entries}}</p>
+        {deprecatedWarning}
+        <p>Error code: <code>{metadata.name.toString}</code></p>
+        <p><em>{metadata.summary}</em></p>
+        <p>{entries}</p>
       </div>
-    }}
+    }
 
 structure ErrorHeaderConfig where
   name : Name
diff --git a/Manual/Meta/Example.lean b/Manual/Meta/Example.lean
index ab6e8f194..896183671 100644
--- a/Manual/Meta/Example.lean
+++ b/Manual/Meta/Example.lean
@@ -238,7 +238,6 @@ def example.descr : BlockDescr where
         pure <| .seq #[← go b, .raw "\n"]
   toHtml :=
     open Verso.Doc.Html in
-    open Verso.Output.Html in
     some <| fun goI goB id data blocks => do
       if h : blocks.size < 1 then
         reportError "Malformed example"
@@ -263,16 +262,16 @@ def example.descr : BlockDescr where
             -- This link is `display: none` hidden by default, and enabled by maybeShowLiveLinks,
             -- assuming we detect that we're a sufficiently recent version of the manual
             -- to be compatible with the versions served by https://live.lean-lang.org
-            {{ <div class="live-link"><a href={{href}}>"Live ↪"</a></div> }}
-          pure {{
-            <details class="example" {{attrs}}>
-              <summary class="description">{{← description.mapM goI}}</summary>
+            html%{<div class="live-link"><a href={href}>Live ↪</a></div>}
+          pure html%{
+            <details class="example" {...attrs}>
+              <summary class="description">{← description.mapM goI}</summary>
               <div class="example-content">
-                {{← blocks.extract 1 blocks.size |>.mapM goB}}
-                  {{liveLink}}
+                {← blocks.extract 1 blocks.size |>.mapM goB}
+                  {liveLink}
               </div>
             </details>
-          }}
+          }
   extraJs := [
 r#"function openDetailsForHashTarget() {
   // Get the current hash from the URL
@@ -423,6 +422,5 @@ def keepEnv.descr : BlockDescr where
   toTeX := none
   toHtml :=
     open Verso.Doc.Html in
-    open Verso.Output.Html in
     some <| fun _ goB _ _ blocks => do
       blocks.mapM goB
diff --git a/Manual/Meta/Executable.lean b/Manual/Meta/Executable.lean
index a9beb4368..6f2154921 100644
--- a/Manual/Meta/Executable.lean
+++ b/Manual/Meta/Executable.lean
@@ -86,7 +86,6 @@ r#"
 ]
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ data _ => do
       let (exe, isDef) ←
         match data with
@@ -97,16 +96,16 @@ r#"
         for id in dest.ids do
           if let some dest := (← read).traverseState.externalTags[id]? then
             if isDef then
-              return {{<code class="executable" id={{dest.htmlId.toString}}>s!"{exe}"</code>}}
+              return html%{<code class="executable" id={dest.htmlId.toString}>{s!"{exe}"}</code>}
             else
               let url := dest.link
-              return {{<code class="executable"><a href={{url}}>s!"{exe}"</a></code>}}
+              return html%{<code class="executable"><a href={url}>{s!"{exe}"}</a></code>}
 
-      return {{<code class="executable">s!"{exe}"</code>}}
+      return html%{<code class="executable">{s!"{exe}"}</code>}
 
-  localContentItem _ info _ := open Verso.Output.Html in do
+  localContentItem _ info _ := do
     if let .arr #[.str exe, .bool isDef] := info then
       if isDef then
-        pure #[(exe, {{<code>{{exe}}</code>}}), (s!"{exe} (Executable)", {{<code>{{exe}}</code>" (Executable)"}})]
+        pure #[(exe, html%{<code>{exe}</code>}), (s!"{exe} (Executable)", html%{<code>{exe}</code> (Executable)})]
       else pure #[]
     else throw s!"Expected a two-element array with a string and a Boolean, got {info}"
diff --git a/Manual/Meta/ExportFormat.lean b/Manual/Meta/ExportFormat.lean
index 8d47db507..46b13a242 100644
--- a/Manual/Meta/ExportFormat.lean
+++ b/Manual/Meta/ExportFormat.lean
@@ -139,7 +139,7 @@ private def registerExportType (id : InternalId) (name : String) :
   Index.addEntry id {term := Verso.Doc.Inline.concat #[.text name, .text " (export format)"]}
   modify (·.saveDomainObject exportTypeDomain name id)
 
-open Verso.Output Html in
+open Verso.Output in
 /--
 Converts highlighted export format text to HTML, linking each type name that has a description.
 -/
@@ -148,9 +148,9 @@ private def exportFormatHtml (state : TraverseState) (text : LexedText) : Html :
     | (none, txt) => (txt : Html)
     | (some "type", txt) =>
       if let some url := exportTypeLink? state txt then
-        {{<span class="type"><a href={{url}}>{{txt}}</a></span>}}
-      else {{<span class="type">{{txt}}</span>}}
-    | (some cls, txt) => {{<span class={{cls}}>{{txt}}</span>}}
+        html%{<span class="type"><a href={url}>{txt}</a></span>}
+      else html%{<span class="type">{txt}</span>}
+    | (some cls, txt) => html%{<span class={cls}>{txt}</span>}
 
 block_extension Block.exportFormat (caption : String) (value : LexedText) where
   data := toJson (caption, value)
@@ -164,17 +164,17 @@ block_extension Block.exportFormat (caption : String) (value : LexedText) where
     return none
   toTeX := none
   extraCss := [exportFormat.css]
-  toHtml := some <| fun _ _ id info _ => open Verso.Output.Html Verso.Doc.Html in do
+  toHtml := some <| fun _ _ id info _ => open Verso.Doc.Html in do
     let .ok ((caption, v) : String × LexedText) := fromJson? info
       | reportError s!"Failed to deserialize {info} as a captioned export format description"; pure .empty
     let state ← HtmlT.state
-    pure {{
-      <figure class="export-format" {{state.htmlId id}}>
-        <figcaption>{{caption}}</figcaption>
-        <pre class="export-format">{{exportFormatHtml state v}}</pre>
+    pure html%{
+      <figure class="export-format" {...state.htmlId id}>
+        <figcaption>{caption}</figcaption>
+        <pre class="export-format">{exportFormatHtml state v}</pre>
       </figure>
-    }}
-  localContentItem _ info _ := open Verso.Output.Html in do
+    }
+  localContentItem _ info _ := do
     let .ok ((caption, _) : String × LexedText) := fromJson? info
       | throw s!"Expected a caption and highlighted text, got {info}"
     let withSuffix := s!"{caption} (Export Format)"
@@ -218,29 +218,29 @@ a.export-type:hover {
 }
 "#
   ]
-  toHtml := some <| fun goI id data contents => open Verso.Output.Html Verso.Doc.Html in do
+  toHtml := some <| fun goI id data contents => open Verso.Doc.Html in do
     let .ok ((name, isDef) : String × Bool) := fromJson? data
       | reportError s!"Failed to deserialize {data} as an export format type name"; contents.mapM goI
     let state ← HtmlT.state
     -- A type named by a code literal is styled like the type names in `exportFormat` blocks, while
     -- custom link text is styled like the surrounding prose.
     let isTypeName := contents matches #[.code _]
-    let typeName (body : Html) : Html := {{<code class="export-format"><span class="type">{{body}}</span></code>}}
+    let typeName (body : Html) : Html := html%{<code class="export-format"><span class="type">{body}</span></code>}
     if isDef then
       if isTypeName then
-        return {{<span class="export-type" {{state.htmlId id}}>{{typeName name}}</span>}}
-      return {{<span class="export-type" {{state.htmlId id}}>{{← contents.mapM goI}}</span>}}
+        return html%{<span class="export-type" {...state.htmlId id}>{typeName name}</span>}
+      return html%{<span class="export-type" {...state.htmlId id}>{← contents.mapM goI}</span>}
     let some url := exportTypeLink? state name
       | reportError s!"Unknown export format type '{name}'"; contents.mapM goI
     if isTypeName then
-      return typeName {{<a href={{url}}>{{name}}</a>}}
-    pure {{<a class="export-type" href={{url}}>{{← contents.mapM goI}}</a>}}
-  localContentItem _ data _ := open Verso.Output.Html in do
+      return typeName html%{<a href={url}>{name}</a>}
+    pure html%{<a class="export-type" href={url}>{← contents.mapM goI}</a>}
+  localContentItem _ data _ := do
     let .ok ((name, isDef) : String × Bool) := fromJson? data
       | throw s!"Expected an export format type name and a Boolean, got {data}"
     if isDef then
       let withSuffix := s!"{name} (Export Format)"
-      pure #[(name, {{<code>{{name}}</code>}}), (withSuffix, {{<code>{{name}}</code>" (Export Format)"}})]
+      pure #[(name, html%{<code>{name}</code>}), (withSuffix, html%{<code>{name}</code> (Export Format)})]
     else pure #[]
 
 structure ExportTypeConfig where
@@ -277,11 +277,11 @@ inline_extension Inline.exportField (name : String) where
   traverse _ _ _ := pure none
   toTeX := none
   extraCss := [exportFormat.css]
-  toHtml := some <| fun goI _ data contents => open Verso.Output.Html in do
+  toHtml := some <| fun goI _ data contents => do
     let .ok (name : String) := fromJson? data
       | reportError s!"Failed to deserialize {data} as an export format field name"; contents.mapM goI
     -- The text is directly inside `<code>` so that the prose linter skips it.
-    pure {{<code class="export-format key">s!"\"{name}\""</code>}}
+    pure html%{<code class="export-format key">{s!"\"{name}\""}</code>}
 
 /--
 Displays the name of a field in an export format object, in the style of field names in
diff --git a/Manual/Meta/Figure.lean b/Manual/Meta/Figure.lean
index de3507ee2..cde8f5dc2 100644
--- a/Manual/Meta/Figure.lean
+++ b/Manual/Meta/Figure.lean
@@ -73,7 +73,6 @@ def figure.descr : BlockDescr where
         pure <| .seq #[← go b, .raw "\n"]
   toHtml :=
     open Verso.Doc.Html in
-    open Verso.Output.Html in
     some <| fun goI goB id _data blocks => do
       if h : blocks.size < 1 then
         reportError "Malformed figure"
@@ -83,12 +82,12 @@ def figure.descr : BlockDescr where
           | reportError "Malformed figure - caption not paragraph"; pure .empty
         let xref ← HtmlT.state
         let attrs := xref.htmlId id
-        pure {{
-          <figure {{attrs}}>
-            {{← blocks.extract 1 blocks.size |>.mapM goB}}
-            <figcaption>{{← caption.mapM goI}}</figcaption>
+        pure html%{
+          <figure {...attrs}>
+            {← blocks.extract 1 blocks.size |>.mapM goB}
+            <figcaption>{← caption.mapM goI}</figcaption>
           </figure>
-        }}
-  localContentItem _ info blocks := open Verso.Output.Html in do
+        }
+  localContentItem _ info blocks := do
     let (captionString, _, _) ← FromJson.fromJson? info (α := String × Option String × Option Tag)
-    pure #[(captionString, {{<span class="figure">{{captionString}}</span>}})]
+    pure #[(captionString, html%{<span class="figure">{captionString}</span>})]
diff --git a/Manual/Meta/GrindTactic.lean b/Manual/Meta/GrindTactic.lean
index 3d444ccd7..fab667efe 100644
--- a/Manual/Meta/GrindTactic.lean
+++ b/Manual/Meta/GrindTactic.lean
@@ -153,7 +153,7 @@ def grindTactic.descr : BlockDescr := withHighlighting {
     pure none
   toHtml := some <| fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let .ok (name, «show», docs?) := FromJson.fromJson? (α := Name × String × Option String) info
         | do reportError "Failed to deserialize grind tactic data"; pure .empty
       let x : Highlighted := .token ⟨.keyword (some name) none docs?, «show»⟩
@@ -161,19 +161,19 @@ def grindTactic.descr : BlockDescr := withHighlighting {
       let xref ← HtmlT.state
       let idAttr := xref.htmlId id
 
-      return {{
-        <div class="namedocs" {{idAttr}}>
-          {{permalink id xref false}}
-          <span class="label">"grind tactic"</span>
-          <pre class="signature hl lean block">{{← x.toHtml (g := Verso.Genre.Manual)}}</pre>
+      return html%{
+        <div class="namedocs" {...idAttr}>
+          {permalink id xref false}
+          <span class="label">grind tactic</span>
+          <pre class="signature hl lean block">{← x.toHtml (g := Verso.Genre.Manual)}</pre>
           <div class="text">
-            {{← contents.mapM goB}}
+            {← contents.mapM goB}
           </div>
         </div>
-      }}
-  localContentItem := fun _id info _contents => open Verso.Output.Html in do
+      }
+  localContentItem := fun _id info _contents => do
     let (_name, «show», _docs?) ← FromJson.fromJson? (α := Name × String × Option String) info
-    pure #[(«show», {{<code class="tactic-name">{{«show»}}</code>}})]
+    pure #[(«show», html%{<code class="tactic-name">{«show»}</code>})]
 
   toTeX := some <| fun _goI goB _id _info contents => contents.mapM goB
   extraCss := [docstringStyle]
diff --git a/Manual/Meta/LakeCmd.lean b/Manual/Meta/LakeCmd.lean
index dec0a71bd..4b6f3255b 100644
--- a/Manual/Meta/LakeCmd.lean
+++ b/Manual/Meta/LakeCmd.lean
@@ -159,7 +159,7 @@ def lakeCommand.descr : BlockDescr where
 
   toHtml := some <| fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let Json.arr #[ Json.str name, aliases, spec] := info
         | do reportError s!"Failed to deserialize data while making HTML for Lake command, got {info}"; pure .empty
       let .ok (aliases : List String) := FromJson.fromJson? aliases
@@ -177,34 +177,34 @@ def lakeCommand.descr : BlockDescr where
       let aliasHtml : Html :=
         match aliases with
         | [] => .empty
-        | _::more => {{
+        | _::more => html%{
             <p>
-              <strong>{{if more.isEmpty then "Alias:" else "Aliases:"}}</strong>
-              " "
-              {{aliases.map (fun (a : String) => {{<code>s!"lake {a}"</code>}}) |>.intersperse {{", "}}}}
+              <strong>{if more.isEmpty then "Alias:" else "Aliases:"}</strong>
+              {" "}
+              {aliases.map (fun (a : String) => html%{<code>{s!"lake {a}"}</code>}) |>.intersperse (.text ", ")}
             </p>
-          }}
-
-      return {{
-        <div class="namedocs" {{idAttr}}>
-          {{permalink id xref false}}
-          <span class="label">"Lake command"</span>
-          <pre class="signature hl lean block" data-lean-context={{name}}>
-            {{← (Highlighted.seq #[lakeTok, .text " ", nameTok, .text " ", spec]).toHtml (g := Verso.Genre.Manual)}}
+          }
+
+      return html%{
+        <div class="namedocs" {...idAttr}>
+          {permalink id xref false}
+          <span class="label">Lake command</span>
+          <pre class="signature hl lean block" data-lean-context={name}>
+            {← (Highlighted.seq #[lakeTok, .text " ", nameTok, .text " ", spec]).toHtml (g := Verso.Genre.Manual)}
           </pre>
           <div class="text">
-            {{aliasHtml}}
-            {{← contents.mapM goB}}
+            {aliasHtml}
+            {← contents.mapM goB}
           </div>
         </div>
-      }}
+      }
   toTeX := none
   extraCss := [highlightingStyle, docstringStyle]
   extraJs := [highlightingJs]
-  localContentItem _ info _ := open Verso.Output.Html in do
+  localContentItem _ info _ := do
     if let Json.arr #[ Json.str name, _, _] := info then
       let str := s!"lake {name}"
-      pure #[(str, {{<code>{{str}}</code>}})]
+      pure #[(str, html%{<code>{str}</code>})]
     else throw s!"Expected a three-element array with a string first, got {info}"
 
 @[role_expander lakeMeta]
@@ -228,7 +228,6 @@ def lakeMeta.descr : InlineDescr := withHighlighting {
       pure <| .seq <| ← content.mapM fun b => do
         pure <| .seq #[← go b, .raw "\n"]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ data _ => do
       let (mName, ctx) :=
         match data with
@@ -274,7 +273,6 @@ a.lake-command:hover {
 "#
 ]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goI _ data is => do
       let (name) :=
         match data with
@@ -285,7 +283,7 @@ a.lake-command:hover {
         if let some dest := (← read).traverseState.getDomainObject? lakeCommandDomain n then
           for id in dest.ids do
             if let some dest := (← read).traverseState.externalTags[id]? then
-              return {{<a href={{dest.link}} class="lake-command"><code>s!"lake {n}"</code></a>}}
+              return html%{<a href={dest.link} class="lake-command"><code>{s!"lake {n}"}</code></a>}
 
       reportError s!"No name for lake command in {data.compress}"
       is.mapM goI
@@ -315,7 +313,6 @@ def lakeArgs.descr : InlineDescr := withHighlighting {
   toTeX := none
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ data _ => do
       if let .arr #[hl, name] := data then
         match fromJson? (α := Highlighted) hl with
diff --git a/Manual/Meta/LakeManifest.lean b/Manual/Meta/LakeManifest.lean
index 73373b767..8828f9f56 100644
--- a/Manual/Meta/LakeManifest.lean
+++ b/Manual/Meta/LakeManifest.lean
@@ -89,10 +89,10 @@ block_extension Block.json (value : LexedText) where
   traverse _ _ _ := pure none
   toTeX := none
   extraCss := [json.css]
-  toHtml := some <| fun _ _ _ info _ => open Verso.Output.Html in do
+  toHtml := some <| fun _ _ _ info _ => do
     let .ok (v : LexedText) := fromJson? info
       | reportError s!"Failed to deserialize {info} as lexer-enhanced text"; pure .empty
-    pure {{<pre class="json">{{v.toHtml}}</pre>}}
+    pure html%{<pre class="json">{v.toHtml}</pre>}
 
 /--
 Check that contents of the block is a valid manifest file.
diff --git a/Manual/Meta/LakeOpt.lean b/Manual/Meta/LakeOpt.lean
index 0e55ffd16..2badd3c20 100644
--- a/Manual/Meta/LakeOpt.lean
+++ b/Manual/Meta/LakeOpt.lean
@@ -110,7 +110,6 @@ def lakeOptDef.descr : InlineDescr where
   toTeX := none
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goB id data content => do
       let .arr #[.str name, _jsonKind, metadata] := data
         | reportError s!"Failed to deserialize metadata for Lake option def: {data}"; content.mapM goB
@@ -121,13 +120,13 @@ def lakeOptDef.descr : InlineDescr where
         | reportError s!"Failed to deserialize argument metadata for Lake option def: {metadata}"; content.mapM goB
 
       if let some mv := metadata then
-        pure {{<code {{idAttr}} class="lake-opt">{{name}}"="{{mv}}</code>}}
+        pure html%{<code {...idAttr} class="lake-opt">{name}={mv}</code>}
       else
-        pure {{<code {{idAttr}} class="lake-opt">{{name}}</code>}}
+        pure html%{<code {...idAttr} class="lake-opt">{name}</code>}
 
-  localContentItem _ info _ := open Verso.Output.Html in do
+  localContentItem _ info _ := do
     if let .arr #[.str name, _jsonKind, _meta] := info then
-      pure #[(name, {{<code>{{name}}</code>}})]
+      pure #[(name, html%{<code>{name}</code>})]
     else throw s!"Expected three-element array with string first, got {info}"
 
 
@@ -154,7 +153,6 @@ def lakeOpt.descr : InlineDescr where
   extraCss := [lakeOptCss]
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goB _ data content => do
       let .arr #[.str name, .str original] := data
         | reportError s!"Failed to deserialize metadata for Lake option ref: {data}"; content.mapM goB
@@ -162,6 +160,6 @@ def lakeOpt.descr : InlineDescr where
       if let some obj := (← read).traverseState.getDomainObject? lakeOptDomain name then
         for id in obj.ids do
           if let some dest := (← read).traverseState.externalTags[id]? then
-            return {{<code class="lake-opt"><a href={{dest.link}} class="lake-command">{{name}}</a>{{original.drop name.length |>.copy}}</code>}}
+            return html%{<code class="lake-opt"><a href={dest.link} class="lake-command">{name}</a>{original.drop name.length |>.copy}</code>}
 
-      pure {{<code class="lake-opt">{{original}}</code>}}
+      pure html%{<code class="lake-opt">{original}</code>}
diff --git a/Manual/Meta/LakeToml.lean b/Manual/Meta/LakeToml.lean
index 6f9951450..fdce6fdfe 100644
--- a/Manual/Meta/LakeToml.lean
+++ b/Manual/Meta/LakeToml.lean
@@ -142,28 +142,28 @@ def Block.tomlField.descr : BlockDescr where
 
   toHtml := some <| fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let .ok (_, _inTable, field) := FromJson.fromJson? (α := Option Nat × Name × Toml.Field Empty) info
         | do reportError "Failed to deserialize field doc data"; pure .empty
-      let sig : Html := {{ {{field.name.toString}} }}
+      let sig : Html := field.name.toString
 
       let xref ← HtmlT.state
       let idAttr := xref.htmlId id
 
-      return {{
-        <dt {{idAttr}}>
-          <code class="field-name">{{sig}}</code>
+      return html%{
+        <dt {...idAttr}>
+          <code class="field-name">{sig}</code>
         </dt>
         <dd>
-            <p><strong>"Contains:"</strong>" " {{field.type.toHtml}}</p>
-            {{← contents.mapM goB}}
+            <p><strong>Contains:</strong> {field.type.toHtml}</p>
+            {← contents.mapM goB}
         </dd>
-      }}
-  localContentItem _ info _ := open Verso.Output Html in do
+      }
+  localContentItem _ info _ := open Verso.Output in do
     let (_, _inTable, field) ← FromJson.fromJson? (α := Option Nat × Name × Toml.Field Empty) info
     let name := field.name.toString
     pure #[
-      (name, {{<code class="field-name">{{name}}</code>}})
+      (name, html%{<code class="field-name">{name}</code>})
     ]
 
 private partial def flattenBlocks (blocks : Array (Block genre)) : Array (Block genre) :=
@@ -206,7 +206,7 @@ def Block.tomlFieldCategory.descr : BlockDescr where
 
   toHtml := some <| fun _goI goB _id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let .arr #[.str title, _fields] := info
         | do reportError "Failed to deserialize field category doc data"; pure .empty
 
@@ -215,15 +215,15 @@ def Block.tomlFieldCategory.descr : BlockDescr where
           | .other {name := `Manual.Block.tomlField, ..} _ => false
           | _ => true
 
-      return {{
+      return html%{
         <div class="field-category">
-          <p><strong>{{title}}":"</strong></p>
-          {{← nonField.mapM goB}}
+          <p><strong>{title}:</strong></p>
+          {← nonField.mapM goB}
           <dl>
-            {{← field.mapM goB}}
+            {← field.mapM goB}
           </dl>
         </div>
-      }}
+      }
 
 @[block_extension Block.tomlTable]
 def Block.tomlTable.descr : BlockDescr where
@@ -252,7 +252,7 @@ dl.toml-table-field-spec {
 
   toHtml := some <| fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let .ok (arrayKey, humanName, typeName) := FromJson.fromJson? (α := Option String × String × Name) info
         | do reportError "Failed to deserialize Lake TOML table doc data"; pure .empty
 
@@ -262,7 +262,7 @@ dl.toml-table-field-spec {
       -- Don't include links here because they'd just be self-links anyway
       let tableArrayName : Option Html := tableArrayName.map (Toml.Highlighted.toHtml (fun _ => none) (fun _ _ => none))
 
-      let sig : Html := {{ {{humanName}} {{tableArrayName.map ({{" — " <code class="toml">{{·}}</code> }}) |>.getD .empty }} }}
+      let sig : Html := html%{{humanName}{tableArrayName.map (html%{ — <code class="toml">{·}</code>}) |>.getD .empty}}
 
       let xref ← HtmlT.state
       let idAttr := xref.htmlId id
@@ -327,46 +327,46 @@ dl.toml-table-field-spec {
       let uncatHtml ← uncategorized.mapM goB
       let catHtml ← categories.mapM goB
 
-      let fieldHeader := {{
+      let fieldHeader := html%{
         <p>
           <strong>
-            {{if categories.isEmpty then "Fields:" else "Other Fields:"}}
+            {if categories.isEmpty then "Fields:" else "Other Fields:"}
           </strong>
         </p>
-      }}
+      }
 
-      let fieldHtml := {{
-        {{if categories.isEmpty then .empty else catHtml}}
-        {{if uncategorized.isEmpty then .empty
-          else {{
+      let fieldHtml := html%{
+        {if categories.isEmpty then .empty else catHtml}
+        {if uncategorized.isEmpty then .empty
+          else html%{
             <div class="field-category">
-              {{fieldHeader}}
+              {fieldHeader}
               <dl class="toml-table-field-spec">
-                {{uncatHtml}}
+                {uncatHtml}
               </dl>
             </div>
-          }}
-        }}
-      }}
-
-      return {{
-        <div class="namedocs" {{idAttr}}>
-          <span class="label">"TOML table"</span>
-          <pre class="signature">{{sig}}</pre>
+          }
+        }
+      }
+
+      return html%{
+        <div class="namedocs" {...idAttr}>
+          <span class="label">TOML table</span>
+          <pre class="signature">{sig}</pre>
           <div class="text">
-            {{← notFields.mapM goB}}
+            {← notFields.mapM goB}
 
-            {{fieldHtml}}
+            {fieldHtml}
           </div>
         </div>
-      }}
+      }
 
-  localContentItem _ info _ := open Verso.Output Html in do
+  localContentItem _ info _ := open Verso.Output in do
     let (arrayKey, humanName, typeName) ← FromJson.fromJson? (α := Option String × String × Name) info
     if let some arrayKey := arrayKey then
-      pure #[(s!"[[{arrayKey}]]", {{<code>s!"[[{arrayKey}]]"</code>}})]
+      pure #[(s!"[[{arrayKey}]]", html%{<code>{s!"[[{arrayKey}]]"}</code>})]
     else
-      pure #[(humanName, {{ {{humanName}} }})]
+      pure #[(humanName, html%{{humanName}})]
 
 
 namespace Toml
@@ -527,7 +527,6 @@ r#"
 
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goB _id data content => do
       let .ok (tableName, fieldName) := fromJson? (α := Name × Name) data
         | reportError s!"Failed to deserialize metadata for Lake option ref: {data}"; content.mapM goB
@@ -535,8 +534,8 @@ r#"
       if let some obj := (← read).traverseState.getDomainObject? tomlFieldDomain s!"{tableName} {fieldName}" then
         for id in obj.ids do
           if let some dest := (← read).traverseState.externalTags[id]? then
-            return {{<code class="toml-field"><a href={{dest.link}}>{{fieldName.toString}}</a></code>}}
+            return html%{<code class="toml-field"><a href={dest.link}>{fieldName.toString}</a></code>}
       else
         reportError s!"No link destination for TOML field {tableName}:{fieldName}"
 
-      pure {{<code class="toml-field">{{fieldName.toString}}</code>}}
+      pure html%{<code class="toml-field">{fieldName.toString}</code>}
diff --git a/Manual/Meta/LakeToml/Table.lean b/Manual/Meta/LakeToml/Table.lean
index b94af7dcb..71617fb66 100644
--- a/Manual/Meta/LakeToml/Table.lean
+++ b/Manual/Meta/LakeToml/Table.lean
@@ -57,7 +57,7 @@ where
     | .other x y z => mkCApp ``FieldType.other #[quote x, quote y, quote z]
 
 
-open Output Html in
+open Output in
 def FieldType.toHtml (plural : Bool := false) : FieldType → Html
   | .string => if plural then "strings" else "String"
   | .stringOf x => s!"{x} (as string{if plural then "s" else ""}"
@@ -71,9 +71,9 @@ def FieldType.toHtml (plural : Bool := false) : FieldType → Html
   | .option t => t.toHtml ++ " (optional)"
   | .oneOf xs =>
     let opts := xs
-      |>.map ({{<code>{{show Html from .text s!"\"{·}\""}}</code>}})
-      |>.intersperse {{", "}}
-    {{"one of " {{opts}} }}
+      |>.map (html%{<code>{show Html from .text s!"\"{·}\""}</code>})
+      |>.intersperse html%{{", "}}
+    html%{one of {opts}}
 
 structure Field (α) where
   name : Name
diff --git a/Manual/Meta/LakeToml/Toml.lean b/Manual/Meta/LakeToml/Toml.lean
index 6ce36c2f2..e224d0dd4 100644
--- a/Manual/Meta/LakeToml/Toml.lean
+++ b/Manual/Meta/LakeToml/Toml.lean
@@ -42,39 +42,39 @@ private def configPaths : Std.HashMap (List String) Name := Std.HashMap.ofList [
   (["lean_exe"], ``Lake.LeanExeConfig),
 ]
 
-open Verso Output Html in
+open Verso Output in
 partial def Highlighted.toHtml (tableLink : Name → Option String) (keyLink : Name → Name → Option String) (urlLinks : Bool := true) : Highlighted -> Html
   | .token t s =>
     match t with
-    | .bool _ => {{<span class="bool">{{s}}</span>}}
-    | .string _ => {{<span class="string">{{s}}</span>}}
-    | .num _ => {{<span class="num">{{s}}</span>}}
+    | .bool _ => html%{<span class="bool">{s}</span>}
+    | .string _ => html%{<span class="string">{s}</span>}
+    | .num _ => html%{<span class="num">{s}</span>}
   | .tableHeader hl =>
-    {{<span class="table-header">{{hl.toHtml tableLink keyLink urlLinks}}</span>}}
+    html%{<span class="table-header">{hl.toHtml tableLink keyLink urlLinks}</span>}
   | .tableName n hl =>
     let tableName := n.map (·.splitOn ".") >>= (configPaths[·]?)
     if let some dest := tableName >>= tableLink then
-      {{<a href={{dest}}>{{hl.toHtml tableLink keyLink urlLinks}}</a>}}
+      html%{<a href={dest}>{hl.toHtml tableLink keyLink urlLinks}</a>}
     else
       hl.toHtml tableLink keyLink urlLinks
-  | .tableDelim hl => {{<span class="table-delimiter">{{hl.toHtml tableLink keyLink urlLinks}}</span>}}
+  | .tableDelim hl => html%{<span class="table-delimiter">{hl.toHtml tableLink keyLink urlLinks}</span>}
   | .concat hls => .seq (hls.map (toHtml tableLink keyLink urlLinks))
   | .link url hl =>
     if urlLinks then
-      {{<a href={{url}}>{{hl.toHtml tableLink keyLink urlLinks}}</a>}}
+      html%{<a href={url}>{hl.toHtml tableLink keyLink urlLinks}</a>}
     else
       hl.toHtml tableLink keyLink urlLinks
   | .text s => s
   | .ws s =>
     let comment := s.find (· == '#')
     let commentStr := s.extract comment s.endPos
-    let commentHtml := if commentStr.isEmpty then .empty else {{<span class="comment">{{commentStr}}</span>}}
-    {{ {{s.extract s.startPos comment}} {{commentHtml}} }}
-  | .key none k => {{
+    let commentHtml := if commentStr.isEmpty then .empty else html%{<span class="comment">{commentStr}</span>}
+    html%{{s.extract s.startPos comment}{commentHtml}}
+  | .key none k => html%{
     <span class="key">
-      {{k.toHtml tableLink keyLink urlLinks}}
+      {k.toHtml tableLink keyLink urlLinks}
     </span>
-  }}
+  }
   | .key (some p) k =>
     let path := p.splitOn "."
     let dest :=
@@ -84,12 +84,12 @@ partial def Highlighted.toHtml (tableLink : Name → Option String) (keyLink : N
         else none
       else none
 
-    {{ <span class="key" data-toml-key={{p}}>
-        {{ if let some url := dest then {{
-          <a href={{url}}>{{k.toHtml tableLink keyLink urlLinks}}</a>
-        }} else k.toHtml tableLink keyLink urlLinks }}
+    html%{<span class="key" data-toml-key={p}>
+        {if let some url := dest then html%{
+          <a href={url}>{k.toHtml tableLink keyLink urlLinks}</a>
+        } else k.toHtml tableLink keyLink urlLinks}
       </span>
-    }}
+    }
 
 
 
@@ -104,13 +104,13 @@ def Inline.toml (highlighted : Toml.Highlighted) : Inline where
   data := toJson highlighted
 
 
-open Verso.Output Html in
+open Verso.Output in
 private def htmlLink (state : TraverseState) (id : InternalId) (html : Html) : Html :=
   if let some dest := state.externalTags[id]? then
-    {{<a href={{dest.link}}>{{html}}</a>}}
+    html%{<a href={dest.link}>{html}</a>}
   else html
 
-open Verso.Output Html in
+open Verso.Output in
 private def htmlDest (state : TraverseState) (id : InternalId) : Option String :=
   if let some dest := state.externalTags[id]? then
     some <| dest.link
@@ -214,17 +214,17 @@ def Block.toml.descr : BlockDescr where
 
   toHtml := some <| fun _goI _ _ info _ =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let .ok (hl, link) := FromJson.fromJson? (α := Toml.Highlighted × Bool) info
         | do reportError "Failed to deserialize highlighted TOML data"; pure .empty
 
       let xref := (← read).traverseState
 
-      return {{
+      return html%{
         <pre class="toml">
-          {{hl.toHtml (Toml.tableLink xref) (Toml.fieldLink xref) link}}
+          {hl.toHtml (Toml.tableLink xref) (Toml.fieldLink xref) link}
         </pre>
-      }}
+      }
 
 @[inline_extension Inline.toml]
 def Inline.toml.descr : InlineDescr where
@@ -236,14 +236,14 @@ def Inline.toml.descr : InlineDescr where
 
   toHtml := some <| fun _ _ info _ =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let .ok hl := FromJson.fromJson? (α := Toml.Highlighted) info
         | do reportError "Failed to deserialize highlighted TOML data"; pure .empty
 
       let xref := (← read).traverseState
 
-      return {{
+      return html%{
         <code class="toml">
-          {{hl.toHtml (Toml.tableLink xref) (Toml.fieldLink xref)}}
+          {hl.toHtml (Toml.tableLink xref) (Toml.fieldLink xref)}
         </code>
-      }}
+      }
diff --git a/Manual/Meta/LexedText.lean b/Manual/Meta/LexedText.lean
index 3da7e5969..c4bb3a717 100644
--- a/Manual/Meta/LexedText.lean
+++ b/Manual/Meta/LexedText.lean
@@ -75,7 +75,7 @@ meta def C : CodeBlockExpanderOf Unit
     let toks ← LexedText.highlight hlC codeStr
     ``(Block.other (Block.c $(quote toks)) #[Block.code $(quote codeStr)])
 
-open Verso.Output Html in
+open Verso.Output in
 open Verso.Doc.Html in
 @[block_extension Block.c]
 def c.descr : BlockDescr where
@@ -84,10 +84,10 @@ def c.descr : BlockDescr where
   toHtml := some <| fun _ _ _ info _ => do
     let .ok (v : LexedText) := fromJson? info
       | reportError s!"Failed to deserialize {info} as lexer-enhanced text"; pure .empty
-    pure {{<pre class="c">{{v.toHtml}}</pre>}}
+    pure html%{<pre class="c">{v.toHtml}</pre>}
   extraCss := [c.css]
 
-open Verso.Output Html in
+open Verso.Output in
 open Verso.Doc.Html in
 @[inline_extension Inline.c]
 def c.idescr : InlineDescr where
@@ -96,7 +96,7 @@ def c.idescr : InlineDescr where
   toHtml := some <| fun _ _ info _ => do
     let .ok (v : LexedText) := fromJson? info
       | reportError s!"Failed to deserialize {info} as lexer-enhanced text"; pure .empty
-    pure {{<code class="c">{{v.toHtml}}</code>}}
+    pure html%{<code class="c">{v.toHtml}</code>}
   extraCss := [c.css]
 
 @[role C]
diff --git a/Manual/Meta/LexedText/Basic.lean b/Manual/Meta/LexedText/Basic.lean
index 4302f2d3c..4dc010382 100644
--- a/Manual/Meta/LexedText/Basic.lean
+++ b/Manual/Meta/LexedText/Basic.lean
@@ -75,11 +75,11 @@ def highlight (hl : Highlighter) (str : String) : IO LexedText := do
 def token (kind : Name) (p : ParserFn) : ParserFn :=
   nodeFn kind <| ignoreFn p
 
-open Verso.Output Html
+open Verso.Output
 
 def toHtml (text : LexedText) : Html :=
   text.content.map fun
     | (none, txt) => (txt : Html)
-    | (some cls, txt) => {{ <span class={{cls}}>{{txt}}</span>}}
+    | (some cls, txt) => html%{<span class={cls}>{txt}</span>}
 
 end LexedText
diff --git a/Manual/Meta/ListBullet.lean b/Manual/Meta/ListBullet.lean
index 4d4783d6c..494563ab4 100644
--- a/Manual/Meta/ListBullet.lean
+++ b/Manual/Meta/ListBullet.lean
@@ -37,7 +37,6 @@ def listBullet.descr : BlockDescr where
   toTeX := none
   toHtml :=
     open Verso.Doc.Html in
-    open Verso.Output.Html in
     some <| fun _goI goB _id data blocks => do
       let bullet ←
         match data with
@@ -45,9 +44,9 @@ def listBullet.descr : BlockDescr where
         | _ =>
           reportError "Invalid data for listBullet block"
           pure ""
-      pure {{
-        <div class="listBullet" style=s!"--bullet: '{bullet} ';">
-          {{← blocks.mapM goB}}
+      pure html%{
+        <div class="listBullet" style={s!"--bullet: '{bullet} ';"}>
+          {← blocks.mapM goB}
         </div>
-      }}
+      }
   extraCss := [r##".listBullet li::marker { content: var(--bullet); font-size: 1.2em; }"##]
diff --git a/Manual/Meta/Markdown.lean b/Manual/Meta/Markdown.lean
index 783cf4a45..726ce7fff 100644
--- a/Manual/Meta/Markdown.lean
+++ b/Manual/Meta/Markdown.lean
@@ -27,9 +27,8 @@ def Block.noVale.descr : BlockDescr where
   traverse _ _ _ := pure none
   toTeX := none
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ goB _ _ content => do
-      pure {{<div class="no-vale">{{← content.mapM goB}}</div>}}
+      pure html%{<div class="no-vale">{← content.mapM goB}</div>}
 
 meta section
 
diff --git a/Manual/Meta/ParserAlias.lean b/Manual/Meta/ParserAlias.lean
index 546488a1d..403954684 100644
--- a/Manual/Meta/ParserAlias.lean
+++ b/Manual/Meta/ParserAlias.lean
@@ -95,7 +95,7 @@ def parserAlias.descr : BlockDescr where
     pure none
   toHtml := some <| fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let Json.arr #[ name, declName, «show», stackSz?, autoGroupArgs, docs?, argCount] := info
         | do reportError s!"Failed to deserialize docstring data while making HTML for parser alias, expected array but got {info}"; pure .empty
 
@@ -121,28 +121,28 @@ def parserAlias.descr : BlockDescr where
 
       let arity : Html :=
         match stackSz? with
-        | some n => {{s!"Arity: {n}"}}
-        | none => {{"Arity is sum of arguments' arities"}}
+        | some n => s!"Arity: {n}"
+        | none => "Arity is sum of arguments' arities"
       let grp :=
         if autoGroupArgs then
-          some {{"Automatically wraps arguments in a " <code>"null"</code> " node unless there's exactly one"}}
+          some html%{Automatically wraps arguments in a <code>null</code> node unless there's exactly one}
         else none
       let metadata :=
         match grp with
-        | none => {{<p>{{arity}}</p>}}
-        | some g => {{<ul><li>{{arity}}</li><li>{{g}}</li></ul>}}
-
-      return {{
-        <div class="namedocs" {{idAttr}}>
-          {{permalink id xref false}}
-          <span class="label">"parser alias"</span>
-          <pre class="signature hl lean block">{{← (Highlighted.seq #[x, args]).toHtml (g := Verso.Genre.Manual)}}</pre>
+        | none => html%{<p>{arity}</p>}
+        | some g => html%{<ul><li>{arity}</li><li>{g}</li></ul>}
+
+      return html%{
+        <div class="namedocs" {...idAttr}>
+          {permalink id xref false}
+          <span class="label">parser alias</span>
+          <pre class="signature hl lean block">{← (Highlighted.seq #[x, args]).toHtml (g := Verso.Genre.Manual)}</pre>
           <div class="text">
-            {{metadata}}
-            {{← contents.mapM goB}}
+            {metadata}
+            {← contents.mapM goB}
           </div>
         </div>
-      }}
+      }
   toTeX := none
   extraCss := [highlightingStyle, docstringStyle]
   extraJs := [highlightingJs]
diff --git a/Manual/Meta/SectionNotes.lean b/Manual/Meta/SectionNotes.lean
index 9e9cd4f1d..1cc20f4c8 100644
--- a/Manual/Meta/SectionNotes.lean
+++ b/Manual/Meta/SectionNotes.lean
@@ -80,9 +80,9 @@ def sectionNote.css := r#"
 
 "#
 
-open Verso.Output Html in
+open Verso.Output in
 private def sectionNoteHtml (content : Html) : Html :=
-  {{<div class="section-note"><div class="note">{{content}}</div></div>}}
+  html%{<div class="section-note"><div class="note">{content}</div></div>}
 
 
 block_extension Block.sectionNote where
@@ -91,7 +91,6 @@ block_extension Block.sectionNote where
 
   extraCss := [sectionNote.css]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ goB _ _ content  => do
       sectionNoteHtml <$> content.mapM goB
 
@@ -107,11 +106,10 @@ block_extension Block.sectionNoteTitle where
   traverse _ _ _ := return none
   toTeX := none
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goI _ _ _ content => do
       match content with
       | #[.para xs] =>
-        return {{<h1> {{← xs.mapM goI}} </h1>}}
+        return html%{<h1>{← xs.mapM goI}</h1>}
       | _ => reportError "Malformed section note title"; return .empty
 
 @[directive]
diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean
index 32739fb55..3d37b3156 100644
--- a/Manual/Meta/Syntax.lean
+++ b/Manual/Meta/Syntax.lean
@@ -118,7 +118,7 @@ def keywordOf.descr : InlineDescr := withHighlighting {
     pure none
   toTeX := none
   toHtml :=
-    open Verso.Output Html in
+    open Verso.Output in
     some <| fun goI _ info content => do
       match FromJson.fromJson? (α := (String × Option Name × Name × Option String)) info with
       | .ok (kw, cat, kind, kindDoc) =>
@@ -132,20 +132,20 @@ def keywordOf.descr : InlineDescr := withHighlighting {
           match tgt[0]? with
           | none => html
           | some l =>
-            {{<a href={{l.href}}>{{html}}</a>}}
-        pure {{
+            html%{<a href={l.href}>{html}</a>}
+        pure html%{
           <span class="hl lean keyword-of">
             <code class="hover-info">
-              <code>{{kind.toString}} {{cat.map (" : " ++ toString ·) |>.getD ""}}</code>
-              {{if let some doc := kindDoc then
-                  {{ <span class="sep"/> <code class="docstring">{{doc}}</code>}}
+              <code>{kind.toString}{cat.map (" : " ++ toString ·) |>.getD ""}</code>
+              {if let some doc := kindDoc then
+                  html%{<span class="sep"/><code class="docstring">{doc}</code>}
                 else
                   .empty
-              }}
+              }
             </code>
-            {{addLink {{<code class="kw">{{kw}}</code>}} }}
+            {addLink html%{<code class="kw">{kw}</code>}}
           </span>
-        }}
+        }
       | .error e =>
         reportError s!"Couldn't deserialized keywordOf data: {e}"
         content.mapM goI
@@ -218,11 +218,11 @@ def keyword.descr : InlineDescr where
     pure none
   toTeX := none
   toHtml :=
-    open Verso.Output Html in
+    open Verso.Output in
     some <| fun goI _ info content => do
       let .str kw := info
         | reportError s!"Expected a JSON string for a plain keyword, got {info}"; content.mapM goI
-      pure {{<code class="plain-keyword">{{kw}}</code>}}
+      pure html%{<code class="plain-keyword">{kw}</code>}
 
   extraCss := [
 r#".plain-keyword {
@@ -462,7 +462,7 @@ def syntax.descr : BlockDescr where
       pure none
   toTeX := none
   toHtml :=
-    open Verso.Output.Html Verso.Doc.Html in
+    open Verso.Doc.Html in
     some <| fun goI goB id data content => do
       let (titleString, label) ←
         match FromJson.fromJson? (α := Option String × Name × String × Option Tag × Array Name) data with
@@ -480,17 +480,17 @@ def syntax.descr : BlockDescr where
           pure (#[], content)
 
       let titleHtml ←  descr.mapM goI
-      let titleHtml := if titleHtml.isEmpty then .empty else {{<span class="title">{{titleHtml}}</span>}}
+      let titleHtml := if titleHtml.isEmpty then .empty else html%{<span class="title">{titleHtml}</span>}
 
-      pure {{
-        <div class="namedocs" {{attrs}}>
-          <span class="label">{{label}}</span>
-          {{titleHtml}}
+      pure html%{
+        <div class="namedocs" {...attrs}>
+          <span class="label">{label}</span>
+          {titleHtml}
           <div class="text">
-            {{← content.mapM goB}}
+            {← content.mapM goB}
           </div>
         </div>
-      }}
+      }
   extraCss := [
 r#"
 .namedocs .title {
@@ -596,7 +596,7 @@ window.addEventListener("load", () => {
 });
 "#
 
-open Verso.Output Html HtmlT in
+open Verso.Output Verso.Doc.Html HtmlT in
 private def nonTermHtmlOf (kind : Name) (doc? : Option String) (rendered : Html) : HtmlT Manual (ReaderT Multi.AllRemotes (ReaderT ExtensionImpls (BuildLogT IO))) Html := do
   let xref ← match (← state).resolveDomainObject syntaxKindDomain kind.toString with
     | .error _ =>
@@ -606,21 +606,21 @@ private def nonTermHtmlOf (kind : Name) (doc? : Option String) (rendered : Html)
   let addXref := fun html =>
     match xref with
     | none => html
-    | some tgt => {{<a href={{tgt}}>{{html}}</a>}}
+    | some tgt => html%{<a href={tgt}>{html}</a>}
 
   return addXref <|
     match doc? with
-    | some doc => {{
-        <span class="nonterminal documented" {{#[("data-kind", kind.toString)]}}>
-          <code class="hover-info"><code class="docstring">{{doc}}</code></code>
-          {{rendered}}
+    | some doc => html%{
+        <span class="nonterminal documented" data-kind={kind.toString}>
+          <code class="hover-info"><code class="docstring">{doc}</code></code>
+          {rendered}
         </span>
-      }}
-    | none => {{
-        <span class="nonterminal" {{#[("data-kind", kind.toString)]}}>
-          {{rendered}}
+      }
+    | none => html%{
+        <span class="nonterminal" data-kind={kind.toString}>
+          {rendered}
         </span>
-      }}
+      }
 
 
 structure GrammarHtmlContext where
@@ -642,7 +642,7 @@ def noLook (ctx : GrammarHtmlContext) : GrammarHtmlContext :=
 
 end GrammarHtmlContext
 
-open Verso.Output Html in
+open Verso.Output Verso.Doc.Html in
 abbrev GrammarHtmlM := ReaderT GrammarHtmlContext (HtmlT Manual (ReaderT Multi.AllRemotes (ReaderT ExtensionImpls (BuildLogT IO))))
 
 private def lookingAt (k : Name) : GrammarHtmlM α → GrammarHtmlM α := withReader (·.look k)
@@ -666,7 +666,7 @@ private def productionDomainMapper : DomainMapper where
     ref: value,
   }))"
 
-open Verso.Output Html in
+open Verso.Output Verso.Doc.Html in
 @[block_extension grammar]
 partial def grammar.descr : BlockDescr := withHighlighting {
   init s := s.addQuickJumpMapper productionDomain (productionDomainMapper.setFont { family := .code })
@@ -685,37 +685,36 @@ partial def grammar.descr : BlockDescr := withHighlighting {
     pure none
   toTeX := none
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _goI _goB id info _ => do
       match FromJson.fromJson? (α := Name × TaggedText GrammarTag × Json) info with
       | .ok (kind, bnf, _searchable) =>
         let t ← match (← read).traverseState.externalTags.get? id with
           | some dest => pure dest.htmlId.toString
           | _ => reportError s!"Couldn't get HTML ID for grammar of {kind}" *> pure ""
-        pure {{
-          <pre class="grammar hl lean" data-lean-context="--grammar" id={{t}}>
-            {{← bnfHtml bnf |>.run (GrammarHtmlContext.default.skip kind) }}
+        pure html%{
+          <pre class="grammar hl lean" data-lean-context="--grammar" id={t}>
+            {← bnfHtml bnf |>.run (GrammarHtmlContext.default.skip kind)}
           </pre>
-        }}
+        }
       | .error e =>
         reportError s!"Couldn't deserialize BNF: {e}"
         pure .empty
   extraCss := [grammarCss, "#toc .split-toc > ol .syntax .keyword { font-family: var(--verso-code-font-family); font-weight: 600; }"]
   extraJs := [grammarJs]
-  localContentItem _ json _ := open Verso.Output.Html in do
+  localContentItem _ json _ := do
     if let .arr #[_, .arr #[_, .arr toks]] := json then
       let toks ← toks.mapM fun v => do
           let Json.str str ← v.getObjVal? "string"
             | throw "Not a string"
           let .str k ← v.getObjVal? "kind"
             | throw "Not a string"
-          pure (str, {{<span class={{k}}>{{str}}</span>}})
+          pure (str, html%{<span class={k}>{str}</span>})
       let (strs, toks) := toks.unzip
       if strs == #["…"] || strs == #["..."] then
         -- Don't add the item if it'd be useless for navigating the page
         pure #[]
       else
-        pure #[(String.join strs.toList, {{<span class="syntax">{{toks}}</span>}})]
+        pure #[(String.join strs.toList, html%{<span class="syntax">{toks}</span>})]
     else throw s!"Expected a Json array shaped like [_, [_, [tok, ...]]], got {json}"
 }
 where
@@ -729,44 +728,44 @@ where
   tagHtml (t : GrammarTag) (go : GrammarHtmlM Html) : GrammarHtmlM Html :=
     match t with
     | .lhs | .rhs => go
-    | .bnf => ({{<span class="bnf">{{·}}</span>}}) <$> notLooking go
-    | .comment => ({{<span class="comment">{{·}}</span>}}) <$> notLooking go
-    | .error => ({{<span class="err">{{·}}</span>}}) <$> notLooking go
-    | .literalIdent => ({{<span class="literal-ident">{{·}}</span>}}) <$> notLooking go
+    | .bnf => (html%{<span class="bnf">{·}</span>}) <$> notLooking go
+    | .comment => (html%{<span class="comment">{·}</span>}) <$> notLooking go
+    | .error => (html%{<span class="err">{·}</span>}) <$> notLooking go
+    | .literalIdent => (html%{<span class="literal-ident">{·}</span>}) <$> notLooking go
     | .keyword => do
       let inner ← go
       if let some k := (← read).lookingAt then
         unless k == nullKind do
           if let some tgt := ((← HtmlT.state (genre := Manual) (m := ReaderT Multi.AllRemotes (ReaderT ExtensionImpls (BuildLogT IO)))).localTargets.keyword k none)[0]? then
-            return {{<a href={{tgt.href}}><span class="keyword">{{inner}}</span></a>}}
-      return {{<span class="keyword">{{inner}}</span>}}
+            return html%{<a href={tgt.href}><span class="keyword">{inner}</span></a>}
+      return html%{<span class="keyword">{inner}</span>}
     | .nonterminal k doc? => do
       let inner ← notLooking go
       nonTermHtmlOf k doc? inner
     | .fromNonterminal k none => do
       let inner ← lookingAt k go
-      return {{<span class="from-nonterminal" {{#[("data-kind", k.toString)]}}>{{inner}}</span>}}
+      return html%{<span class="from-nonterminal" data-kind={k.toString}>{inner}</span>}
     | .fromNonterminal k (some doc) => do
       let inner ← lookingAt k go
-      return {{
-        <span class="from-nonterminal documented" {{#[("data-kind", k.toString)]}}>
-          <code class="hover-info"><code class="docstring">{{doc}}</code></code>
-          {{inner}}
+      return html%{
+        <span class="from-nonterminal documented" data-kind={k.toString}>
+          <code class="hover-info"><code class="docstring">{doc}</code></code>
+          {inner}
         </span>
-      }}
+      }
     | .localName x n cat doc? => do
       let doc :=
         match doc? with
         | none => .empty
-        | some d => {{<span class="sep"/><code class="docstring">{{d}}</code>}}
+        | some d => html%{<span class="sep"/><code class="docstring">{d}</code>}
       let inner ← notLooking go
       -- The "token" class below triggers binding highlighting
-      return {{
-        <span class="local-name token documented" {{#[("data-kind", cat.toString)]}} data-binding=s!"grammar-var-{n}-{x}">
-          <code class="hover-info"><code>{{x.toString}} " : " {{cat.toString}}</code>{{doc}}</code>
-          {{inner}}
+      return html%{
+        <span class="local-name token documented" data-kind={cat.toString} data-binding={s!"grammar-var-{n}-{x}"}>
+          <code class="hover-info"><code>{x.toString} : {cat.toString}</code>{doc}</code>
+          {inner}
         </span>
-      }}
+      }
 
 
 def Inline.syntaxKind : Inline where
@@ -798,16 +797,15 @@ def syntaxKind.inlinedescr : InlineDescr := withHighlighting {
   extraCss := [grammarCss]
   extraJs := [grammarJs]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun goI _ data inls => do
       match FromJson.fromJson? (α := Name × String × Option String) data with
       | .error e =>
         reportError s!"Couldn't deserialize syntax kind name: {e}"
-        return {{<code>{{← inls.mapM goI}}</code>}}
+        return html%{<code>{← inls.mapM goI}</code>}
       | .ok (k, showAs, doc?) =>
-        return {{
+        return html%{
           <code class="grammar">
-            {{← nonTermHtmlOf k doc? showAs}}
+            {← nonTermHtmlOf k doc? showAs}
           </code>
-        }}
+        }
 }
diff --git a/Manual/Meta/Syntax/Grammar.lean b/Manual/Meta/Syntax/Grammar.lean
index 1dd36b856..d860b5787 100644
--- a/Manual/Meta/Syntax/Grammar.lean
+++ b/Manual/Meta/Syntax/Grammar.lean
@@ -609,7 +609,7 @@ where
       return bar ++ .nest 2 (← production which stx |>.run' {})
 
 def testGetBnf (config : FreeSyntaxConfig) (isFirst : Bool) (stxs : List Syntax) : TermElabM String := do
-  let (tagged, _) ← getBnf config isFirst stxs |>.run ⟨default, default, default, default⟩ {} {partContext := ⟨⟨default, default, default, default, default, default⟩, default⟩}
+  let (tagged, _) ← getBnf config isFirst stxs |>.run default {} {partContext := ⟨⟨default, default, default, default, default, default⟩, default⟩}
   pure tagged.stripTags
 
 
diff --git a/Manual/Meta/Tactics.lean b/Manual/Meta/Tactics.lean
index 37be40c40..3d1713791 100644
--- a/Manual/Meta/Tactics.lean
+++ b/Manual/Meta/Tactics.lean
@@ -555,7 +555,6 @@ def proofState.descr : BlockDescr := withHighlighting {
   extraCss := [proofStateStyle]
 
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ id data _ => do
       match FromJson.fromJson? (α := Option Tag × Array (Highlighted.Goal Highlighted)) data with
       | .error err =>
@@ -565,16 +564,16 @@ def proofState.descr : BlockDescr := withHighlighting {
         let xref ← HtmlT.state
         let idAttr := xref.htmlId id
 
-        pure {{
+        pure html%{
           <div class="hl lean tactic-view">
-            <div class="tactic-state" {{idAttr}}>
-              {{← if goals.isEmpty then
-                  pure {{"All goals completed! 🐙"}}
+            <div class="tactic-state" {...idAttr}>
+              {← if goals.isEmpty then
+                  pure html%{All goals completed! 🐙}
                 else
-                  .seq <$> goals.mapIdxM fun i x => withCollapsedSubgoals (g := Verso.Genre.Manual) .never <| x.toHtml (·.toHtml) i}}
+                  .seq <$> goals.mapIdxM fun i x => withCollapsedSubgoals (g := Verso.Genre.Manual) .never <| x.toHtml (·.toHtml) i}
             </div>
           </div>
-        }}
+        }
 }
 
 structure StateConfig where
diff --git a/Manual/NotationsMacros/DoElab.lean b/Manual/NotationsMacros/DoElab.lean
index ac7e9f131..d99f13034 100644
--- a/Manual/NotationsMacros/DoElab.lean
+++ b/Manual/NotationsMacros/DoElab.lean
@@ -623,10 +623,15 @@ In some advanced cases, one of the functions in {namespace}`Lean.Elab.Do.InferCo
 
 ## Mutable Variables
 
+:::leanSection
+```lean -show
+open Lean.Elab.Do (MutVar)
+```
 One important part of the context is the set of mutable variables available for the {keywordOf Lean.Parser.Term.do}`do`-element being elaborated.
 This is available in two fields: {name Lean.Elab.Do.Context.mutVars}`mutVars` provides the identifiers that initially bound the variables, while {name Lean.Elab.Do.Context.mutVarDefs}`mutVarDefs` maps their names to the local variables that represent them.
 Due to {tech}[hygiene], the identifiers in {name Lean.Elab.Do.Context.mutVars}`mutVars` contain {tech}[macro scopes], but these are automatically removed by the {inst}`ToMessageData MutVar` instance.
 If the names are displayed in some other way, then the macro scopes should be removed using {name}`Name.simpMacroScopes` prior to constructing a user-facing error message.
+:::
 
 {docstring Lean.Elab.Do.MutVar}
 
diff --git a/Tutorial/MVCGen.lean b/Tutorial/MVCGen.lean
index de732fe9a..25b73f3c7 100644
--- a/Tutorial/MVCGen.lean
+++ b/Tutorial/MVCGen.lean
@@ -26,7 +26,6 @@ set_option linter.unusedVariables false
 set_option linter.typography.quotes true
 set_option linter.typography.dashes true
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 #doc (Tutorial) "Verifying Imperative Programs Using `mvcgen`" =>
@@ -51,7 +50,6 @@ import Std.Tactic.Do
 ```
 :::codeOnly
 ```lean
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 ```
 :::
diff --git a/Tutorial/Meta/Theme.lean b/Tutorial/Meta/Theme.lean
index fc74bc381..63e764536 100644
--- a/Tutorial/Meta/Theme.lean
+++ b/Tutorial/Meta/Theme.lean
@@ -354,7 +354,7 @@ def layoutConfig : LayoutConfig :=
     hasSpecialStyling := fun path => if isFro path then some "fro" else if path.isEmpty then "tutorials" else none,
     renderPostList := fun path html =>
       if isUseCases path then
-        {{ <div class="use-cases-grid"> {{ html }} </div> }}
+        html%{<div class="use-cases-grid">{html}</div>}
       else
         html
   }
@@ -364,12 +364,12 @@ def theme : Theme :=
     { siteName := "Lean Lang", rootTitle := "Lean enables correct, maintainable, and formally verified code", socialMeta, headConfig, variables := colorTheme }
     layoutConfig
     buildFroNavBarConfig
-    {{
+    html%{
       <script async src="https://plausible.io/js/pa-RTua_4FfKHhfAvAc3liZd.js"></script>
       <script>
-        "window.plausible=window.plausible||function(){(plausible.q=plausible.q||[]).push(arguments)},plausible.init=plausible.init||function(i){plausible.o=i||{}};
-        plausible.init()"
+        {"window.plausible=window.plausible||function(){(plausible.q=plausible.q||[]).push(arguments)},plausible.init=plausible.init||function(i){plausible.o=i||{}};
+        plausible.init()"}
       </script>
-    }}
+    }
     (beforeNavBar := .empty)
     (pure footer)
diff --git a/TutorialMain.lean b/TutorialMain.lean
index 0f98cec83..d908f9740 100644
--- a/TutorialMain.lean
+++ b/TutorialMain.lean
@@ -14,10 +14,9 @@ open Verso.Genre.Manual
 open Verso.Genre.Tutorial
 open Verso.Genre.Blog (Page)
 
-open Verso.Output.Html in
-def plausible := {{
+def plausible := html%{
     <script defer="defer" data-domain="lean-lang.org" src="https://plausible.io/js/script.outbound-links.js"></script>
-  }}
+  }
 
 section
 open Verso.Doc.Elab
diff --git a/lake-manifest.json b/lake-manifest.json
index 7d2cdbb8c..111ee8a4d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "71a2035b44e7f54a797ce799fd1b03cdd3a44684",
+   "rev": "7965b16761e85e6fbd75979b51b86f903f5c8426",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f58dcf79abdf0343048798df5c28d50dcc8e8466",
+   "rev": "238598f68274ba03b8a8c0d1be77f48208835fb0",
    "name": "versowebcomponents",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",