diff --git a/doc-gen4/DocGen4/Output.lean b/doc-gen4/DocGen4/Output.lean
index 874aed388..04e6ccc0b 100644
--- a/doc-gen4/DocGen4/Output.lean
+++ b/doc-gen4/DocGen4/Output.lean
@@ -49,13 +49,13 @@ def htmlOutputSetup (config : SiteBaseContext) (tacticInfo : Array (Process.Tact
   FS.createDirAll <| declarationsBasePath config.buildDir
 
   -- All the doc-gen static stuff
-  let indexHtml := ReaderT.run index config |>.toString
-  let notFoundHtml := ReaderT.run notFound config |>.toString
-  let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
-  let navbarHtml := ReaderT.run navbar config |>.toString
-  let searchHtml := ReaderT.run search config |>.toString
-  let referencesHtml := ReaderT.run (references (← collectBackrefs config.buildDir)) config |>.toString
-  let tacticsHtml := ReaderT.run (tactics tacticInfo) config |>.toString
+  let indexHtml := ReaderT.run index config |>.render
+  let notFoundHtml := ReaderT.run notFound config |>.render
+  let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.render
+  let navbarHtml := ReaderT.run navbar config |>.render
+  let searchHtml := ReaderT.run search config |>.render
+  let referencesHtml := ReaderT.run (references (← collectBackrefs config.buildDir)) config |>.render
+  let tacticsHtml := ReaderT.run (tactics tacticInfo) config |>.render
   let docGenStatic := #[
     ("style.css", styleCss),
     ("favicon.svg", faviconSvg),
@@ -80,7 +80,7 @@ def htmlOutputSetup (config : SiteBaseContext) (tacticInfo : Array (Process.Tact
   for (fileName, content) in docGenStatic do
     writeFileAtomic (basePath config.buildDir / fileName) content
 
-  let findHtml := ReaderT.run find { config with depthToRoot := 1 } |>.toString
+  let findHtml := ReaderT.run find { config with depthToRoot := 1 } |>.render
   let findStatic := #[
     ("index.html", findHtml),
     ("find.js", findJs)
@@ -147,7 +147,7 @@ def htmlOutputResultsParallel (baseConfig : SiteBaseContext) (dbPath : System.Fi
         let filePath := baseConfig.buildDir / relFilePath
         if let .some d := filePath.parent then
           FS.createDirAll d
-        writeFileAtomic filePath moduleHtml.toString
+        writeFileAtomic filePath moduleHtml.render
 
         -- Write backrefs JSON
         writeFileAtomic (declarationsBasePath baseConfig.buildDir / s!"backrefs-{module.name}.json")
@@ -335,7 +335,7 @@ def updateNavbarFromDisk (buildDir : System.FilePath) : IO Unit := do
     refs := refs
   }
   -- Regenerate navbar
-  let navbarHtml := ReaderT.run navbar baseConfig |>.toString
+  let navbarHtml := ReaderT.run navbar baseConfig |>.render
   writeFileAtomic (docDir / "navbar.html") navbarHtml
 
 end DocGen4
diff --git a/doc-gen4/DocGen4/Output/Arg.lean b/doc-gen4/DocGen4/Output/Arg.lean
index 536f7268c..1a4085114 100644
--- a/doc-gen4/DocGen4/Output/Arg.lean
+++ b/doc-gen4/DocGen4/Output/Arg.lean
@@ -12,7 +12,7 @@ type of binder it has.
 def argToHtml (arg : Process.Arg) : HtmlM Html := do
   let node ← renderedCodeToHtml arg.binder
   let inner := <span class="fn">[node]</span>
-  let html := Html.element "span" false #[("class", "decl_args")] #[inner]
+  let html := .element "span" #[("class", "decl_args")] #[inner]
   if arg.implicit then
     return <span class="impl_arg">{html}</span>
   else
diff --git a/doc-gen4/DocGen4/Output/DocString.lean b/doc-gen4/DocGen4/Output/DocString.lean
index fbb491c68..35a23d3a8 100644
--- a/doc-gen4/DocGen4/Output/DocString.lean
+++ b/doc-gen4/DocGen4/Output/DocString.lean
@@ -179,7 +179,7 @@ def autoLinkInline (ss : Array String) : HtmlM (Array Html) := do
     for part in parts do
       match ← nameToLink? part with
       | some link =>
-        result := result.push <| Html.element "a" true #[("href", link)] #[Html.text part]
+        result := result.push <| .element "a" #[("href", link)] #[Html.text part]
       | none =>
         let sHead := part.dropEndWhile (· != '.') |>.copy
         let sTail := part.takeEndWhile (· != '.') |>.copy
@@ -187,7 +187,7 @@ def autoLinkInline (ss : Array String) : HtmlM (Array Html) := do
         | some link =>
           if !sHead.isEmpty then
             result := result.push <| Html.text sHead
-          result := result.push <| Html.element "a" true #[("href", link)] #[Html.text sTail]
+          result := result.push <| .element "a" #[("href", link)] #[Html.text sTail]
         | none =>
           result := result.push <| Html.text part
   return result
@@ -211,16 +211,16 @@ partial def renderText (t : MD4Lean.Text) (funName : String) (inLink : Bool := f
   | .entity s => return #[Html.raw s]
   | .em ts =>
     let inner ← renderTexts ts funName inLink
-    return #[Html.element "em" true #[] inner]
+    return #[.element "em" #[] inner]
   | .strong ts =>
     let inner ← renderTexts ts funName inLink
-    return #[Html.element "strong" true #[] inner]
+    return #[.element "strong" #[] inner]
   | .u ts =>
     let inner ← renderTexts ts funName inLink
-    return #[Html.element "u" true #[] inner]
+    return #[.element "u" #[] inner]
   | .del ts =>
     let inner ← renderTexts ts funName inLink
-    return #[Html.element "del" true #[] inner]
+    return #[.element "del" #[] inner]
   | .a href title _isAuto children =>
     let hrefStr := attrTextToString href
     let titleStr := attrTextToString title
@@ -240,13 +240,13 @@ partial def renderText (t : MD4Lean.Text) (funName : String) (inLink : Bool := f
       let mut attrs : Array (String × String) := #[("href", extHref)]
       attrs := attrs.push ("title", bibitem.plaintext)
       attrs := attrs.push ("id", s!"_backref_{newBackref.index}")
-      return #[Html.element "a" true attrs newChildren]
+      return #[.element "a" attrs newChildren]
     | .none =>
       let childrenHtml ← renderTexts children funName (inLink := true)
       let mut attrs : Array (String × String) := #[("href", extHref)]
       if !titleStr.isEmpty then
         attrs := attrs.push ("title", titleStr)
-      return #[Html.element "a" true attrs childrenHtml]
+      return #[.element "a" attrs childrenHtml]
   | .img src title alt =>
     let srcStr := Html.escape (attrTextToString src)
     let titleStr := Html.escape (attrTextToString title)
@@ -262,7 +262,7 @@ partial def renderText (t : MD4Lean.Text) (funName : String) (inLink : Bool := f
         pure #[Html.text (String.join ss.toList)]
       else
         autoLinkInline ss
-    return #[Html.element "code" true #[] inner]
+    return #[.element "code" #[] inner]
   -- Math is rendered with dollar signs because MathJax will later render them
   | .latexMath ss =>
     let content := String.join ss.toList
@@ -274,7 +274,7 @@ partial def renderText (t : MD4Lean.Text) (funName : String) (inLink : Bool := f
   | .wikiLink target children =>
     let inner ← renderTexts children funName inLink
     let targetStr := attrTextToString target
-    return #[Html.element "x-wikilink" true #[("data-target", targetStr)] inner]
+    return #[.element "x-wikilink" #[("data-target", targetStr)] inner]
 
 /-- Render an array of `MD4Lean.Text` inline elements to HTML. -/
 partial def renderTexts (texts : Array MD4Lean.Text) (funName : String) (inLink : Bool := false) : HtmlM (Array Html) := do
@@ -291,13 +291,13 @@ partial def renderBlock (block : MD4Lean.Block) (funName : String) (tight : Bool
     if tight then
       return inner
     else
-      return #[Html.element "p" true #[] inner]
+      return #[.element "p" #[] inner]
   | .ul isTight _mark items =>
     let mut lis : Array Html := #[]
     for item in items do
       let liHtml ← renderLi item funName isTight
       lis := lis ++ liHtml
-    return #[Html.element "ul" true #[] lis]
+    return #[.element "ul" #[] lis]
   | .ol isTight start _mark items =>
     let mut lis : Array Html := #[]
     for item in items do
@@ -305,15 +305,15 @@ partial def renderBlock (block : MD4Lean.Block) (funName : String) (tight : Bool
       lis := lis ++ liHtml
     let attrs : Array (String × String) :=
       if start != 1 then #[("start", toString start)] else #[]
-    return #[Html.element "ol" true attrs lis]
+    return #[.element "ol" attrs lis]
   | .hr => return #[Html.raw "<hr>\n"]
   | .header level texts =>
     let id := mdGetHeadingId texts
     let inner ← renderTexts texts funName
-    let anchor := Html.element "a" true #[("class", "hover-link"), ("href", s!"#{id}")] #[Html.text "#"]
+    let anchor := .element "a" #[("class", "hover-link"), ("href", s!"#{id}")] #[Html.text "#"]
     let children := inner.push (Html.text " ") |>.push anchor
     let tag := s!"h{level}"
-    return #[Html.element tag true #[("id", id), ("class", "markdown-heading")] children]
+    return #[.element tag #[("id", id), ("class", "markdown-heading")] children]
   | .code _info lang _fenceChar content =>
     let langStr := attrTextToString lang
     let codeAttrs : Array (String × String) :=
@@ -323,31 +323,31 @@ partial def renderBlock (block : MD4Lean.Block) (funName : String) (tight : Bool
         autoLinkInline content
       else
         pure #[Html.text (String.join content.toList)]
-    let codeElem := Html.element "code" true codeAttrs inner
-    return #[Html.element "pre" true #[] #[codeElem]]
+    let codeElem : Html := .element "code" codeAttrs inner
+    return #[.element "pre" #[] #[codeElem]]
   | .html content =>
     return #[Html.raw (String.join content.toList)]
   | .blockquote blocks =>
     let mut inner : Array Html := #[]
     for b in blocks do
       inner := inner ++ (← renderBlock b funName)
-    return #[Html.element "blockquote" true #[] inner]
+    return #[.element "blockquote" #[] inner]
   | .table head body =>
     let mut headCells : Array Html := #[]
     for cell in head do
       let cellHtml ← renderTexts cell funName
-      headCells := headCells.push (Html.element "th" true #[] cellHtml)
-    let headRow := Html.element "tr" true #[] headCells
-    let thead := Html.element "thead" true #[] #[headRow]
+      headCells := headCells.push (.element "th" #[] cellHtml)
+    let headRow : Html := .element "tr" #[] headCells
+    let thead := .element "thead" #[] #[headRow]
     let mut bodyRows : Array Html := #[]
     for row in body do
       let mut rowCells : Array Html := #[]
       for cell in row do
         let cellHtml ← renderTexts cell funName
-        rowCells := rowCells.push (Html.element "td" true #[] cellHtml)
-      bodyRows := bodyRows.push (Html.element "tr" true #[] rowCells)
-    let tbody := Html.element "tbody" true #[] bodyRows
-    return #[Html.element "table" true #[] #[thead, tbody]]
+        rowCells := rowCells.push (.element "td" #[] cellHtml)
+      bodyRows := bodyRows.push (.element "tr" #[] rowCells)
+    let tbody : Html := .element "tbody" #[] bodyRows
+    return #[.element "table" #[] #[thead, tbody]]
 
 /-- Render a list item to HTML. -/
 partial def renderLi (li : MD4Lean.Li MD4Lean.Block) (funName : String) (tight : Bool) : HtmlM (Array Html) := do
@@ -360,7 +360,7 @@ partial def renderLi (li : MD4Lean.Li MD4Lean.Block) (funName : String) (tight :
       inner := inner.push (Html.raw "<input type=\"checkbox\" disabled=\"\">")
   for b in li.contents do
     inner := inner ++ (← renderBlock b funName tight)
-  return #[Html.element "li" true #[] inner]
+  return #[.element "li" #[] inner]
 
 end
 
diff --git a/doc-gen4/DocGen4/Output/Module.lean b/doc-gen4/DocGen4/Output/Module.lean
index 02ebc6cde..580089b3b 100644
--- a/doc-gen4/DocGen4/Output/Module.lean
+++ b/doc-gen4/DocGen4/Output/Module.lean
@@ -43,7 +43,7 @@ and name.
 -/
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
-  nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription]
+  nodes := nodes.push <| .element "span" #[("class", "decl_kind")] #[Html.text doc.getKindDescription]
   -- TODO: Can we inline if-then-else and avoid repeating <span> here?
   if doc.getSorried then
     nodes := nodes.push <span class="decl_name" title="declaration uses 'sorry'"> {← declNameToHtmlBreakWithinLink doc.getName} </span>
@@ -57,7 +57,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   | DocInfo.classInfo i => nodes := nodes.append (← structureInfoHeader i)
   | _ => nodes := nodes
 
-  nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"]
+  nodes := nodes.push <| .element "span" #[("class", "decl_args")] #[Html.text " :"]
   nodes := nodes.push <div class="decl_type">[← renderedCodeToHtml doc.getType]</div>
   return <div class="decl_header"> [nodes] </div>
 
@@ -89,7 +89,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   let attrsHtml :=
     if attrs.size > 0 then
       let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
-      #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
+      #[.element "div" #[("class", "attributes")] #[Html.text attrStr]]
     else
       #[]
   -- custom decoration (e.g., verification badges from external tools)
@@ -184,7 +184,7 @@ def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBas
   let memberNames := filterDocInfo relevantMembers.iter |>.map DocInfo.getName |>.toArray
   templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[
     ← internalNav memberNames module.name,
-    Html.element "main" false #[] memberDocs
+    .element "main" #[] memberDocs
   ]
 
 end Output
diff --git a/doc-gen4/DocGen4/Output/Tactics.lean b/doc-gen4/DocGen4/Output/Tactics.lean
index 54ad7c910..c4d5cba74 100644
--- a/doc-gen4/DocGen4/Output/Tactics.lean
+++ b/doc-gen4/DocGen4/Output/Tactics.lean
@@ -61,7 +61,7 @@ def tactics (tacticInfo : Array (TacticInfo Html)) : BaseHtmlM Html := do
       <p><a href="#top">return to top</a></p>
       [tacticInfo.map (· |>.navLink)]
     </nav>,
-    Html.element "main" false #[] (
+    .element "main" #[] (
       #[<p>The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword <code>by</code>.</p>] ++
       sectionsHtml)
   ]
diff --git a/doc-gen4/DocGen4/Output/ToHtmlFormat.lean b/doc-gen4/DocGen4/Output/ToHtmlFormat.lean
index b6381931d..abb65e387 100644
--- a/doc-gen4/DocGen4/Output/ToHtmlFormat.lean
+++ b/doc-gen4/DocGen4/Output/ToHtmlFormat.lean
@@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki, Sebastian Ullrich, Henrik Böving
 -/
 import Lean.Data.Json
 import Lean.Parser
+import Lean.Data.Html
 
 /-! This module defines:
 - a representation of HTML trees
@@ -16,19 +17,6 @@ namespace DocGen4
 
 open Lean
 
-inductive Html where
-  -- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson
-  -- element (tag : String) (flatten : Bool) (attrs : Array HtmlAttribute) (children : Array Html)
-  | element : String → Bool → Array (String × String) → Array Html → Html
-  /-- A text node, which will be escaped in the output -/
-  | text : String → Html
-  /-- An arbitrary string containing HTML -/
-  | raw : String → Html
-  deriving Repr, BEq, Inhabited, FromJson, ToJson
-
-instance : Coe String Html :=
-  ⟨Html.text⟩
-
 namespace Html
 
 
@@ -57,25 +45,11 @@ where
 def attributesToString (attrs : Array (String × String)) :String :=
   attrs.foldl (fun acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ escape v ++ "\"") ""
 
--- TODO: Termination proof
-partial def toStringAux : Html → String
-| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{escape s}</{tag}>\n"
-| element tag false attrs #[raw s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
-| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
-| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"
-| element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
-| text s => escape s
-| raw s => s
-
-def toString (html : Html) : String :=
-  html.toStringAux.trimAsciiEnd.copy
-
 partial def textLength : Html → Nat
-| raw s => s.length  -- measures lengths of escape sequences too!
-| text s => s.length
-| element _ _ _ children =>
-  let lengths := children.map textLength
-  lengths.foldl Nat.add 0
+  | .raw s => s.length  -- measures lengths of escape sequences too!
+  | .text s => s.length
+  | .element _ _ c => textLength c
+  | .seq s => s.foldl (· + textLength ·) 0
 
 end Html
 
@@ -149,10 +123,10 @@ macro_rules
   | `(<$n $attrs* />) => do
     let kind := quote (toString n.getId)
     let attrs ← translateAttrs attrs
-    `(Html.element $kind true $attrs #[])
+    `(Html.element $kind $attrs (.seq #[]))
   | `(<$n $attrs* >$children*</$m>) => do
     let (tag, children) ← htmlHelper n children m
-    `(Html.element $(quote tag) true $(← translateAttrs attrs) $children)
+    `(Html.element $(quote tag) $(← translateAttrs attrs) (.seq $children))
 
 end Jsx
 
@@ -161,4 +135,30 @@ as the resulting HTML in editors which support it. -/
 class ToHtmlFormat (α : Type u) where
   formatHtml : α → Html
 
+/-! ## Deprecation aliases -/
+-- TODO: Remove aliases later.
+
+-- Constants with same name and type are re-exported in the old namespace.
+export Lean (Html Html.text Html.raw)
+
+-- Constants whose name or type changed become deprecated protected abbrevs in the old namespace.
+set_option linter.unusedVariables false in
+@[deprecated Lean.Html.element +typeChanged (since := "2026-09-02")]
+protected abbrev Html.element (tag : String) (flatten : Bool) (attrs : Array (String × String)) (children : Array Html) :=
+  Lean.Html.element tag attrs (.ofCollection children)
+
+@[deprecated Lean.Html.render (since := "2026-09-02")]
+protected abbrev Html.toString (html : Html) : String :=
+  Lean.Html.render html
+
 end DocGen4
+
+-- Constants whose name or type changed, and which are commonly used with dot notation,
+-- also get a deprecated alias in the new namespace.
+namespace Lean.Html
+
+@[deprecated Lean.Html.render (since := "2026-09-02")]
+protected abbrev toString (html : Html) : String :=
+  Lean.Html.render html
+
+end Lean.Html
diff --git a/doc-gen4/DocGen4/Output/ToJson.lean b/doc-gen4/DocGen4/Output/ToJson.lean
index c95869d81..94e0fe320 100644
--- a/doc-gen4/DocGen4/Output/ToJson.lean
+++ b/doc-gen4/DocGen4/Output/ToJson.lean
@@ -124,7 +124,7 @@ def DocInfo.toJson (sourceLinker : Option DeclarationRange → String) (info : P
   let docLink ← declNameToLink info.getName
   let sourceLink := sourceLinker info.getDeclarationRange
   let line := info.getDeclarationRange.pos.line
-  let header := (← docInfoHeader info).toString
+  let header := (← docInfoHeader info).render
   let info := { name, kind, doc, docLink, sourceLink, line }
   return { info, header }
 
diff --git a/lean-toolchain b/lean-toolchain
index 1aa2a00d6..2a8f9f07d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-10-01
+leanprover/lean4-pr-releases:pr-release-14935-8eaba5e
diff --git a/reference-manual/Main.lean b/reference-manual/Main.lean
index 11db40808..89b32eabc 100644
--- a/reference-manual/Main.lean
+++ b/reference-manual/Main.lean
@@ -14,7 +14,7 @@ open Verso.Genre.Manual.InlineLean
 open Verso.Output.Html in
 def plausible := {{
     <script async src="https://plausible.io/js/pa-RTua_4FfKHhfAvAc3liZd.js"></script>
-    <script>{{Verso.Output.Html.text false 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>
diff --git a/reference-manual/Manual/Meta/ErrorExplanation.lean b/reference-manual/Manual/Meta/ErrorExplanation.lean
index 1e9b16b31..42a53ed95 100644
--- a/reference-manual/Manual/Meta/ErrorExplanation.lean
+++ b/reference-manual/Manual/Meta/ErrorExplanation.lean
@@ -30,6 +30,6 @@ def getBreakableSuffix (name : Name) : Option String := do
   htmlText breakableHtml
 where
   htmlText : Verso.Output.Html → String
-    | .text _ txt => txt
+    | .text txt | .raw txt => txt
     | .seq elts => elts.foldl (· ++ htmlText ·) ""
-    | .tag _nm _attrs children => htmlText children
+    | .element _nm _attrs children => htmlText children
diff --git a/reference-manual/Manual/Meta/ErrorExplanation/Header.lean b/reference-manual/Manual/Meta/ErrorExplanation/Header.lean
index 30fe4b699..355af37b1 100644
--- a/reference-manual/Manual/Meta/ErrorExplanation/Header.lean
+++ b/reference-manual/Manual/Meta/ErrorExplanation/Header.lean
@@ -82,8 +82,8 @@ block_extension Block.errorExplanationHeader (metadata : ErrorExplanationExtende
       ++ (metadata.removedVersion?.map fun v => #[("Removed", v)]).getD #[]
     let entries := entries.map fun (label, data) =>
       {{ <span class="error-explanation-metadatum">
-           <strong>{{Html.text true label}}": "</strong>
-           {{Html.text true data}}
+           <strong>{{Html.text label}}": "</strong>
+           {{Html.text data}}
           </span> }}
     return {{
       <div class="error-explanation-metadata">
diff --git a/reference-manual/Manual/Meta/LakeToml/Table.lean b/reference-manual/Manual/Meta/LakeToml/Table.lean
index 42a80f88f..b94af7dcb 100644
--- a/reference-manual/Manual/Meta/LakeToml/Table.lean
+++ b/reference-manual/Manual/Meta/LakeToml/Table.lean
@@ -71,7 +71,7 @@ def FieldType.toHtml (plural : Bool := false) : FieldType → Html
   | .option t => t.toHtml ++ " (optional)"
   | .oneOf xs =>
     let opts := xs
-      |>.map ({{<code>{{show Html from .text true s!"\"{·}\""}}</code>}})
+      |>.map ({{<code>{{show Html from .text s!"\"{·}\""}}</code>}})
       |>.intersperse {{", "}}
     {{"one of " {{opts}} }}
 
diff --git a/reference-manual/Manual/Meta/Syntax.lean b/reference-manual/Manual/Meta/Syntax.lean
index d40fd8522..32739fb55 100644
--- a/reference-manual/Manual/Meta/Syntax.lean
+++ b/reference-manual/Manual/Meta/Syntax.lean
@@ -721,7 +721,7 @@ partial def grammar.descr : BlockDescr := withHighlighting {
 where
 
   bnfHtml : TaggedText GrammarTag → GrammarHtmlM Html
-  | .text str => pure <| .text true str
+  | .text str => pure <| .text str
   | .tag t txt => tagHtml t (bnfHtml txt)
   | .append txts => .seq <$> txts.mapM bnfHtml
 
diff --git a/reference-manual/Tutorial/Meta/Theme.lean b/reference-manual/Tutorial/Meta/Theme.lean
index 23aa16d58..9e4b643db 100644
--- a/reference-manual/Tutorial/Meta/Theme.lean
+++ b/reference-manual/Tutorial/Meta/Theme.lean
@@ -95,7 +95,7 @@ def footer : FooterConfig := {
 Helper to create FRO home navigation item
 -/
 def navFroItem (path : Path) : NavBarItem :=
-  { title := .text false "Home"
+  { title := .raw "Home"
   , url := some "/fro"
   , active := path == #["fro"] }
 
@@ -116,15 +116,15 @@ def buildFroNavBarConfig : TemplateM NavBarConfig := do
   let path ← currentPath
 
   let froPathItems (path : Path) : Array NavBarItem := #[
-    { title := .text false "About", url := some "/fro/about", active := path == #["fro", "about"] },
-    { title := .text false "Team", url := some "/fro/team", active := path == #["fro", "team"] },
-    { title := .text false "Roadmap", url := some "/fro/roadmap", active := path == #["fro", "roadmap"] },
-    { title := .text false "Contact", url := some "/fro/contact", active := path == #["fro", "contact"] }
+    { title := .raw "About", url := some "/fro/about", active := path == #["fro", "about"] },
+    { title := .raw "Team", url := some "/fro/team", active := path == #["fro", "team"] },
+    { title := .raw "Roadmap", url := some "/fro/roadmap", active := path == #["fro", "roadmap"] },
+    { title := .raw "Contact", url := some "/fro/contact", active := path == #["fro", "contact"] }
   ]
 
   let externalLinks : Array NavBarItem := #[
-    { title := .text false "Playground", url := some "https://live.lean-lang.org/?from=lean", blank := true },
-    { title := .text false "Reservoir", url := some "https://reservoir.lean-lang.org/", blank := true }
+    { title := .raw "Playground", url := some "https://live.lean-lang.org/?from=lean", blank := true },
+    { title := .raw "Reservoir", url := some "https://reservoir.lean-lang.org/", blank := true }
   ]
 
   let rightItems : Array NavBarItem := #[
diff --git a/verso-slides/Tests/Render.lean b/verso-slides/Tests/Render.lean
index 3e547345a..f4bc53497 100644
--- a/verso-slides/Tests/Render.lean
+++ b/verso-slides/Tests/Render.lean
@@ -20,6 +20,7 @@ open SubVerso.Highlighting Highlighted
 open Verso.Code (HighlightHtmlM)
 open Verso.Code.Hover (State)
 open Verso Output Html
+open Lean (Html)
 open VersoSlides
 
 
@@ -48,7 +49,7 @@ def runHighlightHtml (act : HighlightHtmlM Slides Html) : Html :=
 
 /-- Renders a `SlideCode` to an HTML string. -/
 def renderStr (sc : SlideCode) : String :=
-  (runHighlightHtml (sc.toHtml (g := Slides))).asString
+  (runHighlightHtml (sc.toHtml (g := Slides))).render
 
 
 structure TestState where
@@ -226,5 +227,5 @@ where
       { extraHead := #[{{ <script type="module" src={{blueprintRuntime}}></script> }}] }
       "Deck" (.seq #[])
     testHtmlHas "extraHead renders module script"
-      fullHtml.asString
+      fullHtml.render
       s!"<script type=\"module\" src=\"{blueprintRuntime}\"></script>"
diff --git a/verso-slides/VersoSlides/Directives.lean b/verso-slides/VersoSlides/Directives.lean
index 64a20ebdf..6207cb9ae 100644
--- a/verso-slides/VersoSlides/Directives.lean
+++ b/verso-slides/VersoSlides/Directives.lean
@@ -587,8 +587,8 @@ Usage:
 @[code_block]
 public meta def html : CodeBlockExpanderOf Unit
   | (), str => do
-    -- The `false` parameter treats the text as unescaped raw HTML data.
-    let html := Verso.Output.Html.text false str.getVersoCodeBlock
+    -- `raw` treats the text as unescaped raw HTML data.
+    let html := Lean.Html.raw str.getVersoCodeBlock
     ``(Verso.Doc.Block.other (BlockExt.ofHtml $(quote html)) #[])
 
 /--
@@ -606,5 +606,5 @@ public meta def htmlRole : RoleExpanderOf Unit
     | throwError "Expected a single inline code argument"
   let some { content := htmlStr, .. } := CodeView.of arg
     | throwErrorAt arg "Expected inline code"
-  let html := Verso.Output.Html.text false htmlStr.getVersoCode
+  let html := Lean.Html.raw htmlStr.getVersoCode
   ``(Verso.Doc.Inline.other (VersoSlides.InlineExt.ofHtml $(quote html)) #[])
diff --git a/verso-slides/VersoSlides/Render.lean b/verso-slides/VersoSlides/Render.lean
index 8ca15adaf..9e6b48df6 100644
--- a/verso-slides/VersoSlides/Render.lean
+++ b/verso-slides/VersoSlides/Render.lean
@@ -15,6 +15,7 @@ import Illuminate.Animation.Render
 set_option doc.verso true
 
 open Verso Doc Output Html
+open Lean (Html)
 open Verso.Doc.Html (HtmlT GenreHtml ToHtml mkPartHeader)
 open SubVerso.Highlighting (Highlighted hlFromExport!)
 open Verso.Code (HighlightHtmlM highlightingStyle highlightingJs)
@@ -29,13 +30,13 @@ namespace VersoSlides
 
 /-- Pushes a CSS class onto all top-level HTML tags in a fragment. -/
 partial def addClassToHtml (cls : String) : Html → Html
-  | .tag name attrs children =>
+  | .element name attrs children =>
     let attrs :=
       if let some i := attrs.findFinIdx? (·.1 == "class") then
         attrs.set i ("class", attrs[i].2 ++ " " ++ cls)
       else
         attrs.push ("class", cls)
-    .tag name attrs children
+    .element name attrs children
   | .seq elts => .seq (elts.map (addClassToHtml cls))
   | other => other
 
@@ -53,9 +54,9 @@ private def pushOneAttr (attrs : Array (String × String)) (k v : String) : Arra
 
 /-- Pushes arbitrary attributes onto all top-level HTML tags in a fragment. -/
 partial def pushAttrsOntoHtml (newAttrs : Array (String × String)) : Html → Html
-  | .tag name attrs children =>
+  | .element name attrs children =>
     let attrs := newAttrs.foldl (fun acc (k, v) => pushOneAttr acc k v) attrs
-    .tag name attrs children
+    .element name attrs children
   | .seq elts => .seq (elts.map (pushAttrsOntoHtml newAttrs))
   | other => other
 
@@ -111,7 +112,7 @@ instance [Monad m] [MonadBuildLog (HtmlT Slides m)] : GenreHtml Slides m where
       pure (pushAttrsOntoHtml attrs (.seq inner))
     | .wrap attrs =>
       let inner ← contents.mapM blockHtml
-      pure (.tag "div" attrs (.seq inner))
+      pure (.element "div" attrs (.seq inner))
     | .ofHtml html =>
       pure html
     | .slideCode scExport panel stretch =>
@@ -173,7 +174,7 @@ instance [Monad m] [MonadBuildLog (HtmlT Slides m)] : GenreHtml Slides m where
           let cells := .seq (← row.mapIdxM (mkCell false ·))
           pure {{ <tr>{{cells}}</tr> }}
         pure {{ <tbody>{{.seq trs}}</tbody> }}
-      pure (.tag "table" tableAttrs (.seq #[theadHtml, tbodyHtml]))
+      pure (.element "table" tableAttrs (.seq #[theadHtml, tbodyHtml]))
     | .css _ =>
       pure .empty
     | .diagram svgStr cssWidth background =>
@@ -183,7 +184,7 @@ instance [Monad m] [MonadBuildLog (HtmlT Slides m)] : GenreHtml Slides m where
       let style := s!"width: {cssWidth}{bgStyle}"
       pure {{
         <div class="diagram" style={{style}}>
-          {{Html.text false svgStr}}
+          {{Html.raw svgStr}}
         </div>
       }}
     | .animate containerId animDataJson cssWidth background fragmentIndices autoplay =>
@@ -202,7 +203,7 @@ instance [Monad m] [MonadBuildLog (HtmlT Slides m)] : GenreHtml Slides m where
         let attrs := match idx with
           | some n => baseAttrs.push ("data-fragment-index", toString n)
           | none => baseAttrs
-        .tag "span" attrs .empty
+        .element "span" attrs .empty
       let autoplayAttr := if autoplay then "true" else "false"
       pure {{
         <div class="illuminate-anim" id={{containerId}} style={{style}}
@@ -210,7 +211,7 @@ instance [Monad m] [MonadBuildLog (HtmlT Slides m)] : GenreHtml Slides m where
         </div>
         {{fragSpans}}
         <script type="application/json" data-illuminate-anim={{containerId}}>
-          {{Html.text false animDataJson}}
+          {{Html.raw animDataJson}}
         </script>
       }}
   inline inlineHtml container contents := do
@@ -221,10 +222,10 @@ instance [Monad m] [MonadBuildLog (HtmlT Slides m)] : GenreHtml Slides m where
       let mut attrs : Array (String × String) := #[("class", cls)]
       if let some i := index then
         attrs := attrs.push ("data-fragment-index", toString i)
-      pure (.tag "span" attrs (.seq inner))
+      pure (.element "span" attrs (.seq inner))
     | .styled attrs =>
       let inner ← contents.mapM inlineHtml
-      pure (.tag "span" attrs (.seq inner))
+      pure (.element "span" attrs (.seq inner))
     | .image imgSrcVal alt width height cssClass =>
       let imgSrc ← match imgSrcVal with
         | .projectRelative resolved => do
@@ -247,7 +248,7 @@ instance [Monad m] [MonadBuildLog (HtmlT Slides m)] : GenreHtml Slides m where
         | (false, some c) => some c
         | (false, none)   => none
       if let some c := classVal then attrs := attrs.push ("class", c)
-      pure (.tag "img" attrs .empty)
+      pure (.element "img" attrs .empty)
     | .ofHtml html =>
       pure html
     | .slideCode scExport =>
@@ -277,7 +278,7 @@ private def blkToHtml (b : Block Slides) : HtmlT Slides m Html :=
 /-- Renders an array of inlines as a heading at the given level. -/
 private def renderHeading (level : Nat) (title : Array (Inline Slides)) : HtmlT Slides m Html := do
   let titleHtml ← title.mapM inlToHtml
-  pure (.tag s!"h{level}" #[] (.seq titleHtml))
+  pure (.element s!"h{level}" #[] (.seq titleHtml))
 
 /-- Returns {name}`true` if a {name}`Part` has any non-empty direct content blocks. -/
 private def hasDirectContent (p : Part Slides) : Bool :=
@@ -301,19 +302,19 @@ partial def renderSlidePart (config : Config) (level : Nat) (parentVertical : Bo
       let mut slides := #[]
       -- If there's direct content, create implicit first vertical sub-slide
       if hasDirectContent p then
-        slides := slides.push (.tag "section" #[] (.seq (#[heading] ++ contentHtml)))
+        slides := slides.push (.element "section" #[] (.seq (#[heading] ++ contentHtml)))
       -- Render each ## sub-part as a vertical sub-slide
       for sub in p.subParts do
         slides := slides.push (← renderSlidePart config 1 true sub)
-      pure (.tag "section" attrs (.seq slides))
+      pure (.element "section" attrs (.seq slides))
     else
       -- Single horizontal slide (no vertical sub-slides)
       let subContent ← p.subParts.mapM (renderSlidePart config 1 false)
-      pure (.tag "section" attrs (.seq (#[heading] ++ contentHtml ++ subContent)))
+      pure (.element "section" attrs (.seq (#[heading] ++ contentHtml ++ subContent)))
   else if level == 1 && parentVertical then
     -- `##` section under vertical parent: emit as vertical sub-slide (<section>)
     let subContent ← p.subParts.mapM (renderSlidePart config 2 false)
-    pure (.tag "section" attrs (.seq (#[heading] ++ contentHtml ++ subContent)))
+    pure (.element "section" attrs (.seq (#[heading] ++ contentHtml ++ subContent)))
   else
     -- `##` under non-vertical parent, or `###` and deeper: flatten (no <section> wrapper)
     let subContent ← p.subParts.mapM (renderSlidePart config (level + 1) false)
@@ -445,7 +446,7 @@ def renderFullHtml (config : Config) (title : String) (slidesBody : Html) (custo
     if config.mathPrelude.isEmpty then #[]
     else
       let js := s!"window.__versoMathPrelude = {jsString config.mathPrelude};"
-      #[{{ <script>{{Html.text false js}}</script> }}]
+      #[{{ <script>{{Html.raw js}}</script> }}]
   let themeHref := match config.theme with
     | .builtin name => s!"{libPrefix}/reveal.js/dist/theme/{name}.css"
     | .custom theme => theme.stylesheet.filename
@@ -493,7 +494,7 @@ def renderFullHtml (config : Config) (title : String) (slidesBody : Html) (custo
       <link rel="stylesheet" href={{s!"{libPrefix}/illuminate-anim.css"}} />
       <link rel="stylesheet" href={{s!"{libPrefix}/table.css"}} />
       <link rel="stylesheet" href={{s!"{libPrefix}/katex/dist/katex.min.css"}} />
-      {{ customCss.map fun css => {{ <style>{{Html.text false css}}</style> }} }}
+      {{ customCss.map fun css => {{ <style>{{Html.raw css}}</style> }} }}
       {{config.extraHead}}
     </head>
     <body>
@@ -509,7 +510,7 @@ def renderFullHtml (config : Config) (title : String) (slidesBody : Html) (custo
       {{mathPreludeScripts}}
       <script src={{s!"{libPrefix}/math.js"}}></script>
       {{extraJsScripts}}
-      <script>{{Html.text false initScript}}</script>
+      <script>{{Html.raw initScript}}</script>
       <script src={{s!"{libPrefix}/marked.min.js"}}></script>
       <script src={{s!"{libPrefix}/popper.js"}}></script>
       <script src={{s!"{libPrefix}/tippy.js"}}></script>
@@ -698,7 +699,7 @@ def slidesMain (config : Config := {}) (doc : Part Slides) : IO UInt32 := runWit
   if !(← dir.pathExists) then
     IO.FS.createDirAll dir
   let indexPath := dir / "index.html"
-  IO.FS.writeFile indexPath ("<!doctype html>\n" ++ fullHtml.asString)
+  IO.FS.writeFile indexPath ("<!doctype html>\n" ++ fullHtml.render)
 
   -- Write hover data JSON for highlighted code tooltips
   let docsJsonPath := dir / "-verso-docs.json"
diff --git a/verso-slides/VersoSlides/SlideCode/Render.lean b/verso-slides/VersoSlides/SlideCode/Render.lean
index 41a76feb6..2f3f48990 100644
--- a/verso-slides/VersoSlides/SlideCode/Render.lean
+++ b/verso-slides/VersoSlides/SlideCode/Render.lean
@@ -15,6 +15,7 @@ Renders SlideCode trees to HTML for `reveal.js`.
 
 
 open Verso Output Html
+open Lean (Html)
 open SubVerso.Highlighting (Highlighted)
 open Verso.Code (HighlightHtmlM)
 open Lean (Json toJson)
@@ -96,7 +97,7 @@ public def SlideCode.toHtml : SlideCode → HighlightHtmlM g Html
     pure {{
       <span class="tactic" "data-tactic-range"={{s!"{startPos}-{endPos}"}}>
         {{contentHtml}}
-        {{Html.tag "span" (#[("class", "tactic-state"), ("style", "display:none")] ++ fmtAttr) goalsHtml}}
+        {{Html.element "span" (#[("class", "tactic-state"), ("style", "display:none")] ++ fmtAttr) goalsHtml}}
       </span>
     }}
   | .span info content => do
@@ -118,17 +119,17 @@ public def SlideCode.toHtml : SlideCode → HighlightHtmlM g Html
     }}
   | .fragment w true content => do
     let contentHtml ← content.toHtml
-    pure (Html.tag "div" (#[("class", fragClass w)] ++ fragIndexAttr w) contentHtml)
+    pure (Html.element "div" (#[("class", fragClass w)] ++ fragIndexAttr w) contentHtml)
   | .fragment w false content => do
     let contentHtml ← content.toHtml
-    pure (Html.tag "span" (#[("class", fragClass w)] ++ fragIndexAttr w) contentHtml)
+    pure (Html.element "span" (#[("class", fragClass w)] ++ fragIndexAttr w) contentHtml)
   | .click target index => do
     let targetHtml ← target.toHtml
     let cls := "fragment slide-click-only"
     let attrs := match index with
       | some i => #[("class", cls), ("data-fragment-index", toString i)]
       | none => #[("class", cls)]
-    pure (Html.tag "span" attrs targetHtml)
+    pure (Html.element "span" attrs targetHtml)
   | .commandOutput info => do
     -- Use the highest severity for the wrapper class
     let severity := info.foldl (fun acc (s, _) => match acc, s with
diff --git a/verso-web-components/VersoWeb/Components/ArchiveEntry.lean b/verso-web-components/VersoWeb/Components/ArchiveEntry.lean
index a89e0f57e..065e13f9a 100644
--- a/verso-web-components/VersoWeb/Components/ArchiveEntry.lean
+++ b/verso-web-components/VersoWeb/Components/ArchiveEntry.lean
@@ -11,6 +11,7 @@ import VersoWeb.Util
 namespace Verso.Web.Components
 
 open Verso.Output Html
+open Lean (Html)
 open Verso.Genre.Blog Template
 
 /--
@@ -19,7 +20,7 @@ Render the metadata section (authors and date)
 private def renderArchiveMetadata (md : Post.PartMetadata) : Html :=
   {{
     <div class="metadata">
-      {{md.authors.map ({{<div class="author">{{Html.text true ·}}</div>}}) |>.toArray}}
+      {{md.authors.map ({{<div class="author">{{Html.text ·}}</div>}}) |>.toArray}}
       <div class="date">
         {{md.date.toIso8601String}}
       </div>
diff --git a/verso-web-components/VersoWeb/Components/Card/Learn.lean b/verso-web-components/VersoWeb/Components/Card/Learn.lean
index 9de43986c..6959c9e10 100644
--- a/verso-web-components/VersoWeb/Components/Card/Learn.lean
+++ b/verso-web-components/VersoWeb/Components/Card/Learn.lean
@@ -45,7 +45,7 @@ def learnCard [MonadStateOf Component.State m] [Monad m]  (card : Card) : m Html
           {{
             if card.tags.isEmpty then .empty else
               {{<div class="tags">
-                {{ card.tags.map fun tag => {{ <span class="item-tag">{{ .text true tag }}</span> }} }}
+                {{ card.tags.map fun tag => {{ <span class="item-tag">{{ .text tag }}</span> }} }}
                 </div>
               }}
           }}
diff --git a/verso-web-components/VersoWeb/Components/Title.lean b/verso-web-components/VersoWeb/Components/Title.lean
index d2c2c0bc5..d3f50f359 100644
--- a/verso-web-components/VersoWeb/Components/Title.lean
+++ b/verso-web-components/VersoWeb/Components/Title.lean
@@ -10,6 +10,7 @@ import VersoWeb.Components.Icon
 namespace Verso.Web.Components
 
 open Verso.Output Html
+open Lean (Html)
 open Verso.Genre.Blog Template
 
 def badge (content : String) (variant : String := "primary") : Html :=
@@ -33,12 +34,12 @@ block_component +directive pageTitle (level : Nat) (title : String) where
   toHtml _ _ _ _ _ := do
     saveCss (include_str "../../static/style/title.css")
 
-    return Html.tag s!"h{level}" #[("class", "page-title")] (.text true title)
+    return Html.element s!"h{level}" #[("class", "page-title")] (.text title)
 
 block_component +directive header (level : Nat) (title : String) where
   toHtml _ _ _ _ _ := do
     saveCss (include_str "../../static/style/title.css")
 
-    return Html.tag s!"h{level}" #[("id", defaultPostName.slugify title)] (.text true title)
+    return Html.element s!"h{level}" #[("id", defaultPostName.slugify title)] (.text title)
 
 end Verso.Web.Components
diff --git a/verso-web-components/VersoWeb/Features.lean b/verso-web-components/VersoWeb/Features.lean
index 37c4fede0..57fab1fef 100644
--- a/verso-web-components/VersoWeb/Features.lean
+++ b/verso-web-components/VersoWeb/Features.lean
@@ -13,7 +13,7 @@ open Verso Doc Elab
 open Lean Elab
 open Lean.Doc (CodeBlockView CodeView TextView)
 open Verso.ArgParse
-open Verso.Output (Html)
+open Lean (Html)
 
 private def codeblockContents (stx : TSyntax ``Lean.Doc.Parser.block) : Option String :=
   match CodeBlockView.of stx with
@@ -117,7 +117,7 @@ partial def toml : CodeBlockExpander
 where
   infoHtml : SourceInfo → Html → Html
     | .original leading _ trailing _, html =>
-      .text false leading.toString ++ html ++ .text false trailing.toString
+      .raw leading.toString ++ html ++ .raw trailing.toString
     | _, html => html
 
   hl (cls : String) (html : Html) : Html := {{<span class={{cls}}>{{html}}</span>}}
@@ -157,7 +157,7 @@ where
     | .node info ``Lake.Toml.decInt elts => infoHtml info <| hl "num" <| elts.map highlightToml
     | .node info ``Lake.Toml.array elts => infoHtml info <| elts.map highlightToml
     | .node info ``Lake.Toml.inlineTable elts => infoHtml info <| elts.map highlightToml
-    | .atom info str => infoHtml info (.text true str)
+    | .atom info str => infoHtml info (.text str)
     | other => {{ "Failed to highlight TOML (probably highlightToml in Lang.Features needs another pattern case): " {{toString other}} }}
 
 
@@ -169,14 +169,14 @@ def collapsedDetails : DirectiveExpander
   | args, contents => do
     let summary ← ArgParse.run (.positional `summary .string) args
     let blocks ← contents.mapM elabBlock
-    let summary ← ``(Block.other (BlockExt.blob (Html.tag "summary" #[] #[Html.text true $(quote summary)])) #[])
+    let summary ← ``(Block.other (BlockExt.blob (Html.element "summary" #[] #[Html.text $(quote summary)])) #[])
     pure #[← ``(Block.other (BlockExt.htmlWrapper "details" #[]) #[$summary, $blocks,*])]
 
 @[directive_expander TODO]
 def TODO : DirectiveExpander
   | _, contents => do
     let blocks ← contents.mapM elabBlock
-    let header ← ``(Block.other (BlockExt.blob (Html.tag "h3" #[] #[Html.text true "TODO"])) #[])
+    let header ← ``(Block.other (BlockExt.blob (Html.element "h3" #[] #[Html.text "TODO"])) #[])
     pure #[← ``(Block.other (BlockExt.htmlWrapper "div" #[("class", "TODO")]) #[$header, $blocks,*])]
 
 @[role_expander TODO]
diff --git a/verso-web-components/VersoWeb/Theme/Head.lean b/verso-web-components/VersoWeb/Theme/Head.lean
index 9a5e3eef5..00f949679 100644
--- a/verso-web-components/VersoWeb/Theme/Head.lean
+++ b/verso-web-components/VersoWeb/Theme/Head.lean
@@ -140,7 +140,7 @@ def head (siteName : String) (rootTitle : String) (config : HeadConfig) (variabl
       <link rel="preconnect" href="https://fonts.gstatic.com" crossorigin="anonymous" />
       <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Fira+Code:wght@300..700&family=Open+Sans:ital,wght@0,300..800;1,300..800&family=Oranienbaum&display=swap" />
 
-      <style> {{ .text false (variables.toCSS) }} </style>
+      <style> {{ .raw (variables.toCSS) }} </style>
 
       <link rel="apple-touch-icon" href="apple-touch-icon.png"/>
 
diff --git a/verso-web-components/VersoWeb/Theme/Post.lean b/verso-web-components/VersoWeb/Theme/Post.lean
index ea749d002..ce5798639 100644
--- a/verso-web-components/VersoWeb/Theme/Post.lean
+++ b/verso-web-components/VersoWeb/Theme/Post.lean
@@ -9,6 +9,7 @@ import VersoWeb.Components.ArchiveEntry
 import VersoWeb.Components.Aside
 
 open Verso Genre Blog Template Output Html
+open Lean (Html)
 open Verso.Web Components Util Multi
 
 namespace Verso.Web.Theme
@@ -31,7 +32,7 @@ def articleContent (title : Html) (content : Html) (metadata : Option Post.PartM
         | none => Html.empty
         | some md => {{
             <div class="metadata">
-              {{(md : Post.PartMetadata).authors.map ({{<div class="author">{{Html.text true ·}}</div>}}) |>.toArray}}
+              {{(md : Post.PartMetadata).authors.map ({{<div class="author">{{Html.text ·}}</div>}}) |>.toArray}}
               <div class="date">
                 {{md.date.toIso8601String}}
               </div>
diff --git a/verso-web-components/VersoWeb/Util.lean b/verso-web-components/VersoWeb/Util.lean
index 358f2bedb..826e4e0a1 100644
--- a/verso-web-components/VersoWeb/Util.lean
+++ b/verso-web-components/VersoWeb/Util.lean
@@ -11,7 +11,8 @@ import Std.Data.HashSet
 
 namespace Verso.Web.Util
 
-open Verso.Output Html
+open Verso
+open Lean (Html)
 open Verso Genre Blog Template ArgParse
 
 /--
@@ -70,7 +71,7 @@ Sets an attribute on an HTML element only if the value is defined.
 -/
 def setAttributeOption (attr : String) (value : Option String) (html : Html) : Html :=
   if let some value := value
-    then setAttribute attr value html
+    then Html.setAttribute attr value html
     else html
 
 /--
@@ -85,8 +86,8 @@ Extract text content from HTML, removing all tags.
 -/
  def extractText (html : Html) : String :=
   match html with
-  | Html.text _ content => content
-  | Html.tag _ _ contents => extractText contents
+  | Html.text content | Html.raw content => content
+  | Html.element _ _ contents => extractText contents
   | Html.seq contents =>
     contents.foldl (fun acc h => acc ++ extractText h) ""
 
@@ -116,14 +117,14 @@ Truncate HTML text content to a maximum length, adding "..." if truncated.
             else acc ++ "..."
         else buildResult newAcc rest
     let truncatedText := buildResult "" words
-    Html.text false truncatedText
+    Html.raw truncatedText
 
 /--
 Remove HTML wrapper and extract text content.
 -/
 partial def removeWrapper : Html → String
-  | .text _ s => s
-  | .tag _ _ h => removeWrapper h
+  | .text s | .raw s => s
+  | .element _ _ h => removeWrapper h
   | .seq hs => String.intercalate " " (hs.toList.map removeWrapper)
 
 /--
@@ -140,8 +141,9 @@ no leading slash) so that the permalink href resolves correctly against the Vers
 -/
 partial def addSlug (page : String) : Html → Html
   | .seq h => .seq (h.map (addSlug page))
-  | .text s e => .text s e
-  | .tag t a h =>
+  | .text s => .text s
+  | .raw s => .raw s
+  | .element t a h =>
     let findId (attrs : Array (String × String)) := (attrs.find? (·.1 == "id")).map (·.2)
     let theresId (attrs : Array (String × String)) := attrs.any (·.1 == "id")
 
@@ -149,19 +151,19 @@ partial def addSlug (page : String) : Html → Html
     | "h1" =>
       let slug := findId a |>.getD (createSlug (removeWrapper h))
       let finalAttrs := if theresId a then a else a.push ("id", slug)
-      .tag "h1" finalAttrs h
+      .element "h1" finalAttrs h
     | "h2" | "h3" | "h4" =>
       let slug := findId a |>.getD (createSlug (removeWrapper h))
       let finalAttrs := if theresId a then a else a.push ("id", slug)
       let hasNoPermalink := a.any (fun (k, v) => k == "class" && v.splitOn.any (· == "no-permalink"))
       if hasNoPermalink then
-        .tag t finalAttrs h
+        .element t finalAttrs h
       else
-        let anchor := Html.tag "a" #[("href", s!"{page}#{slug}"), ("title", "Permalink")] #[Html.text false "🔗"]
-        let widget := Html.tag "span" #[("class", "permalink-widget inline")] #[anchor]
-        .tag t finalAttrs (.seq #[h, widget])
+        let anchor := Html.element "a" #[("href", s!"{page}#{slug}"), ("title", "Permalink")] #[Html.raw "🔗"]
+        let widget := Html.element "span" #[("class", "permalink-widget inline")] #[anchor]
+        .element t finalAttrs (.seq #[h, widget])
     | _ =>
-      .tag t a (addSlug page h)
+      .element t a (addSlug page h)
 
 /--
 Collect H1-H4 headings and build a table of contents.
@@ -170,7 +172,7 @@ partial def collectH1 (html : Html) (page : String) : Option Html :=
     let res := (collect [] html |>.reverse)
     if ¬ res.isEmpty then
       let (html, _) := compact 2 res
-      Html.tag "ol" #[] #[Html.seq (html.toArray |>.map (Html.tag "li" #[]))]
+      Html.element "ol" #[] #[Html.seq (html.toArray |>.map (Html.element "li" #[]))]
     else
       none
   where
@@ -182,8 +184,8 @@ partial def collectH1 (html : Html) (page : String) : Option Html :=
       | _ => 0
 
     collect (col : List (Nat × String)) : Html → List (Nat × String)
-      | .text _ _ => col
-      | .tag t _ h =>
+      | .text _ | .raw _ => col
+      | .element t _ h =>
         match t with
         | "h1" | "h2" | "h3" | "h4" => (getLevel t, removeWrapper h) :: col
         | _ => collect col h
@@ -193,10 +195,10 @@ partial def collectH1 (html : Html) (page : String) : Option Html :=
       | (level, str) :: xs =>
         if level = current then
           let slug := createSlug str
-          let headingLink := Html.tag "a" #[("href", s!"{page}#{slug}")] #[Html.text false str]
+          let headingLink := Html.element "a" #[("href", s!"{page}#{slug}")] #[Html.raw str]
 
           let (children, remaining) := compactChildren (level + 1) xs
-          let item := if children.isEmpty then headingLink else Html.seq #[headingLink, Html.tag "ol" #[] (Html.seq children.toArray)]
+          let item := if children.isEmpty then headingLink else Html.seq #[headingLink, Html.element "ol" #[] (Html.seq children.toArray)]
           let (siblings, final) := compact level remaining
 
           (item :: siblings, final)
@@ -211,7 +213,7 @@ partial def collectH1 (html : Html) (page : String) : Option Html :=
         if level >= minLevel then
           let (item, remaining) := compact level ((level, str) :: xs)
           let (siblings, final) := compactChildren minLevel remaining
-          (item.map (Html.tag "li" #[]) ++ siblings, final)
+          (item.map (Html.element "li" #[]) ++ siblings, final)
         else
           ([], (level, str) :: xs)
       | [] => ([], [])
@@ -219,8 +221,8 @@ partial def collectH1 (html : Html) (page : String) : Option Html :=
 defmethod Html.classNames (html : Html) : Array  String :=
   let rec go (h : Html) (acc : Std.HashSet String) : Std.HashSet String :=
     match h with
-    | .text _ _ => acc
-    | .tag _ attrs contents =>
+    | .text _ | .raw _ => acc
+    | .element _ attrs contents =>
       let classAcc := attrs.foldl (fun acc (k, v) =>
         if k == "class" then
           -- Split class string by whitespace and add each class
diff --git a/verso/doc/UsersGuide/Output/HTML.lean b/verso/doc/UsersGuide/Output/HTML.lean
index adb7d31ec..dcf7fa994 100644
--- a/verso/doc/UsersGuide/Output/HTML.lean
+++ b/verso/doc/UsersGuide/Output/HTML.lean
@@ -15,6 +15,7 @@ open InlineLean
 open Verso.Doc
 
 open Verso.Output
+open Lean (Html)
 
 open Verso.Code
 
@@ -26,24 +27,22 @@ tag := "output-html"
 While most users of Verso don't need to worry about the specific details of the HTML that it produces, authors of new {tech}[genres] or of substantial extensions to existing genres may need to produce custom HTML.
 Verso's HTML output follows a number of conventions and uses built-in libraries and features.
 
-Verso's {name}`Html` type represents HTML documents.
-They are typically produced using an embedded DSL that is available when the namespace `Verso.Output.Html` is opened.
+Lean's {name}`Html` type represents HTML documents.
+In Verso, they are typically produced using an embedded DSL that is available when the namespace `Verso.Output.Html` is opened.
 
 {docstring Html}
 
 {docstring Html.empty}
 
-{docstring Html.fromArray}
+{docstring Html.ofArray}
 
-{docstring Html.fromList}
+{docstring Html.ofList}
 
 {docstring Html.append}
 
-{docstring Html.visitM}
+{docstring Html.rewritePostM}
 
-{docstring Html.format}
-
-{docstring Html.asString}
+{docstring Html.render}
 
 HTML documents are written in double curly braces, in a syntax very much like HTML itself.
 The differences are:
@@ -59,19 +58,12 @@ def mkList (xs : List Html) : Html :=
   {{ <ul> {{ xs.map ({{<li>{{·}}</li>}}) }} </ul>}}
 
 #eval mkList ["A", {{<emph>"B"</emph>}}, "C"]
-  |>.asString
+  |>.render
   |> IO.println
 ```
 
 ```leanOutput htmllist
-<ul>
-  <li>
-    A</li>
-  <li>
-    <emph>B</emph></li>
-  <li>
-    C</li>
-  </ul>
+<ul><li>A</li><li><emph>B</emph></li><li>C</li></ul>
 ```
 
 # Conventions
diff --git a/verso/doc/UsersGuide/Websites.lean b/verso/doc/UsersGuide/Websites.lean
index 116214076..57e48a79a 100644
--- a/verso/doc/UsersGuide/Websites.lean
+++ b/verso/doc/UsersGuide/Websites.lean
@@ -63,7 +63,7 @@ The URL layout of a site is specified via a {name Blog.Site}`Site`:
 These are usually constructed using a small embedded configuration language.
 
 A blog is rendered using a theme, which is a collection of templates.
-Templates are monadic functions that construct {name Verso.Output.Html}`Html` from a set of dynamically-typed parameters.
+Templates are monadic functions that construct {name Lean.Html}`Html` from a set of dynamically-typed parameters.
 
 {docstring Blog.Theme}
 
diff --git a/verso/src/tests/VersoTests/GenericCode.lean b/verso/src/tests/VersoTests/GenericCode.lean
index 44f395989..c502e7707 100644
--- a/verso/src/tests/VersoTests/GenericCode.lean
+++ b/verso/src/tests/VersoTests/GenericCode.lean
@@ -42,21 +42,21 @@ info: Verso.Doc.Part.mk
 #test_msgs in
   #eval code1.toPart
 /--
-info: Verso.Output.Html.tag
+info: Lean.Html.element
   "section"
   #[]
-  (Verso.Output.Html.seq
-    #[Verso.Output.Html.tag "h1" #[] (Verso.Output.Html.seq #[Verso.Output.Html.text true "More writing"]),
-      Verso.Output.Html.tag
+  (Lean.Html.seq
+    #[Lean.Html.element "h1" #[] (Lean.Html.seq #[Lean.Html.text "More writing"]),
+      Lean.Html.element
         "section"
         #[]
-        (Verso.Output.Html.seq
-          #[Verso.Output.Html.tag "h2" #[] (Verso.Output.Html.seq #[Verso.Output.Html.text true "Section 1"]),
-            Verso.Output.Html.tag "p" #[] (Verso.Output.Html.seq #[Verso.Output.Html.text true "Here's some code"]),
-            Verso.Output.Html.tag
+        (Lean.Html.seq
+          #[Lean.Html.element "h2" #[] (Lean.Html.seq #[Lean.Html.text "Section 1"]),
+            Lean.Html.element "p" #[] (Lean.Html.text "Here's some code"),
+            Lean.Html.element
               "pre"
               #[]
-              (Verso.Output.Html.text true "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n")])])
+              (Lean.Html.text "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n")])])
 -/
 #test_msgs in
   #eval Doc.Genre.none.toHtml (m := Id) {} () () {} {} {} code1.toPart |>.run .empty |>.fst
diff --git a/verso/src/tests/VersoTests/HoverMerge.lean b/verso/src/tests/VersoTests/HoverMerge.lean
index 542871abf..5b075e8d7 100644
--- a/verso/src/tests/VersoTests/HoverMerge.lean
+++ b/verso/src/tests/VersoTests/HoverMerge.lean
@@ -11,7 +11,8 @@ meta import SubVerso.Highlighting
 
 open SubVerso.Highlighting (Highlighted)
 open Verso.Code (takeAttrs)
-open Verso.Output (Html)
+open Verso.Output
+open Lean (Html)
 
 namespace Verso.HoverMergeTest
 
@@ -21,64 +22,64 @@ shares the token's extent: `Highlighted.normalize` makes the sole-token shape re
 and `takeAttrs` moves the token's hover attributes up to the span.
 -/
 
-def tok : Html := .tag "span" #[("class", "token"), ("data-verso-hover", "5")] (.text true "x")
-def tokNoHover : Html := .tag "span" #[("class", "token")] (.text true "x")
+def tok : Html := .element "span" #[("class", "token"), ("data-verso-hover", "5")] (.text "x")
+def tokNoHover : Html := .element "span" #[("class", "token")] (.text "x")
 
 -- The attribute is taken from a bare element.
 #test_guard takeAttrs #["data-verso-hover"] tok == (#[("data-verso-hover", "5")], tokNoHover)
 
 -- The attribute is found through a wrapping element, such as a link.
-#test_guard takeAttrs #["data-verso-hover"] (.tag "a" #[("href", "x.html")] tok) ==
-  (#[("data-verso-hover", "5")], .tag "a" #[("href", "x.html")] tokNoHover)
+#test_guard takeAttrs #["data-verso-hover"] (.element "a" #[("href", "x.html")] tok) ==
+  (#[("data-verso-hover", "5")], .element "a" #[("href", "x.html")] tokNoHover)
 
 -- Attributes are gathered across the wrappers of a sole element: the hover from the token
 -- and the extra links from the link element around it.
 #test_guard takeAttrs #["data-verso-hover", "data-verso-links"]
-    (.tag "a" #[("data-verso-links", "[]")] tok) ==
-  (#[("data-verso-links", "[]"), ("data-verso-hover", "5")], .tag "a" #[] tokNoHover)
+    (.element "a" #[("data-verso-links", "[]")] tok) ==
+  (#[("data-verso-links", "[]"), ("data-verso-hover", "5")], .element "a" #[] tokNoHover)
 
 -- Only the attributes that are present appear in the result.
 #test_guard takeAttrs #["data-verso-hover", "data-verso-links"]
-    (.tag "a" #[("data-verso-links", "[]")] tokNoHover) ==
-  (#[("data-verso-links", "[]")], .tag "a" #[] tokNoHover)
+    (.element "a" #[("data-verso-links", "[]")] tokNoHover) ==
+  (#[("data-verso-links", "[]")], .element "a" #[] tokNoHover)
 
 def tokLinked : Html :=
-  .tag "span" #[("class", "token"), ("data-verso-hover", "5"), ("data-verso-links", "[2]")]
-    (.text true "x")
+  .element "span" #[("class", "token"), ("data-verso-hover", "5"), ("data-verso-links", "[2]")]
+    (.text "x")
 
 -- Each attribute is taken from the outermost element that carries it, and repeats on
 -- elements nested inside stay in place.
 #test_guard takeAttrs #["data-verso-hover", "data-verso-links"]
-    (.tag "a" #[("data-verso-hover", "9")] tokLinked) ==
+    (.element "a" #[("data-verso-hover", "9")] tokLinked) ==
   (#[("data-verso-hover", "9"), ("data-verso-links", "[2]")],
-   .tag "a" #[] (.tag "span" #[("class", "token"), ("data-verso-hover", "5")] (.text true "x")))
+   .element "a" #[] (.element "span" #[("class", "token"), ("data-verso-hover", "5")] (.text "x")))
 #test_guard takeAttrs #["data-verso-hover", "data-verso-links"]
-    (.tag "a" #[("data-verso-links", "[1]")] tokLinked) ==
+    (.element "a" #[("data-verso-links", "[1]")] tokLinked) ==
   (#[("data-verso-links", "[1]"), ("data-verso-hover", "5")],
-   .tag "a" #[] (.tag "span" #[("class", "token"), ("data-verso-links", "[2]")] (.text true "x")))
+   .element "a" #[] (.element "span" #[("class", "token"), ("data-verso-links", "[2]")] (.text "x")))
 
 -- The outermost attribute wins, and inner ones are left in place.
-#test_guard takeAttrs #["data-verso-hover"] (.tag "a" #[("data-verso-hover", "9")] tok) ==
-  (#[("data-verso-hover", "9")], .tag "a" #[] tok)
+#test_guard takeAttrs #["data-verso-hover"] (.element "a" #[("data-verso-hover", "9")] tok) ==
+  (#[("data-verso-hover", "9")], .element "a" #[] tok)
 
 -- Empty content around a sole element does not block the search.
-#test_guard takeAttrs #["data-verso-hover"] (.seq #[.text true "", tok, .seq #[]]) ==
+#test_guard takeAttrs #["data-verso-hover"] (.seq #[.text "", tok, .seq #[]]) ==
   (#[("data-verso-hover", "5")], tokNoHover)
 
 -- Adjacent content blocks the search, including whitespace.
-#test_guard takeAttrs #["data-verso-hover"] (.seq #[tok, .text true "y"]) ==
-  (#[], .seq #[tok, .text true "y"])
+#test_guard takeAttrs #["data-verso-hover"] (.seq #[tok, .text "y"]) ==
+  (#[], .seq #[tok, .text "y"])
 #test_guard takeAttrs #["data-verso-hover"] (.seq #[tok, tokNoHover]) == (#[], .seq #[tok, tokNoHover])
-#test_guard takeAttrs #["data-verso-hover"] (.seq #[.text true " ", tok]) ==
-  (#[], .seq #[.text true " ", tok])
+#test_guard takeAttrs #["data-verso-hover"] (.seq #[.text " ", tok]) ==
+  (#[], .seq #[.text " ", tok])
 
 -- Adjacent content inside a wrapper blocks the search.
-#test_guard takeAttrs #["data-verso-hover"] (.tag "a" #[] (.seq #[tok, tokNoHover])) ==
-  (#[], .tag "a" #[] (.seq #[tok, tokNoHover]))
+#test_guard takeAttrs #["data-verso-hover"] (.element "a" #[] (.seq #[tok, tokNoHover])) ==
+  (#[], .element "a" #[] (.seq #[tok, tokNoHover]))
 
 -- Content without the attributes is unchanged.
 #test_guard takeAttrs #["data-verso-hover"] tokNoHover == (#[], tokNoHover)
-#test_guard takeAttrs #["data-verso-hover"] (.text true "x") == (#[], .text true "x")
+#test_guard takeAttrs #["data-verso-hover"] (.text "x") == (#[], .text "x")
 #test_guard takeAttrs #["data-verso-hover"] (.seq #[]) == (#[], .seq #[])
 
 def hlTok : Highlighted := .token ⟨.keyword none none none, "rfl"⟩
diff --git a/verso/src/tests/VersoTests/Html.lean b/verso/src/tests/VersoTests/Html.lean
index f8293079c..c99b22eb9 100644
--- a/verso/src/tests/VersoTests/Html.lean
+++ b/verso/src/tests/VersoTests/Html.lean
@@ -9,7 +9,7 @@ meta import all Verso.Output.Html
 
 namespace Verso.Tests.Html
 
-open Verso.Output
+open Lean (Html)
 open Verso.Output.Html
 
 /-! ## Tests for HTML syntax macros -/
@@ -17,10 +17,10 @@ open Verso.Output.Html
 private def testAttrs := {{ <html charset="UTF-8" charset = "UTF-8" a="b" a-b-c="44" {{#[("x", "y")] }} /> }}
 
 /--
-info: Verso.Output.Html.tag
+info: Lean.Html.element
   "html"
   #[("charset", "UTF-8"), ("charset", "UTF-8"), ("a", "b"), ("a-b-c", "44"), ("x", "y")]
-  (Verso.Output.Html.seq #[])
+  (Lean.Html.seq #[])
 -/
 #test_msgs in
 #eval testAttrs
@@ -29,10 +29,10 @@ private def testAttrsAntiquotes :=
   {{ <html charset={{"UTF" ++ "-8"}} "charset" = "UTF-8" a="b" a-b-c="44" {{#[("x", "y")]}} /> }}
 
 /--
-info: Verso.Output.Html.tag
+info: Lean.Html.element
   "html"
   #[("charset", "UTF-8"), ("charset", "UTF-8"), ("a", "b"), ("a-b-c", "44"), ("x", "y")]
-  (Verso.Output.Html.seq #[])
+  (Lean.Html.seq #[])
 -/
 #test_msgs in
 #eval testAttrsAntiquotes
@@ -52,27 +52,26 @@ private def test : Html := {{
 }}
 
 /--
-info: Verso.Output.Html.tag
+info: Lean.Html.element
   "html"
   #[]
-  (Verso.Output.Html.seq
-    #[Verso.Output.Html.tag
+  (Lean.Html.seq
+    #[Lean.Html.element
         "head"
         #[]
-        (Verso.Output.Html.seq
-          #[Verso.Output.Html.tag "meta" #[("charset", "UTF-8")] (Verso.Output.Html.seq #[]),
-            Verso.Output.Html.tag "script" #[] (Verso.Output.Html.seq #[])]),
-      Verso.Output.Html.tag
+        (Lean.Html.seq
+          #[Lean.Html.element "meta" #[("charset", "UTF-8")] (Lean.Html.seq #[]),
+            Lean.Html.element "script" #[] (Lean.Html.seq #[])]),
+      Lean.Html.element
         "body"
         #[("lang", "en"), ("class", "thing"), ("data-foo", "data foo")]
-        (Verso.Output.Html.seq
-          #[Verso.Output.Html.tag "input" #[("type", "checkbox"), ("checked", "")] (Verso.Output.Html.seq #[]),
-            Verso.Output.Html.tag
+        (Lean.Html.seq
+          #[Lean.Html.element "input" #[("type", "checkbox"), ("checked", "")] (Lean.Html.seq #[]),
+            Lean.Html.element
               "p"
               #[]
-              (Verso.Output.Html.seq
-                #[Verso.Output.Html.text true "foo bar", Verso.Output.Html.tag "br" #[] (Verso.Output.Html.seq #[]),
-                  Verso.Output.Html.text true "hey"])])])
+              (Lean.Html.seq
+                #[Lean.Html.text "foo bar", Lean.Html.element "br" #[] (Lean.Html.seq #[]), Lean.Html.text "hey"])])])
 -/
 #test_msgs in
   #eval test
@@ -81,7 +80,7 @@ private def leanKwTest : Html := {{
   <label for="foo">"Blah"</label>
 }}
 
-/-- info: Verso.Output.Html.tag "label" #[("for", "foo")] (Verso.Output.Html.text true "Blah") -/
+/-- info: Lean.Html.element "label" #[("for", "foo")] (Lean.Html.text "Blah") -/
 #test_msgs in
   #eval leanKwTest
 
@@ -94,33 +93,3 @@ Hint: Remove contents
 -/
 #test_msgs in
   #eval show Html from {{ <br>"foo" "foo"</br> }}
-
-/--
-info: |
-<html>
-  <head>
-    <meta charset="UTF-8">
-    <script></script>
-    </head>
-  <body lang="en" class="thing" data-foo="data foo">
-    <input type="checkbox" checked=""><p>
-      foo bar<br>hey</p>
-    </body>
-  </html>
--/
-#test_msgs in
-  #eval IO.println <| "|\n" ++ test.asString
-
-/-! ## Tests for escaping -/
-
-/-- info: "<p>x &amp; y &amp;lt; &lt;z&gt;</p>" -/
-#guard_msgs in
-  #eval Html.asString {{ <p>"x & y &lt; <z>"</p> }} (breakLines := false)
-
-/-- info: "<p>x & y &lt; <em>z</em></p>" -/
-#guard_msgs in
-  #eval Html.asString (.tag "p" #[] (.text false "x & y &lt; <em>z</em>")) (breakLines := false)
-
-/-- info: "<p class=\"a&amp;b&quot;c\">x</p>" -/
-#guard_msgs in
-  #eval Html.asString {{ <p class="a&b\"c">"x"</p> }} (breakLines := false)
diff --git a/verso/src/tests/VersoTests/HtmlHoist.lean b/verso/src/tests/VersoTests/HtmlHoist.lean
index 18382e88e..fd0042dea 100644
--- a/verso/src/tests/VersoTests/HtmlHoist.lean
+++ b/verso/src/tests/VersoTests/HtmlHoist.lean
@@ -54,11 +54,11 @@ private def note (label : String) : Html :=
 #test_guard compact (hoist "margin" {{"text without a barrier"}}) ==
   "text without a barrier"
 
-#test_guard compact (.tag "span" #[
+#test_guard compact (.element "span" #[
   (generatedWrapperAttr, ""),
   (hoistAttr, "margin"),
   ("class", "kept")
-] (.text true "text")) ==
+] (.text "text")) ==
   "<span class=\"kept\">text</span>"
 
 #test_guard compact (barrier "margin" false {{<div>{{note "custom"}}</div>}}) ==
@@ -128,14 +128,14 @@ private def futureNote (label : String) : Html :=
 }})) ==
   "<span data-verso-hoisted=\"before\">first</span><div></div><span data-verso-hoisted=\"after\">second</span>"
 
-#test_guard compact (.tag "div" #[
+#test_guard compact (.element "div" #[
   (hoistAttr, "none"),
   (barrierAttr, "none"),
   (barrierBeforeAttr, "none"),
   (noBarrierAttr, "none"),
   (suppressAttr, "none"),
   (suppressibleAttr, "none")
-] (.text true "clean")) == "<div>clean</div>"
+] (.text "clean")) == "<div>clean</div>"
 
 private def titleWithMarginalia : Html :=
   {{"Title"{{marker "1"}}{{note "title note"}}}}
@@ -208,8 +208,8 @@ where
     let attrs ← sizedArrayOf do return (← arbitrary, ← arbitrary)
     frequency (pure contents) [
       (2, pure contents),
-      (2, pure <| .tag (← arbitrary) attrs contents),
-      (1, pure <| .tag "table" attrs contents)
+      (2, pure <| .element (← arbitrary) attrs contents),
+      (1, pure <| .element "table" attrs contents)
     ]
 
 instance : ArbitraryFueled HoistCase where
diff --git a/verso/src/tests/VersoTests/NestedTacticHtml.lean b/verso/src/tests/VersoTests/NestedTacticHtml.lean
index 7e140c904..702927128 100644
--- a/verso/src/tests/VersoTests/NestedTacticHtml.lean
+++ b/verso/src/tests/VersoTests/NestedTacticHtml.lean
@@ -20,7 +20,7 @@ open SubVerso.Compat.Frontend (processCommands)
 open SubVerso.Highlighting (Highlighted highlightFrontendResult)
 open Verso.Code (HighlightHtmlM)
 open Verso.Doc (Genre)
-open Verso.Output (Html)
+open Verso.Output
 open Lean Elab Command
 
 namespace Verso.NestedTacticHtmlTest
@@ -111,8 +111,8 @@ def hasClass (attrs : Array (String × String)) (cls : String) : Bool :=
 
 /-- The concatenated text content of an HTML fragment. -/
 partial def htmlText : Html → String
-  | .text _ s => s
-  | .tag _ _ contents => htmlText contents
+  | .text s | .raw s => s
+  | .element _ _ contents => htmlText contents
   | .seq xs => xs.foldl (fun acc x => acc ++ htmlText x) ""
 
 /-- The direct children of an HTML fragment. -/
@@ -122,9 +122,9 @@ def directChildren : Html → Array Html
 
 /-- Whether an HTML fragment renders as nothing visible (whitespace or empty). -/
 partial def htmlInsignificant : Html → Bool
-  | .text _ s => s.trimAscii.isEmpty
+  | .text s | .raw s => s.trimAscii.isEmpty
   | .seq xs => xs.all htmlInsignificant
-  | .tag .. => false
+  | .element .. => false
 
 /-- The last visible element of an HTML fragment, looking through `.seq` tails. -/
 partial def htmlLastVisible? : Html → Option Html
@@ -135,12 +135,12 @@ partial def htmlLastVisible? : Html → Option Html
 def childSpanWithClass (contents : Html) (cls : String) : Option Html :=
   (directChildren contents).find? fun h =>
     match h with
-    | .tag "span" a _ => hasClass a cls
+    | .element "span" a _ => hasClass a cls
     | _ => false
 
 /-- Whether `html` is a `<span class="tactic">` whose own state shows "no goals". -/
 def isNoGoalsState : Html → Bool
-  | .tag "span" attrs contents =>
+  | .element "span" attrs contents =>
     if hasClass attrs "tactic" then
       match childSpanWithClass contents "tactic-state" with
       | some s => htmlText s |>.contains "All goals completed"
@@ -152,7 +152,7 @@ def isNoGoalsState : Html → Bool
 def labelContents (contents : Html) : Html :=
   let html? :=
     directChildren contents |>.findSome? fun
-      | .tag "label" _ c => some c
+      | .element "label" _ c => some c
       | _ => none
   html?.getD .empty
 
@@ -163,15 +163,15 @@ states nested inside each one. A toggle is a `<span class="tactic">` whose own s
 -/
 partial def proofStates : Html → List ProofState
   | .seq xs => xs.toList.flatMap proofStates
-  | .tag name attrs contents =>
+  | .element name attrs contents =>
     if name == "span" && hasClass attrs "tactic" then
       let label := labelContents contents
-      [{ noGoals := isNoGoalsState (.tag name attrs contents),
+      [{ noGoals := isNoGoalsState (.element name attrs contents),
          endsWithNoGoals := htmlLastVisible? label |>.map isNoGoalsState |>.getD false,
          children := proofStates label }]
     else
       proofStates contents
-  | .text .. => []
+  | _ => []
 
 /--
 Whether any proof state with goals ends with a no-goals proof state — the redundant nesting that
diff --git a/verso/src/tests/VersoTests/SerializationGenerators.lean b/verso/src/tests/VersoTests/SerializationGenerators.lean
index d60dbab74..ded2ec6e0 100644
--- a/verso/src/tests/VersoTests/SerializationGenerators.lean
+++ b/verso/src/tests/VersoTests/SerializationGenerators.lean
@@ -259,30 +259,31 @@ where
   html : Nat → Gen Html
     | 0 => text
     | n + 1 =>
-      oneOf #[text, tag n, seq n] (by simp)
-  text := .text <$> arbitrary <*> arbitrary
+      oneOf #[text, raw, tag n, seq n] (by simp)
+  text := .text <$> arbitrary
+  raw := .raw <$> arbitrary
   tag n := do
     let name ← arbitrary
     let attrs ← sizedArrayOf do return (← arbitrary, ← arbitrary)
     let content ← (html n).resize (· - 1)
-    return .tag name attrs content
+    return .element name attrs content
   seq n := .seq <$> sizedArrayOf (html n)
 
 partial instance : Shrinkable Html where
   shrink := shrinkHtml
 where
   shrinkHtml
-    | .text true s =>
-      .text false s :: (shrink s |>.map (.text true))
-    | .text false s =>
-      shrink s |>.map (.text true)
+    | .text s =>
+      .raw s :: (shrink s |>.map .text)
+    | .raw s =>
+      shrink s |>.map .text
     | .seq xs =>
       have : Shrinkable Html := ⟨shrinkHtml⟩
       shrink xs |>.map (.seq)
-    | .tag name attrs content =>
-      (shrink name |>.map (.tag · attrs content)) ++
-      (shrink attrs |>.map (.tag name · content)) ++
-      (shrinkHtml content |>.map (.tag name attrs ·))
+    | .element name attrs content =>
+      (shrink name |>.map (.element · attrs content)) ++
+      (shrink attrs |>.map (.element name · content)) ++
+      (shrinkHtml content |>.map (.element name attrs ·))
 end
 
 section
@@ -402,7 +403,7 @@ def testRefObject := testProp <| ∀ (obj : RefObject), roundTripOk obj
 def testRemoteInfo := testProp <| ∀ (info : RemoteInfo), roundTripOk info
 def testAllRemotes := testProp <| ∀ (remotes : AllRemotes), roundTripOk remotes
 def testTraverseState := testProp <| ∀ (st : Verso.Genre.Manual.TraverseState), roundTripOk st
-def testHtml := testProp <| ∀ (html : Verso.Output.Html), roundTripOk html
+def testHtml := testProp <| ∀ (html : Html), roundTripOk html
 def testDataFile := testProp <| ∀ (f : Verso.Genre.Manual.DataFile), roundTripOk f
 def testNumbering := testProp <| ∀ (n : Verso.Genre.Manual.Numbering), roundTripOk n
 def testXrefSource := testProp <| ∀ (src : XrefSource), isEqOk (XrefSource.fromJson? src.toJson) src
diff --git a/verso/src/tests/VersoTests/VersoManual/Html/SoftHyphenate.lean b/verso/src/tests/VersoTests/VersoManual/Html/SoftHyphenate.lean
index 4e88ddb3d..707a30cc1 100644
--- a/verso/src/tests/VersoTests/VersoManual/Html/SoftHyphenate.lean
+++ b/verso/src/tests/VersoTests/VersoManual/Html/SoftHyphenate.lean
@@ -11,24 +11,24 @@ open Verso.Genre.Manual
 /-- info: "blahNotCode<code><a>foo&shy;Bar&shy;Baz</a></code>" -/
 #test_msgs in
 open Verso.Output Html in
-#eval softHyphenateIdentifiers {{"blahNotCode"<code><a>"fooBarBaz"</a></code>}} |>.asString
+#eval softHyphenateIdentifiers {{"blahNotCode"<code><a>"fooBarBaz"</a></code>}} |>.render
 
-/-- info: "<code>abc.<wbr>def.<wbr>ghi.<wbr>jkl</code>" -/
+/-- info: "<code>abc.<wbr/>def.<wbr/>ghi.<wbr/>jkl</code>" -/
 #test_msgs in
 open Verso.Output Html in
-#eval softHyphenateIdentifiers {{<code>"abc.def.ghi.jkl"</code>}} |>.asString
+#eval softHyphenateIdentifiers {{<code>"abc.def.ghi.jkl"</code>}} |>.render
 
-/-- info: "<code>ABC.<wbr>DEF</code>" -/
+/-- info: "<code>ABC.<wbr/>DEF</code>" -/
 #test_msgs in
 open Verso.Output Html in
-#eval softHyphenateIdentifiers {{<code>"ABC.DEF"</code>}} |>.asString
+#eval softHyphenateIdentifiers {{<code>"ABC.DEF"</code>}} |>.render
 
-/-- info: "blahNotCode<code><a>fooBa.<wbr>rBaz.<wbr>ab&shy;CD</a></code>" -/
+/-- info: "blahNotCode<code><a>fooBa.<wbr/>rBaz.<wbr/>ab&shy;CD</a></code>" -/
 #test_msgs in
 open Verso.Output Html in
-#eval softHyphenateIdentifiers {{"blahNotCode"<code><a>"fooBa.rBaz.abCD"</a></code>}} |>.asString
+#eval softHyphenateIdentifiers {{"blahNotCode"<code><a>"fooBa.rBaz.abCD"</a></code>}} |>.render
 
-/-- info: "blahNotCode<code><a>fooBa...<wbr>rBaz.<wbr>ab&shy;CD</a></code>" -/
+/-- info: "blahNotCode<code><a>fooBa...<wbr/>rBaz.<wbr/>ab&shy;CD</a></code>" -/
 #test_msgs in
 open Verso.Output Html in
-#eval softHyphenateIdentifiers {{"blahNotCode"<code><a>"fooBa...rBaz.abCD"</a></code>}} |>.asString
+#eval softHyphenateIdentifiers {{"blahNotCode"<code><a>"fooBa...rBaz.abCD"</a></code>}} |>.render
diff --git a/verso/src/tests/VersoTests/VersoManual/Sections.lean b/verso/src/tests/VersoTests/VersoManual/Sections.lean
index 9bf8a63b9..98cef6d40 100644
--- a/verso/src/tests/VersoTests/VersoManual/Sections.lean
+++ b/verso/src/tests/VersoTests/VersoManual/Sections.lean
@@ -52,7 +52,7 @@ private def renderDoc : IO String := do
         |>.run remotes
         |>.run extension_impls%
         |>.run logger
-    rendered.set html.asString
+    rendered.set html.render
   unless exitCode == 0 do
     throw <| IO.userError "Manual docstring HTML rendering logged errors"
   rendered.get
diff --git a/verso/src/verso-blog/VersoBlog.lean b/verso/src/verso-blog/VersoBlog.lean
index d6583ce2c..933ef102e 100644
--- a/verso/src/verso-blog/VersoBlog.lean
+++ b/verso/src/verso-blog/VersoBlog.lean
@@ -892,7 +892,7 @@ where
     else
       pure attr
   rwTag (tag : String) (attrs : Array (String × String)) (content : Html) : ReaderT TraverseContext Id (Option Html) := do
-    pure <| some <| .tag tag (← attrs.mapM rwAttr) content
+    pure <| some <| .element tag (← attrs.mapM rwAttr) content
 
 open Verso.Code.External
 
diff --git a/verso/src/verso-blog/VersoBlog/Basic.lean b/verso/src/verso-blog/VersoBlog/Basic.lean
index d72c4ddfc..13fd2eb81 100644
--- a/verso/src/verso-blog/VersoBlog/Basic.lean
+++ b/verso/src/verso-blog/VersoBlog/Basic.lean
@@ -24,7 +24,7 @@ public import VersoBlog.LexedText
 public section
 
 open Std (HashSet HashMap)
-open Lean (Json ToJson FromJson)
+open Lean (Json ToJson FromJson Html)
 
 open Verso Doc Output Html Code
 open Verso.Multi
diff --git a/verso/src/verso-blog/VersoBlog/Component.lean b/verso/src/verso-blog/VersoBlog/Component.lean
index 9d5bbf696..488259a4d 100644
--- a/verso/src/verso-blog/VersoBlog/Component.lean
+++ b/verso/src/verso-blog/VersoBlog/Component.lean
@@ -18,6 +18,7 @@ open Verso.Doc
 open Verso Output Html
 
 open Std (HashSet)
+open Lean (Html)
 
 namespace Verso.Genre.Blog
 
diff --git a/verso/src/verso-blog/VersoBlog/Generate.lean b/verso/src/verso-blog/VersoBlog/Generate.lean
index c9ed0c861..bd41b1441 100644
--- a/verso/src/verso-blog/VersoBlog/Generate.lean
+++ b/verso/src/verso-blog/VersoBlog/Generate.lean
@@ -15,6 +15,7 @@ public section
 open Verso Doc Output Html HtmlT FS
 open Verso.Code.Hover (State)
 open Verso.Code (LinkTargets)
+open Lean (Html)
 
 namespace Verso.Genre.Blog
 
@@ -166,7 +167,7 @@ def writePage (theme : Theme) (params : Template.Params) (template : Template :=
   let header := (← read).header
   IO.FS.withFile ((← currentDir).join "index.html") .write fun h => do
     h.putStrLn header
-    h.putStrLn output.asString
+    h.putStrLn output.render
 
 def writeBlog (theme : Theme) (id : Lean.Name) (txt : Part Page) (posts : Array BlogPost) : GenerateM Unit := do
   -- path from site to here
diff --git a/verso/src/verso-blog/VersoBlog/Template.lean b/verso/src/verso-blog/VersoBlog/Template.lean
index 56aba8ad7..7bb365c26 100644
--- a/verso/src/verso-blog/VersoBlog/Template.lean
+++ b/verso/src/verso-blog/VersoBlog/Template.lean
@@ -24,6 +24,7 @@ public section
 open Std (HashSet TreeMap)
 
 open Verso Doc Output Html HtmlT
+open Lean (Html)
 open Verso.Genre Blog
 open SubVerso.Highlighting
 
@@ -47,11 +48,11 @@ def getD [TypeName α] (value : Val) (default : α) : α :=
 end Params.Val
 
 instance : Coe String Template.Params.Val where
-  coe str := ⟨.mk str, #[.mk <| Html.text true str]⟩
+  coe str := ⟨.mk str, #[.mk <| Html.text str]⟩
 
 instance : Coe Html Template.Params.Val where
   coe
-   | .text true str => ↑str
+   | .text str => ↑str
    | other => ⟨.mk other, #[]⟩
 
 
@@ -163,7 +164,7 @@ def blockHtml (g : Genre)
   | .htmlDetails classes summary, contents => do
     pure {{ <details class={{classes}}><summary>{{summary}}</summary> {{← contents.mapM goB}}</details>}}
   | .htmlWrapper name attrs, contents => do
-    Html.tag name attrs <$> contents.mapM goB
+    Html.element name attrs <$> contents.mapM goB
   | .htmlDiv classes, contents => do
     pure {{ <div class={{classes}}> {{← contents.mapM goB}} </div> }}
   | .blob html, _ => pure html
@@ -194,7 +195,7 @@ def blockHtml (g : Genre)
       let contents := contents.extract 1
       return {{
         <section>
-          {{ .tag s!"h{lvl + 1}" #[] (← first.mapM goI) }}
+          {{ .element s!"h{lvl + 1}" #[] (← first.mapM goI) }}
           {{ ← contents.mapM goB }}
         </section>
       }}
@@ -353,9 +354,9 @@ def builtinHeader : TemplateM Html := do
   -- These should come first so later stylesheets can easily override them.
   out := out ++ {{<style>{{«verso-vars.css»}}</style>}}
   for style in (← read).builtInStyles do
-    out := out ++ {{<style>"\n"{{.text false style}}"\n"</style>"\n"}}
+    out := out ++ {{<style>"\n"{{.raw style}}"\n"</style>"\n"}}
   for script in (← read).builtInScripts do
-    out := out ++ {{<script>"\n"{{.text false script}}"\n"</script>"\n"}}
+    out := out ++ {{<script>"\n"{{.raw script}}"\n"</script>"\n"}}
   for js in (← read).jsFiles do
     out := out ++ {{<script src=s!"-verso-data/{js}"></script>}}
   for css in (← read).cssFiles do
@@ -368,9 +369,9 @@ def builtinHeader : TemplateM Html := do
 
   -- Components
   for style in (← get).headerCss do
-    out := out ++ {{<style>"\n"{{.text false style}}"\n"</style>"\n"}}
+    out := out ++ {{<style>"\n"{{.raw style}}"\n"</style>"\n"}}
   for script in (← get).headerJs do
-    out := out ++ {{<script>"\n"{{.text false script}}"\n"</script>"\n"}}
+    out := out ++ {{<script>"\n"{{.raw script}}"\n"</script>"\n"}}
   pure out
 
 
diff --git a/verso/src/verso-blog/VersoBlog/Theme.lean b/verso/src/verso-blog/VersoBlog/Theme.lean
index c99c7ffc4..6f433fe59 100644
--- a/verso/src/verso-blog/VersoBlog/Theme.lean
+++ b/verso/src/verso-blog/VersoBlog/Theme.lean
@@ -11,6 +11,7 @@ public section
 
 open Verso.Genre.Blog Template
 open Verso Doc Output Html
+open Lean (Html)
 
 namespace Verso.Genre.Blog
 
@@ -307,7 +308,7 @@ def post : Template := do
        | some md => {{
         <div class="metadata">
           <div class="authors">
-            {{(md : Post.PartMetadata).authors.map ({{<span class="author">{{Html.text true ·}}</span>}}) |>.toArray}}
+            {{(md : Post.PartMetadata).authors.map ({{<span class="author">{{Html.text ·}}</span>}}) |>.toArray}}
           </div>
           <div class="date">
             {{md.date.toIso8601String}}
@@ -352,7 +353,7 @@ def archiveEntry : Template := do
          | some md => {{
           <div class="metadata">
             <div class="authors">
-              {{(md : Post.PartMetadata).authors.map ({{<span class="author">{{Html.text true ·}}</span>}}) |>.toArray}}
+              {{(md : Post.PartMetadata).authors.map ({{<span class="author">{{Html.text ·}}</span>}}) |>.toArray}}
             </div>
             <div class="date">
               {{md.date.toIso8601String}}
diff --git a/verso/src/verso-html/VersoHtmlMain.lean b/verso/src/verso-html/VersoHtmlMain.lean
index 568082fdc..18f89ab6b 100644
--- a/verso/src/verso-html/VersoHtmlMain.lean
+++ b/verso/src/verso-html/VersoHtmlMain.lean
@@ -44,8 +44,8 @@ private def headContents : Html := {{
 
   <script src="popper.js"></script>
   <script src="tippy.js"></script>
-  <script>{{Html.text false highlightingJs}}</script>
-  <style>{{Html.text false highlightingStyle}}</style>
+  <script>{{Html.raw highlightingJs}}</script>
+  <style>{{Html.raw highlightingStyle}}</style>
   <link rel="stylesheet" href="verso-vars.css"/>
   <link rel="stylesheet" href="tippy-border.css"/>
   <link rel="stylesheet" href="code.css"/>
@@ -95,7 +95,7 @@ def emitMod (root : Dir) (outDir: System.FilePath) (mod : LitMod) : EmitM Unit :
 
   IO.FS.createDirAll outFile
 
-  IO.FS.writeFile (outFile / "index.html") <| "<!DOCTYPE html>\n" ++ contents.asString
+  IO.FS.writeFile (outFile / "index.html") <| "<!DOCTYPE html>\n" ++ contents.render
 
 def emitDir (outDir : System.FilePath) (dir : Dir) : EmitM Unit := do
   let root := dir
@@ -141,7 +141,7 @@ def emitSearchResultsPage (outDir : System.FilePath) : IO Unit := do
     </html>
   }}
   IO.FS.createDirAll (outDir / "search")
-  IO.FS.writeFile (outDir / "search" / "index.html") <| "<!DOCTYPE html>\n" ++ pageHtml.asString
+  IO.FS.writeFile (outDir / "search" / "index.html") <| "<!DOCTYPE html>\n" ++ pageHtml.render
 
 def main (args : List String) : IO UInt32 := do
   let config ←
diff --git a/verso/src/verso-literate-code/VersoLiterateCode.lean b/verso/src/verso-literate-code/VersoLiterateCode.lean
index 969acb144..6bb217212 100644
--- a/verso/src/verso-literate-code/VersoLiterateCode.lean
+++ b/verso/src/verso-literate-code/VersoLiterateCode.lean
@@ -148,7 +148,7 @@ partial def md2Html (md : MD4Lean.Document) (trackHeadings : Bool := false)
         let hId := toString slug
         let titleHtml := texts title
         hdgs := hdgs.push { level := n, title := titleHtml, htmlId := hId }
-        out := out ++ .tag s!"h{n + 1}" #[("id", hId)] titleHtml
+        out := out ++ .element s!"h{n + 1}" #[("id", hId)] titleHtml
       else
         out := out ++ block (.header n title)
     | b => out := out ++ block b
@@ -167,10 +167,10 @@ where
         </tbody>
       </table>
     }}
-  | .header n title => .tag s!"h{n + 1}" #[] <| texts title
+  | .header n title => .element s!"h{n + 1}" #[] <| texts title
   | .blockquote bs => {{<blockquote>{{blocks bs}}</blockquote>}}
   | .hr => {{<hr/>}}
-  | .html xs => .text false (String.join xs.toList)
+  | .html xs => .raw (String.join xs.toList)
   | .code _ _ _ ss => {{<pre><code>{{String.join ss.toList}}</code></pre>}}
 
   blocks : Array MD4Lean.Block → Html
@@ -196,7 +196,7 @@ where
   | .img src title alt => {{<img src={{attr src}} title={{attr title}} alt={{String.join <| Array.toList <| alt.filterMap fun | .normal s => some s | _ => none}}/>}}
   | .u xs => texts xs -- TODO
   | .wikiLink _target txt => texts txt -- TODO
-  | .entity x => .text false x
+  | .entity x => .raw x
   | .latexMath _x => .empty -- TODO
   | .latexMathDisplay _x => .empty -- TODO
 
diff --git a/verso/src/verso-literate-html/LiterateHtmlMain.lean b/verso/src/verso-literate-html/LiterateHtmlMain.lean
index 5623de1cb..98769cec4 100644
--- a/verso/src/verso-literate-html/LiterateHtmlMain.lean
+++ b/verso/src/verso-literate-html/LiterateHtmlMain.lean
@@ -194,8 +194,8 @@ private def mkHeadContents (litConfig : LiterateConfig) (includeCodeAssets : Boo
     <script src="popper.js"></script>
     <script src="tippy.js"></script>
     <script src="marked.js"></script>
-    <script>{{Html.text false highlightingJs}}</script>
-    <style>{{Html.text false highlightingStyle}}</style>
+    <script>{{Html.raw highlightingJs}}</script>
+    <style>{{Html.raw highlightingStyle}}</style>
     <link rel="stylesheet" href="tippy-border.css"/>
   }} else .empty
   let copyButtonTag : Html := if includeCodeAssets then {{
@@ -362,7 +362,7 @@ def emitMod (root : Dir) (outDir: System.FilePath) (mod : LitMod)
 
   IO.FS.createDirAll outFile
 
-  IO.FS.writeFile (outFile / "index.html") <| "<!DOCTYPE html>\n" ++ pageHtml.asString
+  IO.FS.writeFile (outFile / "index.html") <| "<!DOCTYPE html>\n" ++ pageHtml.render
 
 def emitDir (outDir : System.FilePath) (dir : Dir)
     (srcDirs : Lean.NameMap System.FilePath := {}) : EmitM Unit := do
@@ -399,7 +399,7 @@ partial def emitLandingPage (outDir : System.FilePath) (dir : Dir) (litConfig :
       </body>
     </html>
   }}
-  IO.FS.writeFile (outDir / "index.html") <| "<!DOCTYPE html>\n" ++ pageContents.asString
+  IO.FS.writeFile (outDir / "index.html") <| "<!DOCTYPE html>\n" ++ pageContents.render
 where
   buildToc (dir : Dir) : Html :=
     if dir.children.isEmpty then .empty
@@ -449,7 +449,7 @@ def emitSearchResultsPage (outDir : System.FilePath) (litConfig : LiterateConfig
     </html>
   }}
   IO.FS.createDirAll (outDir / "search")
-  IO.FS.writeFile (outDir / "search" / "index.html") <| "<!DOCTYPE html>\n" ++ pageContents.asString
+  IO.FS.writeFile (outDir / "search" / "index.html") <| "<!DOCTYPE html>\n" ++ pageContents.render
 
 open Verso Output Doc Html in
 /--
@@ -479,7 +479,7 @@ def emitLandingFromModule (outDir : System.FilePath) (root : Dir) (modName : Nam
     | some siteTitle => s!"{modLabel} — {siteTitle}"
     | none => modLabel
   let pageHtml := page landingPageTitle siteRoot headContents mod.name root htmlId? body (pageToc := tocHtml) (litConfig := litConfig)
-  IO.FS.writeFile (outDir / "index.html") <| "<!DOCTYPE html>\n" ++ pageHtml.asString
+  IO.FS.writeFile (outDir / "index.html") <| "<!DOCTYPE html>\n" ++ pageHtml.render
   return hlState
 
 def main (args : List String) : IO UInt32 := do
diff --git a/verso/src/verso-manual/VersoManual.lean b/verso/src/verso-manual/VersoManual.lean
index 1b82da561..0b3ac7598 100644
--- a/verso/src/verso-manual/VersoManual.lean
+++ b/verso/src/verso-manual/VersoManual.lean
@@ -455,7 +455,8 @@ def emitTeX (config : Config) (text : Part Manual) : EmitM Unit := do
   for (f, content) in extra.extraFiles do
     IO.FS.writeFile (dir / f) content
 
-open Verso.Output (Html)
+open Verso.Output
+open Lean (Html)
 
 instance [Monad m] : Inhabited (StateT (State Html) m Html.Toc) := ⟨pure default⟩
 
@@ -494,7 +495,7 @@ partial def toc [Monad m] [Html.ToHtml Manual m (Doc.Inline Manual)] [MonadLiftT
     let children ← sub.mapM (fun p => toc depth' opts (ctxt'.inPart p) state definitionIds linkTargets p)
     pure {
       title := titleHtml,
-      shortTitle := meta.bind (·.shortTitle) |>.map Html.ofString,
+      shortTitle := meta.bind (·.shortTitle) |>.map Html.text,
       path := ctxt'.path,
       id := v.toString,
       sectionNum := ctxt.sectionNumber.mapM _root_.id,
@@ -577,7 +578,7 @@ def emitFindHtml (toc : List Html.Toc) (dir : System.FilePath) (state : Traverse
   emitXrefsJson dir state
   ensureDir (dir / "find")
   IO.FS.writeFile (dir / "find" / "index.html")
-    (Html.doctype ++ (Hoist.postprocess <| relativizeLinks <| xref toc xrefJson find.js state config).asString)
+    (Html.doctype ++ (Hoist.postprocess <| relativizeLinks <| xref toc xrefJson find.js state config).render)
 
 open Output.Html in
 /--
@@ -612,7 +613,7 @@ def emitSearchResultsHtml
   ensureDir (dir / "search")
   IO.FS.writeFile
     (dir / "search" / "index.html")
-    (Html.doctype ++ (Hoist.postprocess <| relativizeLinks <| searchResultsPage toc bookTitle state config).asString)
+    (Html.doctype ++ (Hoist.postprocess <| relativizeLinks <| searchResultsPage toc bookTitle state config).render)
 
 
 section
@@ -820,7 +821,7 @@ where
       if config.verbose then
         IO.println s!"Saving {dir.join "index.html"}"
       h.putStrLn Html.doctype
-      h.putStrLn <| Html.asString <| Hoist.postprocess <| relativizeLinks <|
+      h.putStrLn <| Html.render <| Hoist.postprocess <| relativizeLinks <|
         page toc ctxt.path text.titleString titleToShow pageContent state config.toConfig thisPageToc (showNavButtons := false)
 
 
@@ -941,7 +942,7 @@ where
       if config.verbose then
         IO.println s!"Saving {dir.join "index.html"}"
       h.putStrLn Html.doctype
-      h.putStrLn <| Html.asString <| Hoist.postprocess <| relativizeLinks <|
+      h.putStrLn <| Html.render <| Hoist.postprocess <| relativizeLinks <|
         page bookContents ctxt.path part.titleString bookTitle pageContent state config.toConfig thisPageToc
     if depth > 0 ∧ part.htmlSplit != .never then
       for p in part.subParts do
diff --git a/verso/src/verso-manual/VersoManual/Basic.lean b/verso/src/verso-manual/VersoManual/Basic.lean
index deb3798a8..14f09e3e3 100644
--- a/verso/src/verso-manual/VersoManual/Basic.lean
+++ b/verso/src/verso-manual/VersoManual/Basic.lean
@@ -29,7 +29,7 @@ set_option doc.verso true
 
 public section
 
-open Lean (Name Json NameMap ToJson FromJson)
+open Lean (Name Json NameMap ToJson FromJson Html)
 open Std (HashSet HashMap TreeSet)
 open Verso.Doc
 open Verso.Multi
@@ -238,7 +238,7 @@ structure PartMetadata where
   file : Option String := none
   /-- The internal unique ID, which is automatically assigned during traversal. -/
   id : Option InternalId := none
-  /-- Should this section be numbered? If {name}`false`, then it's like `\section*` in LaTeX -/
+  /-- Should this section be numbered? If {name}`false`, then it's like {lit}`\section*` in LaTeX -/
   number : Bool := true
   /-- If {name}`true`, the part is only rendered in draft mode. -/
   draft : Bool := false
@@ -341,7 +341,7 @@ structure TraverseState extends HtmlAssets where
   ids : TreeSet InternalId := {}
   quickJump : DomainMappers := {}
   /--
-  TeX `\usepackage{…}` lines contributed by block and inline extensions whose blocks actually
+  TeX {lit}`\usepackage{…}` lines contributed by block and inline extensions whose blocks actually
   occur in the document. Populated during traversal at each block/inline occurrence so unused
   extensions don't pollute the preamble.
   -/
@@ -496,10 +496,10 @@ def getDomainObject? (state : TraverseState) (domain : Name) (canonicalName : St
   state.domains.get? domain >>= fun d => d.get? canonicalName
 
 def setDomainTitle (state : TraverseState) (domain : Name) (title : String) : TraverseState :=
-  {state with domains := state.domains.insert! domain {state.domains.get? domain |>.getD {} with title := some title}}
+  {state with domains := state.domains.insert! domain {state.domains.get? domain |>.getD {} with title := some title} }
 
 def setDomainDescription (state : TraverseState) (domain : Name) (description : String) : TraverseState :=
-  {state with domains := state.domains.insert! domain {state.domains.get? domain |>.getD {} with description := some description}}
+  {state with domains := state.domains.insert! domain {state.domains.get? domain |>.getD {} with description := some description} }
 
 open Verso.Search in
 def addQuickJumpMapper (state : TraverseState) (domain : Name) (domainMapper : DomainMapper) : TraverseState :=
@@ -665,9 +665,9 @@ abbrev BlockTraversal genre :=
   ReaderT TraverseContext (StateT TraverseState (BuildLogT IO)) (Option (Doc.Block genre))
 
 abbrev BlockToHtml (genre : Genre) (m) :=
-  (Doc.Inline genre → Html.HtmlT genre m Output.Html) →
-  (Doc.Block genre → Html.HtmlT genre m Output.Html) →
-  InternalId → Json → Array (Doc.Block genre) → Html.HtmlT genre m Output.Html
+  (Doc.Inline genre → Html.HtmlT genre m Html) →
+  (Doc.Block genre → Html.HtmlT genre m Html) →
+  InternalId → Json → Array (Doc.Block genre) → Html.HtmlT genre m Html
 
 abbrev BlockToTeX (genre : Genre) (m) :=
   (Doc.Inline genre → TeX.TeXT genre m Output.TeX) →
@@ -679,8 +679,8 @@ abbrev InlineTraversal genre :=
   ReaderT TraverseContext (StateT TraverseState (BuildLogT IO)) (Option (Doc.Inline genre))
 
 abbrev InlineToHtml (genre : Genre) (m) :=
-  (Doc.Inline genre → Html.HtmlT genre m Output.Html) →
-    InternalId → Json → Array (Doc.Inline genre) → Html.HtmlT genre m Output.Html
+  (Doc.Inline genre → Html.HtmlT genre m Html) →
+    InternalId → Json → Array (Doc.Inline genre) → Html.HtmlT genre m Html
 
 abbrev InlineToTeX (genre : Genre) (m) :=
   (Doc.Inline genre → TeX.TeXT genre m Output.TeX) →
@@ -783,7 +783,7 @@ structure InlineDescr extends HtmlAssets where
 
   The empty array means that the inline should not be included.
   -/
-  localContentItem : InternalId → Json → Array (Doc.Inline Manual) → Except String (Array (String × Verso.Output.Html)) :=
+  localContentItem : InternalId → Json → Array (Doc.Inline Manual) → Except String (Array (String × Html)) :=
     fun _ _ _ => pure #[]
 
   /--
@@ -791,7 +791,7 @@ structure InlineDescr extends HtmlAssets where
   will fail.
   -/
   toTeX : Option (InlineToTeX Manual (ReaderT ExtensionImpls (BuildLogT IO)))
-  /-- Required TeX `\usepackage` lines -/
+  /-- Required TeX {lit}`\usepackage` lines -/
   usePackages : List String := {}
   /-- Required items in the TeX preamble -/
   preamble : List String := {}
@@ -827,7 +827,7 @@ structure BlockDescr extends HtmlAssets where
 
   The empty array means that the block should not be included.
   -/
-  localContentItem : InternalId → Json → Array (Doc.Block Manual) → Except String (Array (String × Verso.Output.Html)) :=
+  localContentItem : InternalId → Json → Array (Doc.Block Manual) → Except String (Array (String × Html)) :=
     fun _ _ _ => pure #[]
 
   /--
@@ -835,7 +835,7 @@ structure BlockDescr extends HtmlAssets where
   will fail.
   -/
   toTeX : Option (BlockToTeX Manual (ReaderT ExtensionImpls (BuildLogT IO)))
-  /-- Required TeX `\usepackage` lines -/
+  /-- Required TeX {lit}`\usepackage` lines -/
   usePackages : List String := {}
   /-- Required items in the TeX preamble -/
   preamble : List String := {}
@@ -1575,7 +1575,7 @@ def sectionHtml (ctxt : TraverseContext) : Html :=
   match sectionString ctxt with
   | none => .empty
    -- Non-breaking space because section numbers shouldn't end up on a line alone
-  | some s => .text true (s ++ " ")
+  | some s => .text (s ++ " ")
 
 open Html in
 /--
@@ -1618,7 +1618,7 @@ instance : Html.GenreHtml Manual (ReaderT AllRemotes (ReaderT ExtensionImpls (Bu
       if let some id := m.id then permalink id st
       else .empty
     let mkHeader lvl content :=
-      .tag s!"h{lvl}" attrs (sectionNumber ++ content ++ permalink? «meta»)
+      .element s!"h{lvl}" attrs (sectionNumber ++ content ++ permalink? «meta»)
     go txt mkHeader
 
   block goI goB b content := do
diff --git a/verso/src/verso-manual/VersoManual/Diagrams.lean b/verso/src/verso-manual/VersoManual/Diagrams.lean
index b1c42672d..e18be8a0a 100644
--- a/verso/src/verso-manual/VersoManual/Diagrams.lean
+++ b/verso/src/verso-manual/VersoManual/Diagrams.lean
@@ -16,7 +16,7 @@ public section
 
 open Lean Elab
 open Verso ArgParse Doc Elab Genre.Manual Html
-open Verso.Output (Html)
+open Verso.Output
 open Verso.Doc.Html (HtmlT)
 open Verso.Illuminate (elabAndStoreDiagram)
 open Verso.Genre.Manual.InlineLean.Scopes (runWithOpenDecls runWithVariables)
@@ -98,7 +98,7 @@ block_extension Block.diagram
           (if isInline then ["display: inline-block"] else [])
       pure {{
         <div class="diagram" style={{style}}>
-          {{Html.text false svgStr}}
+          {{Html.raw svgStr}}
         </div>
       }}
   usePackages := ["\\usepackage{svg}"]
diff --git a/verso/src/verso-manual/VersoManual/Docstring.lean b/verso/src/verso-manual/VersoManual/Docstring.lean
index 99c98a538..ea407949e 100644
--- a/verso/src/verso-manual/VersoManual/Docstring.lean
+++ b/verso/src/verso-manual/VersoManual/Docstring.lean
@@ -1626,7 +1626,7 @@ def optionDocs.descr : BlockDescr := withHighlighting {
     open Verso.Output Html in do
       let .ok (name, defaultValue) := FromJson.fromJson? (α := Name × Highlighted) info
         | do reportError "Failed to deserialize docstring data while generating HTML for an option"; pure .empty
-      let x : Html := Html.text true <| Name.toString name
+      let x : Html := Html.text <| Name.toString name
 
       return namedocsBox id (← HtmlT.state) "option" x {{
         <p>"Default value: " <code class="hl lean inline">{{← defaultValue.toHtml (g := Manual)}}</code></p>
diff --git a/verso/src/verso-manual/VersoManual/Glossary.lean b/verso/src/verso-manual/VersoManual/Glossary.lean
index ec064c9cd..017752797 100644
--- a/verso/src/verso-manual/VersoManual/Glossary.lean
+++ b/verso/src/verso-manual/VersoManual/Glossary.lean
@@ -18,7 +18,7 @@ public import Verso.Doc.Elab.Monad
 open Verso Genre Manual ArgParse
 open Verso.Doc.Elab
 open Verso.Multi (AllRemotes)
-open Lean (Json ToJson FromJson)
+open Lean (Json ToJson FromJson Html)
 
 namespace Verso.Genre.Manual
 
diff --git a/verso/src/verso-manual/VersoManual/Html.lean b/verso/src/verso-manual/VersoManual/Html.lean
index 83653a484..894240e28 100644
--- a/verso/src/verso-manual/VersoManual/Html.lean
+++ b/verso/src/verso-manual/VersoManual/Html.lean
@@ -17,6 +17,7 @@ import VersoManual.Html.Style
 namespace Verso.Genre.Manual.Html
 open Std (HashSet)
 open Verso.Output Html Multi
+open Lean (Html)
 
 public structure Toc.Meta where
   title : Html
@@ -265,9 +266,9 @@ where
   safeTags := ["code", "span", "a"]
 
   getHtmlTitle : Html → Option String
-  | .text _e s => some s
+  | .text s | .raw s => some s
   | .seq es => (String.join ∘ (·.toList)) <$> es.mapM getHtmlTitle
-  | .tag t _ e =>
+  | .element t _ e =>
     if t ∈ safeTags then
       getHtmlTitle e
     else none
@@ -374,7 +375,7 @@ where
 
   linkify (path : Path) (id : Option String) (html : Html) :=
     match html with
-    | .tag "a" _ _ => html
+    | .element "a" _ _ => html
     | other => {{<a href={{path.link id}}>{{other}}</a>}}
   sectionNum num :=
       match num with
@@ -458,8 +459,8 @@ public def page
         <script src="toc-resize.js" defer="defer"></script>
         {{extraJsFiles.map fun f => ({{<script src=s!"{f.1}" {{if f.2 then defer else #[]}}></script>}})}}
         {{extraStylesheets.map (fun url => {{<link rel="stylesheet" href={{url}}/> }})}}
-        {{extraCss.toArray.map ({{<style>{{Html.text false ·.css}}</style>}})}}
-        {{extraJs.toArray.map ({{<script>{{Html.text false ·.js}}</script>}})}}
+        {{extraCss.toArray.map ({{<style>{{Html.raw ·.css}}</style>}})}}
+        {{extraJs.toArray.map ({{<script>{{Html.raw ·.js}}</script>}})}}
         {{extraHead}}
       </head>
       <body>
@@ -520,7 +521,8 @@ public def page
 
 
 public def relativize (path : Path) (html : Html) : Html :=
-  html.visitM (m := ReaderT Path Id) (tag := rwTag) |>.run path
+  html.rewritePostM (m := ReaderT Path Id)
+    (fun | .element t a c => rwTag t a c | h => return h) |>.run path
 where
   urlAttr (name : String) : Bool := name ∈ ["href", "src", "data", "poster"]
   rwAttr (attr : String × String) : ReaderT Path Id (String × String) := do
@@ -531,9 +533,9 @@ where
       }
     else
       pure attr
-  rwTag (tag : String) (attrs : Array (String × String)) (content : Html) : ReaderT Path Id (Option Html) := do
-    if tag == "base" then return none
+  rwTag (tag : String) (attrs : Array (String × String)) (content : Html) : ReaderT Path Id Html := do
+    if tag == "base" then return .element tag attrs content
     -- Don't rewrite URLs that come from remote content. This attribute is inserted by the `ref`
     -- role when referring to remote content.
-    if attrs.any (·.1 == "data-verso-remote") then return none
-    return some <| .tag tag (← attrs.mapM rwAttr) content
+    if attrs.any (·.1 == "data-verso-remote") then return .element tag attrs content
+    return .element tag (← attrs.mapM rwAttr) content
diff --git a/verso/src/verso-manual/VersoManual/Html/Config.lean b/verso/src/verso-manual/VersoManual/Html/Config.lean
index 128d83014..bef139280 100644
--- a/verso/src/verso-manual/VersoManual/Html/Config.lean
+++ b/verso/src/verso-manual/VersoManual/Html/Config.lean
@@ -5,7 +5,7 @@ Author: David Thrane Christiansen
 -/
 
 module
-public import Verso.Output.Html
+public import Lean.Data.Html
 import Verso.BEq
 public import Lean.Data.Json.FromToJson
 import VersoUtil.BinFiles.Z85
@@ -20,9 +20,9 @@ public structure HtmlConfig extends HtmlAssets where
   htmlDepth := 2
   extraFilesHtml : List (System.FilePath × String) := []
   /-- Extra elements to add to every page's `head` tag -/
-  extraHead : Array Output.Html := #[]
+  extraHead : Array Html := #[]
   /-- Extra elements to add to every page's contents -/
-  extraContents : Array Output.Html := #[]
+  extraContents : Array Html := #[]
   /-- The URL from which to draw the logo to show, if any -/
   logo : Option String := none
   /-- The URL that the logo should link to, if any (default is site root) -/
diff --git a/verso/src/verso-manual/VersoManual/Html/Hoist.lean b/verso/src/verso-manual/VersoManual/Html/Hoist.lean
index ac46e8cf0..17007883c 100644
--- a/verso/src/verso-manual/VersoManual/Html/Hoist.lean
+++ b/verso/src/verso-manual/VersoManual/Html/Hoist.lean
@@ -66,16 +66,16 @@ is passed to {name}`f`.
 def mapRootTags
     (f : (name : String) → (attrs : Array (String × String)) → (contents : Output.Html) → Output.Html) :
     Output.Html → Output.Html
-  | .tag name attrs contents => f name attrs contents
+  | .element name attrs contents => f name attrs contents
   | .seq contents => .seq (contents.map (mapRootTags f))
-  | html@(.text ..) => f "span" #[(generatedWrapperAttr, "")] html
+  | html@(.text _) | html@(.raw _) => f "span" #[(generatedWrapperAttr, "")] html
 
 def addTokenAttribute (attr kind : String) : Output.Html → Output.Html :=
   mapRootTags fun name attrs contents =>
     let old := attrTokens attr attrs
     let kinds := if kind ∈ old then old else old.push kind
     let value := String.intercalate " " kinds.toList
-    .tag name (attrs.filter (·.1 != attr) |>.push (attr, value)) contents
+    .element name (attrs.filter (·.1 != attr) |>.push (attr, value)) contents
 
 /--
 Marks the root HTML nodes as auxiliary content that should be moved outside an enclosing barrier
@@ -141,10 +141,10 @@ def effectiveBarriers
 
 partial def rewrite (html : Output.Html) : ReaderT (RewriteContext σ) (ST σ) Output.Html := do
   match html with
-  | .text .. => pure html
+  | .text _ | .raw _ => pure html
   | .seq contents =>
     return .seq (← contents.mapM rewrite)
-  | .tag name attrs contents =>
+  | .element name attrs contents =>
     let context ← read
     let hoistKinds := attrTokens hoistAttr attrs
     let suppressibleKinds := attrTokens suppressibleAttr attrs
@@ -162,9 +162,9 @@ where
   markHoisted (direction : Direction) : Output.Html → Output.Html :=
     mapRootTags fun name attrs contents =>
       if attrs.any fun (attr, _) => attr == generatedWrapperAttr || attr == hoistedAttr then
-        .tag name attrs contents
+        .element name attrs contents
       else
-        .tag name (attrs.push (hoistedAttr, direction.attrValue)) contents
+        .element name (attrs.push (hoistedAttr, direction.attrValue)) contents
   rewriteTag (name : String) (attrs : Array (String × String)) (contents : Output.Html) := do
     let context ← read
     let suppressed := attrTokens suppressAttr attrs
@@ -185,7 +185,7 @@ where
         }
         pure (some (beforeDestination, afterDestination))
     let contents' ← withReader (fun _ => innerContext) (rewrite contents)
-    let out := Output.Html.tag name attrs contents'
+    let out := .element name attrs contents'
     let some (beforeDestination, afterDestination) := destinations? | return out
     let before ← beforeDestination.get
     let after ← afterDestination.get
@@ -193,13 +193,15 @@ where
     return .seq (before ++ #[out] ++ after)
 
 def cleanup (html : Output.Html) : Output.Html :=
-  html.visitM (m := Id) (tag := fun name attrs contents => do
-    let generatedWrapper := attrs.any (·.1 == generatedWrapperAttr)
-    let attrs := attrs.filter fun (attr, _) => attr ∉ rewriteAttributes
-    if name == "span" && generatedWrapper && attrs.isEmpty then
-      pure (some contents)
-    else
-      pure (some (.tag name attrs contents)))
+  html.rewritePost fun
+    | .element name attrs contents =>
+      let generatedWrapper := attrs.any (·.1 == generatedWrapperAttr)
+      let attrs := attrs.filter fun (attr, _) => attr ∉ rewriteAttributes
+      if name == "span" && generatedWrapper && attrs.isEmpty then
+        contents
+      else
+        .element name attrs contents
+    | h => h
 
 /--
 Rewrites HTML to hoist content into a context where it can be used. This is used to lift marginal
diff --git a/verso/src/verso-manual/VersoManual/Html/SoftHyphenate.lean b/verso/src/verso-manual/VersoManual/Html/SoftHyphenate.lean
index 3cd526847..b0d3686c2 100644
--- a/verso/src/verso-manual/VersoManual/Html/SoftHyphenate.lean
+++ b/verso/src/verso-manual/VersoManual/Html/SoftHyphenate.lean
@@ -12,11 +12,12 @@ set_option doc.verso true
 namespace Verso.Genre.Manual
 
 open Verso.Output Html
+open Lean (Html)
 
 private def addShy (xs : Array Html) : Array Html :=
   if xs.isEmpty then xs
-  else if let some (Verso.Output.Html.tag "wbr" ..) := xs.back? then xs
-  else  xs.push (.text false "&shy;")
+  else if let some (.element "wbr" ..) := xs.back? then xs
+  else  xs.push (.raw "&shy;")
 
 /--
 Adds soft hyphenation opportunities ({lit}`<wbr>` or {lit}`&shy;`) to a single text node, allowing
@@ -36,7 +37,7 @@ public def softHyphenateText (esc : Bool) (str : String) : Html := Id.run do
     let current := iter.get h
     let iter' := iter.next h
     if prior == some '.' && current != '.' then
-      strs := strs.push (.text esc <| str.extract start iter)
+      strs := strs.push (.ofString esc <| str.extract start iter)
       -- Break lines after dots without hyphens
       strs := strs.push {{<wbr/>}}
       start := iter
@@ -45,7 +46,7 @@ public def softHyphenateText (esc : Bool) (str : String) : Html := Id.run do
         if !strs.isEmpty then
           strs := addShy strs
         -- Break lines at case changes with hyphens
-        strs := strs.push (.text esc <| str.extract start iter)
+        strs := strs.push (.ofString esc <| str.extract start iter)
         start := iter
 
     prior := some current
@@ -53,7 +54,7 @@ public def softHyphenateText (esc : Bool) (str : String) : Html := Id.run do
 
   if start != iter then
     strs := addShy strs
-    strs := strs.push (.text esc <| str.extract start iter)
+    strs := strs.push (.ofString esc <| str.extract start iter)
 
   if h : strs.size = 1 then strs[0] else .seq strs
 
@@ -65,9 +66,10 @@ HTML, allowing browsers to break the word at that point. Line break opportunitie
 {lit}`Verso.<wbr>Genre.<wbr>Manual.<wbr>soft&shy;Hyphenate&shy;Identifiers`.
 -/
 public def softHyphenateTextNodes (html : Html) : Html :=
-  html.visitM (m := Id) (text := rwText)
-where
-  rwText esc str := pure (some (softHyphenateText esc str))
+  html.rewritePost fun
+    | .text s => softHyphenateText true s
+    | .raw s => softHyphenateText false s
+    | h => h
 
 /--
 Adds soft hyphenation opportunities ({lit}`<wbr>` or {lit}`&shy;`) to identifiers in HTML, allowing
@@ -79,8 +81,6 @@ hyphenation opportunities on transitions from lower-case to upper-case letters,
 Here, “identifiers” refers to text nodes found within `<code>` tags.
 -/
 public partial def softHyphenateIdentifiers (html : Html) : Html :=
-  html.visitM (m := Id) (tag := rwTag)
-where
-  rwTag
-    | "code", attrs, content => pure (some (.tag "code" attrs (softHyphenateTextNodes content)))
-    | _, _, _ => pure none
+  html.rewritePost fun
+    | .element "code" attrs content => .element "code" attrs (softHyphenateTextNodes content)
+    | h => h
diff --git a/verso/src/verso-manual/VersoManual/Index.lean b/verso/src/verso-manual/VersoManual/Index.lean
index e0e2b7dbc..0087b2a5a 100644
--- a/verso/src/verso-manual/VersoManual/Index.lean
+++ b/verso/src/verso-manual/VersoManual/Index.lean
@@ -20,7 +20,7 @@ open Verso Genre Manual
 open Verso.Multi
 open Verso.Doc.Elab
 open Verso.ArgParse
-open Lean (ToJson FromJson quote)
+open Lean (ToJson FromJson quote Html)
 open Std (HashMap HashSet)
 
 namespace Verso.Genre.Manual.Index
@@ -324,7 +324,7 @@ instance : Hashable IndexCat where
     | .letter c => mixHash 7 (hash c.toNat)
 
 open Output.Html in
-def IndexCat.header : IndexCat → Output.Html
+def IndexCat.header : IndexCat → Html
   | .symbolic => "Symbols"
   | .digit => "0–9"
   | .letter c => c.toUpper.toString
@@ -447,7 +447,7 @@ def theIndex.descr : BlockDescr where
         let r := v.render
         let out ← r.mapM fun (cat, entries) => do
           let h := (← read).1.headerLevel + 1
-          let hdr := Output.Html.tag s!"h{h}" #[("id", s!"---index-hdr-{cat.id}")] (cat.header)
+          let hdr := Html.element s!"h{h}" #[("id", s!"---index-hdr-{cat.id}")] (cat.header)
           let entries' ← entries.mapM fun e => do
             return softHyphenateIdentifiers {{<li>{{← e.toHtml goI}}</li>}}
           return {{<div class="division">{{hdr ++ {{<ol>{{entries'}}</ol>}} }}</div>}}
diff --git a/verso/src/verso-manual/VersoManual/License.lean b/verso/src/verso-manual/VersoManual/License.lean
index 41460ad56..5d8f6e89d 100644
--- a/verso/src/verso-manual/VersoManual/License.lean
+++ b/verso/src/verso-manual/VersoManual/License.lean
@@ -15,7 +15,7 @@ import VersoManual.Basic
 
 
 
-open Lean (ToJson FromJson)
+open Lean (ToJson FromJson Html)
 
 open Verso ArgParse Doc Elab
 
@@ -45,7 +45,7 @@ private def paragraphedHtml (text : String) : Html :=
 def LicenseInfo.toHtml (license : LicenseInfo) (headerLevel : Nat) : Html :=
   let {identifier, dependency, howUsed, link, text} := license
   {{<section class="license-info">
-      {{.tag s!"h{headerLevel}" #[] dependency }}
+      {{.element s!"h{headerLevel}" #[] dependency }}
       {{link.map (fun url => {{<a class="link" href={{url}}>{{url}}</a>}}) |>.getD .empty}}
       {{howUsed.map paragraphedHtml |>.getD .empty}}
       <code class="spdx">{{identifier}}</code>
@@ -56,7 +56,7 @@ where
     | (hdr?, txt) =>
       let hdrHtml :=
         if let some hdr := hdr? then
-          Html.tag s!"h{headerLevel+1}" #[] hdr
+          Html.element s!"h{headerLevel+1}" #[] hdr
         else
           .empty
       {{<section>{{hdrHtml}}{{paragraphedHtml txt}}</section>}}
diff --git a/verso/src/verso-manual/VersoManual/Literate.lean b/verso/src/verso-manual/VersoManual/Literate.lean
index b8dc47a2d..78ef9b79a 100644
--- a/verso/src/verso-manual/VersoManual/Literate.lean
+++ b/verso/src/verso-manual/VersoManual/Literate.lean
@@ -48,7 +48,7 @@ block_extension Block.literateDocstringPart (level : Nat) where
     let contents := contents.extract 1
     pure {{
       <section>
-        {{.tag s!"h{level + 1}" #[] title}}
+        {{.element s!"h{level + 1}" #[] title}}
         {{← contents.mapM goB}}
       </section>
     }}
diff --git a/verso/src/verso-manual/VersoManual/LocalContents.lean b/verso/src/verso-manual/VersoManual/LocalContents.lean
index 23c84aefa..c03eba684 100644
--- a/verso/src/verso-manual/VersoManual/LocalContents.lean
+++ b/verso/src/verso-manual/VersoManual/LocalContents.lean
@@ -236,7 +236,7 @@ partial def localContentsCore [Monad m] [MonadLiftT IO m] [ToHtml Manual m (Doc.
     let shortTitle := p.metadata.bind (·.shortTitle)
     let titleHtml ←
       if let some title := shortTitle then
-        pure (Html.ofString title)
+        pure (Html.text title)
       else
         let (html, _) ← p.title.mapM (Manual.toHtml (m := m) opts ctxt xref {} {} {} ·) |>.run {}
         pure html
diff --git a/verso/src/verso-manual/VersoManual/Row.lean b/verso/src/verso-manual/VersoManual/Row.lean
index b46a38f75..175c7db28 100644
--- a/verso/src/verso-manual/VersoManual/Row.lean
+++ b/verso/src/verso-manual/VersoManual/Row.lean
@@ -15,7 +15,7 @@ public section
 open Lean Elab
 open Verso ArgParse Doc Elab Genre.Manual Html
 open Verso.Doc.Html (HtmlT)
-open Verso.Output (Html)
+open Verso.Output
 
 namespace Verso.Genre.Manual
 
diff --git a/verso/src/verso-manual/VersoManual/Table.lean b/verso/src/verso-manual/VersoManual/Table.lean
index 97d304afd..185b5de2b 100644
--- a/verso/src/verso-manual/VersoManual/Table.lean
+++ b/verso/src/verso-manual/VersoManual/Table.lean
@@ -117,8 +117,8 @@ block_extension Block.table (columns : Nat) (header : Bool) (tag : Option String
         return {{
           <table class={{«class»}} {{attrs}}>
             {{← rows.mapIdxM fun i r => do
-              let cols ← Output.Html.seq <$> r.mapM fun c => do
-                let cell : Output.Html ← c.mapM goB
+              let cols ← Html.seq <$> r.mapM fun c => do
+                let cell : Html ← c.mapM goB
                 if header && i == 0 then
                   pure {{<th>{{cell}}</th>}}
                 else
diff --git a/verso/src/verso-search/VersoSearch/DomainSearch.lean b/verso/src/verso-search/VersoSearch/DomainSearch.lean
index e8222be8b..52a2f9565 100644
--- a/verso/src/verso-search/VersoSearch/DomainSearch.lean
+++ b/verso/src/verso-search/VersoSearch/DomainSearch.lean
@@ -284,7 +284,7 @@ by every genre at once.
 emitted search assets. It is spliced into every {lit}`src`/{lit}`href`, with a trailing
 slash added automatically if missing.
 -/
-public def searchAssetTags (searchDir : String := "-verso-search") : Verso.Output.Html :=
+public def searchAssetTags (searchDir : String := "-verso-search") : Html :=
   open Verso.Output.Html in
   let d := if searchDir.endsWith "/" then searchDir else searchDir ++ "/"
   -- Deferring the four scripts keeps them off the render-blocking path. `search-init.js` below is a
diff --git a/verso/src/verso-tutorial/VersoTutorial.lean b/verso/src/verso-tutorial/VersoTutorial.lean
index 20d13c352..5c56c8f0c 100644
--- a/verso/src/verso-tutorial/VersoTutorial.lean
+++ b/verso/src/verso-tutorial/VersoTutorial.lean
@@ -208,7 +208,7 @@ def EmitM.writeFile (path : System.FilePath) (content : String) : EmitM Unit :=
 def EmitM.writeHtmlFile (path : System.FilePath) (content : Html) : EmitM Unit := do
   if (← readThe EmitContext).config.verbose then
     IO.println s!"Writing {path}"
-  IO.FS.writeFile path <| doctype ++ "\n" ++ (Hoist.postprocess content).asString
+  IO.FS.writeFile path <| doctype ++ "\n" ++ (Hoist.postprocess content).render
 
 def LocalToC.ofPage (path : Path) (text : Part Blog.Page) : EmitM LocalToC := do
   let title := text.titleString
diff --git a/verso/src/verso/Verso/Code/Highlighted.lean b/verso/src/verso/Verso/Code/Highlighted.lean
index 14bc13852..cc75ad4f7 100644
--- a/verso/src/verso/Verso/Code/Highlighted.lean
+++ b/verso/src/verso/Verso/Code/Highlighted.lean
@@ -16,7 +16,7 @@ meta import Verso.Instances.Deriving
 
 open SubVerso.Highlighting
 open Verso.Output Html
-open Lean (Json ToJson FromJson Quote)
+open Lean (Json ToJson FromJson Quote Html)
 open Std (HashMap)
 
 namespace SubVerso.Highlighting
@@ -112,7 +112,7 @@ public def Dedup.insert (table : Dedup α) (val : α) : Nat × Dedup α :=
 public def Dedup.get? (table : Dedup α) (id : Nat) : Option α := table.contentId[id]?
 
 public def Dedup.docJson (table : Dedup Html) : Json :=
-  table.contentId.fold (init := .mkObj []) fun out id html => out.setObjVal! (toString id) (.str html.asString)
+  table.contentId.fold (init := .mkObj []) fun out id html => out.setObjVal! (toString id) (.str html.render)
 
 public structure IdSupply where
   nextId : Nat := 0
@@ -396,7 +396,7 @@ public defmethod Highlighted.trimOneTrailingNl : Highlighted → Highlighted
   | .tactics i s e hl => .tactics i s e (trimOneTrailingNl hl)
   | .span i hl => .span i (trimOneTrailingNl hl)
 
-public defmethod Highlighted.containsNewline : (t : Highlighted) → Bool
+public partial defmethod Highlighted.containsNewline : (t : Highlighted) → Bool
   | .text s => s.contains '\n'
   | .unparsed s => s.contains '\n'
   | .seq xs => xs.any containsNewline
@@ -502,11 +502,11 @@ defmethod Token.htmlContent (tok : Token) : HighlightHtmlM g Html := do
       iter := iter.next h
       str := str.push c
       if c == '.' then
-        html := html ++ .text true str
+        html := html ++ .text str
         str := ""
         if iter ≠ content.endPos then
-          html := html ++ .text false "&shy;"
-    if !str.isEmpty then html := html ++ .text true str
+          html := html ++ .raw "&shy;"
+    if !str.isEmpty then html := html ++ .text str
     return html
   else
     return content
@@ -605,9 +605,9 @@ where
 
 /-- HTML that renders no visible content. -/
 partial def isEmptyHtml : Html → Bool
-  | .text _ s => s.isEmpty
+  | .text s | .raw s => s.isEmpty
   | .seq xs => xs.all isEmptyHtml
-  | .tag .. => false
+  | .element .. => false
 
 /--
 Removes the attributes named in `attrs` from `html`, returning their values alongside the
@@ -619,11 +619,11 @@ partial def takeAttrs (attrs : Array String) (html : Html) : Array (String × St
   go attrs html
 where
   go (remaining : Array String) : Html → Array (String × String) × Html
-    | html@(.tag name as contents) =>
+    | html@(.element name as contents) =>
       let here := as.filter (remaining.contains ·.1)
       let (found, contents') := go (remaining.filter (fun r => !here.any (·.1 == r))) contents
       if here.isEmpty && found.isEmpty then (#[], html)
-      else (here ++ found, .tag name (as.filter (!remaining.contains ·.1)) contents')
+      else (here ++ found, .element name (as.filter (!remaining.contains ·.1)) contents')
     | html@(.seq xs) =>
       let trimmed := xs.popWhile isEmptyHtml
       let trimmed := trimmed.extract (trimmed.findIdx (!isEmptyHtml ·)) trimmed.size
@@ -664,7 +664,7 @@ public partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM g H
       pure {{<span class={{"has-info " ++ cls}} {{spanAttrs}}>
           <span class="hover-container">
             <span class={{"hover-info messages"}}>
-              {{←  infos.mapM fun (s, info) => do return {{
+              {{← infos.mapM fun (s, info) => do return {{
                 <code class={{"verso-message " ++ s.«class»}}>{{← info.toHtml [] 10 toHtml}}</code> }}
               }}
             </span>
@@ -689,7 +689,7 @@ public partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM g H
             {{← if info.isEmpty then
                 pure {{"All goals completed! 🐙"}}
               else
-                .seq <$> info.mapIdxM (fun i x => x.toHtml toHtml i)}}
+                info.mapIdxM (fun i x => x.toHtml toHtml i)}}
           </span>
         </span>
       }}
diff --git a/verso/src/verso/Verso/Doc/Html.lean b/verso/src/verso/Verso/Doc/Html.lean
index 0d7c01167..35640379a 100644
--- a/verso/src/verso/Verso/Doc/Html.lean
+++ b/verso/src/verso/Verso/Doc/Html.lean
@@ -13,6 +13,7 @@ public import Verso.BuildLog
 namespace Verso.Doc.Html
 
 open Verso Output Doc Html
+open Lean (Html)
 open Verso (Severity SourceSpan MonadBuildLog Logger)
 open Verso.Code (HighlightHtmlM)
 
@@ -86,7 +87,7 @@ public instance [Monad m] : MonadLift (HighlightHtmlM genre) (HtmlT genre m) whe
 open HtmlT
 
 public def mkPartHeader (level : Nat) (contents : Html) (headerAttrs : Array (String × String) := #[]) : Html :=
-  .tag s!"h{level}" headerAttrs contents
+  .element s!"h{level}" headerAttrs contents
 
 public class ToHtml (genre : Genre) (m : Type → Type) (α : Type u) where
   toHtml (val : α) : HtmlT genre m Html
@@ -118,19 +119,19 @@ section
 open ToHtml
 
 partial def Inline.toHtml [Monad m] [GenreHtml g m] : Inline g → HtmlT g m Html
-  | .text str => pure <| .text true str
+  | .text str => return .text str
   | .link content dest => do
     pure {{ <a href={{dest}}> {{← content.mapM toHtml}} </a> }}
   | .image alt dest => do
     pure {{ <img src={{dest}} alt={{alt}}/> }}
   | .footnote name content => do
       pure {{ <details class="footnote"><summary>"["{{name}}"]"</summary>{{← content.mapM toHtml}}</details>}}
-  | .linebreak str => pure <| Html.text false str
+  | .linebreak str => return .raw str
   | .emph content => do
     pure {{ <em> {{← content.mapM toHtml }} </em> }}
   | .bold content => do
     pure {{ <strong> {{← content.mapM toHtml}} </strong> }}
-  | .code str => pure {{ <code> {{str}} </code> }}
+  | .code str => return {{ <code> {{str}} </code> }}
   | .math mode str => do
      let classes := "math " ++ match mode with | .inline => "inline" | .display => "display"
      pure {{ <code class={{classes}}>{{str}}</code> }}
@@ -162,7 +163,7 @@ partial def Block.toHtml [Monad m] [GenreHtml g m] [TraverseBlock g] (b : Block
         }}
       </dl>
     }}
-  | .code content => pure #[{{ <pre> {{ content }} </pre>}}]
+  | .code content => return {{ <pre> {{ content }} </pre>}}
   | .concat items => Html.seq <$> items.mapM Block.toHtml
   | .other container content => GenreHtml.block Inline.toHtml Block.toHtml container content
 
diff --git a/verso/src/verso/Verso/Output/Html.lean b/verso/src/verso/Verso/Output/Html.lean
index 2ddf8d49a..b90f41026 100644
--- a/verso/src/verso/Verso/Output/Html.lean
+++ b/verso/src/verso/Verso/Output/Html.lean
@@ -12,6 +12,7 @@ public import Lean.PrettyPrinter.Parenthesizer
 public import Lean.Elab.Term.TermElabM
 meta import Lean.Elab.Term.TermElabM
 public meta import Lean.Meta.Hint
+public import Lean.Data.Html
 
 import Verso.Output.Html.Entities
 public import Verso.Output.Html.AttributeName
@@ -21,101 +22,9 @@ public meta import Verso.Output.Html.Comments
 public meta import Verso.Output.Html.Tags
 import Verso.Output.Html.Tags
 
-namespace Verso.Output
-
-open Lean
-
-/--
-A representation of HTML, used to render Verso to the web.
--/
-public inductive Html where
-  /--
-  Textual content. If `escape` is `true`, then characters such as `'&'` are escaped to entities such
-  as `"&amp;"` during rendering.
-  -/
-  | text (escape : Bool) (string : String)
-  /--
-  A tag with the given name and attributes.
-  -/
-  | tag (name : String) (attrs : Array (String × String)) (contents : Html)
-  /--
-  A sequence of HTML values.
-  -/
-  | seq (contents : Array Html)
-deriving Repr, Inhabited, TypeName, BEq, Hashable
-
-public instance : ToJson Html where
-  toJson := private to
-where
-  to
-    | .text true string => .str string
-    | .text false string => json%{"raw": $string}
-    | .tag name attrs contents =>
-      let attrs : Json := .arr <| attrs.map fun (x, y) => json%{"name": $x, "value": $y}
-      json%{"tag": $name, "attrs": $attrs, "content": $(to contents)}
-    | .seq xs => .arr <| xs.map to
-
-public partial instance : FromJson Html where
-  fromJson? := private from?
-where
-  from?
-    | .str s => pure <| .text true s
-    | .arr xs => .seq <$> xs.mapM from?
-    | json@(.obj o) => do
-      if let some name := o["tag"]? then
-        let .str name := name
-          | throw s!"Expected a string as a tag name, got: {name.compress}"
-        let attrs ← json.getObjValAs? (Array Json) "attrs"
-        let attrs ← attrs.mapM fun a => do
-          return (← a.getObjValAs? String "name", ← a.getObjValAs? String "value")
-        let content ← json.getObjVal? "content" >>= from?
-        return .tag name attrs content
-      else if let some string := o["raw"]? then
-        let .str string := string
-          | throw s!"Expected a string for raw content, got: {string.compress}"
-        return .text false string
-      else
-        throw <|
-          s!"Failed to deserialize {json.compress} as HTML. " ++
-          "Expected key \"tag\" or key \"raw\"."
-    | other => throw s!"Failed to deserialize {other.compress} as HTML"
-
-
-open Syntax in
-public partial instance : Quote Html where
-  quote := q
-where
-  quoteArray {α : _} (_inst : Quote α) (xs : Array α) : TSyntax `term :=
-    mkCApp ``List.toArray #[quote xs.toList]
-  q
-    | .text esc str =>
-      mkCApp ``Html.text #[quote esc, quote str]
-    | .tag name attrs contents =>
-      mkCApp ``Html.tag #[quote name, quote attrs, q contents]
-    | .seq contents =>
-      mkCApp ``Html.seq #[quoteArray ⟨q⟩ contents]
-
-/--
-The empty HTML document.
--/
-@[suggest_for Verso.Output.Html.nil Verso.Output.Html.none]
-public def Html.empty : Html := .seq #[]
+/-! ## Additions to the Lean namespace -/
 
-/--
-Converts a string to HTML, escaping special characters.
--/
-public def Html.ofString : String → Html := .text true
-
-/--
-Appends two HTML documents.
--/
-public def Html.append : Html → Html → Html
-  | .seq xs, .seq ys => .seq (xs ++ ys)
-  | .seq xs, other => .seq (xs.push other)
-  | other, .seq ys => .seq (#[other] ++ ys)
-  | x, y => .seq #[x, y]
-
-public instance : Append Html := ⟨Html.append⟩
+namespace Lean.Html
 
 /--
 If the HTML consists of a single tag, then the given attribute is set to the provided value. If the
@@ -123,15 +32,15 @@ attribute already exists, then its value is replaced.
 
 If the HTML is not a single tag, no changes are made.
 -/
-public def Html.setAttribute (attr : String) (value : String) (html : Html) : Html :=
+public def setAttribute (attr : String) (value : String) (html : Html) : Html :=
   match html with
-  | .tag name attrs children =>
+  | .element name attrs children =>
     let attrs :=
       if let some i := attrs.findFinIdx? (·.1 == attr) then
         attrs.set i (attr, value)
       else
         attrs.push (attr, value)
-    .tag name attrs children
+    .element name attrs children
   | _ => html
 
 /--
@@ -140,52 +49,11 @@ attribute already exists, then its value is replaced.
 
 Panics if the HTML is not a single tag.
 -/
-public def Html.setAttribute! (attr : String) (value : String) (html : Html) : Html :=
+public def setAttribute! (attr : String) (value : String) (html : Html) : Html :=
   match html with
-  | .tag .. => html.setAttribute attr value
+  | .element .. => html.setAttribute attr value
   | other => panic! s!"Not a single HTML node: {repr other}"
 
-
-/--
-Converts an array of HTML elements into a single element by appending them.
-
-This is equivalent to using `Html.seq`, but may result a more compact representation.
--/
-public def Html.fromArray (htmls : Array Html) : Html :=
-  .seq <| htmls.foldl glue .empty
-where
-  glue
-    | arr, .seq hs => arr.append hs
-    | arr, other => arr.push other
-
-/--
-Converts a list of HTML elements into a single element by appending them.
-
-This is equivalent to using `Html.seq` on the corresponding array, but may result in a more compact representation.
--/
-public def Html.fromList (htmls : List Html) : Html := Id.run do
-  let mut out := Html.empty
-  for elt in htmls do
-    out := out ++ elt
-  out
-
-public instance : Coe (Array Html) Html where
-  coe arr := Html.fromArray arr
-
-public instance : Coe (List Html) Html where
-  coe arr := Html.fromList arr
-
-private def revFrom (i : Nat) (input : Array α) (output : Array α := #[]) : Array α :=
-  if h : i < input.size then
-    revFrom (i+1) input (output.push input[i])
-  else output
-termination_by input.size - i
-
-namespace Html
-
-/-- The default `DOCTYPE` for HTML5. -/
-public abbrev doctype := "<!DOCTYPE html>"
-
 /--
 Wrap content in a named group whose visible label should not participate in the document heading
 outline.
@@ -202,31 +70,18 @@ public def labeledGroup
   let labelAttrs :=
     (if labelClass.isEmpty then #[] else #[("class", labelClass)]) ++
       #[("id", id)]
-  .tag "div" groupAttrs <|
+  .element "div" groupAttrs <|
     .seq #[
-      .tag "p" labelAttrs (.text true label),
+      .element "p" labelAttrs (.text label),
       contents
     ]
 
-/--
-Visit the entire tree, applying rewrites in some monad. Return `none` to signal that no rewrites are
-to be performed.
--/
-public partial def visitM [Monad m]
-    (text : (escape : Bool) → String → m (Option Html) := (fun _ _ => pure none))
-    (tag : (name : String) → (attrs : Array (String × String)) → (contents : Html) → m (Option Html) := fun _ _ _ => pure none)
-    (seq : Array Html → m (Option Html) := fun _ => pure none)
-    (html : Html) : m Html :=
-  match html with
-  | .text esc str => do pure <| (← text esc str).getD html
-  | .tag name attrs contents => do
-    let contents' ← contents.visitM (text := text) (tag := tag) (seq := seq)
-    pure <| (← tag name attrs contents').getD (.tag name attrs contents')
-  | .seq elts => do
-    let elts' ← elts.mapM (visitM (text := text) (tag := tag) (seq := seq))
-    pure <| (← seq elts').getD (.seq elts')
+end Lean.Html
 
-public section
+/-! ## Django/Handlebars-like syntax -/
+
+namespace Verso.Output.Html
+open Lean
 
 declare_syntax_cat tag_name
 scoped syntax rawIdent : tag_name
@@ -242,7 +97,7 @@ scoped syntax (name := attrRawNamed) attributeName " = " attrib_val : attrib
 scoped syntax (name := attrBool) attributeName : attrib
 scoped syntax (name := attrAntiquoted) "{{" term "}}" : attrib
 
-public meta partial def _root_.Lean.TSyntax.tagName : TSyntax `tag_name → String
+public meta def _root_.Lean.TSyntax.tagName : TSyntax `tag_name → String
   | ⟨.node _ _ #[.atom _ x]⟩ => x
   | ⟨.node _ _ #[.ident _ _ x ..]⟩ => x.eraseMacroScopes.toString
   | _ => "unknown"
@@ -257,7 +112,6 @@ scoped syntax "r!" str : html
 
 scoped syntax "{{"  html+ "}}" : term
 scoped syntax "<<<" (attrib ppSpace) * ">>>" : term
-end
 
 open Lean Elab Term Meta in
 meta def elabAttrs (stxs : Array (TSyntax `attrib)) : TermElabM Expr := do
@@ -292,18 +146,18 @@ meta def elabAttrs (stxs : Array (TSyntax `attrib)) : TermElabM Expr := do
 open Lean Elab Term Meta in
 meta partial def elabHtml (stx : TSyntax `html) : TermElabM Expr := withRef stx do
   if stx.raw.getKind == ``comment then
-    return (← mkAppM ``Html.empty #[])
+    return .const ``Html.empty []
   match stx with
   | `(html| {{ $e:term }} ) =>
     elabTermEnsuringType e (some (.const ``Html []))
   | `(html| $text:str ) =>
-    mkAppM ``Html.text #[toExpr true, toExpr text.getString]
+    return mkApp (.const ``Html.text []) (toExpr text.getString)
   | `(html| s! $txt:interpolatedStr ) => do
     let txt ← elabTermEnsuringType (← `(s!$txt:interpolatedStr)) (some <| .const ``String [])
-    mkAppM ``Html.text #[toExpr true, txt]
+    return mkApp (.const ``Html.text []) txt
   | `(html| r! $txt:str ) =>
-    mkAppM ``Html.text #[toExpr false, toExpr txt.getString]
-  | `(html| <%$tk $tag:tag_name $[$extra]* >%$tk' $[$content:html]* </ $tag':tag_name>) => do
+    return mkApp (.const ``Html.raw []) (toExpr txt.getString)
+  | `(html| <%$tk $tag:tag_name $[$extra]* >%$tk' $[$children:html]* </ $tag':tag_name>) => do
     if tag.tagName != tag'.tagName then
       let hint ← MessageData.hint m!"Replace with opening tag" #[tag.tagName] (ref? := some tag')
       throwErrorAt tag' m!"Mismatched closing tag, expected `{tag.tagName}` but got `{tag'.tagName}`\n{hint}"
@@ -316,17 +170,17 @@ meta partial def elabHtml (stx : TSyntax `html) : TermElabM Expr := withRef stx
         else pure m!""
       throwErrorAt tag m!"`<{tag.tagName}>` doesn't allow contents{hint}"
     let attrs ← elabAttrs extra
-    let content ←
-      if h : content.size = 1 then
-        elabHtml content[0]
+    let children ←
+      if h : children.size = 1 then
+        elabHtml children[0]
       else
-        let content ← content.mapM elabHtml
-        let content ← mkArrayLit (.const ``Html []) content.toList
-        mkAppM ``Html.fromArray #[content]
-    mkAppM ``Html.tag #[toExpr tag.tagName, attrs, content]
+        let children ← children.mapM elabHtml
+        let children ← mkArrayLit (.const ``Html []) children.toList
+        pure <| mkApp (.const ``Html.ofArray []) children
+    return mkApp3 (.const ``Html.element []) (toExpr tag.tagName) attrs children
   | `(html| <$tag:tag_name $[$extra]* />) =>
     let attrs ← elabAttrs extra
-    mkAppM ``Html.tag #[toExpr tag.tagName, attrs, ← mkAppM ``Html.empty #[]]
+    return mkApp3 (.const ``Html.element []) (toExpr tag.tagName) attrs (.const ``Html.empty [])
   | _ => throwUnsupportedSyntax
 
 elab_rules : term
@@ -334,65 +188,77 @@ elab_rules : term
     withRef h <| elabHtml h
   | `(term| {{ $[$h:html]* }}) => do
     let h ← h.mapM fun (x : TSyntax `html) => withRef x <| elabHtml x
-    Meta.mkAppM ``Html.fromArray #[← Meta.mkArrayLit (.const ``Html []) h.toList]
+    return h.foldl (init := (.const ``Html.empty [])) (mkApp2 (.const ``Html.append []))
+
+/-- The default `DOCTYPE` for HTML5. -/
+public abbrev doctype := "<!DOCTYPE html>"
 
+end Verso.Output.Html
 
-public scoped instance : Coe String Html := ⟨.text true⟩
+/-! ## Deprecation aliases -/
 
-open Std.Format in
+namespace Verso.Output
 
-/--
-Converts HTML into a pretty-printer document. This is useful for debugging, but it does not preserve
-whitespace around preformatted content and scripts.
--/
-public partial def format : Html → Std.Format
-  | .text true str => .text (str.replace "&" "&amp;" |>.replace "<" "&lt;" |>.replace ">" "&gt;")
-  | .text false str => .text str
-  | .tag name attrs (.seq #[]) =>
-      Format.group (("<" ++ name) ++ group (line.prefixJoin (attrs.toList.map fun (k, v) => group (k ++ "=" ++ Format.line ++ s!"\"{v}\""))) ++ "/>")
-  | .tag "pre" attrs body =>
-      Format.group ("<pre" ++ group (line.prefixJoin (attrs.toList.map fun (k, v) => group (k ++ "=" ++ Format.line ++ s!"\"{v}\""))) ++ ">") ++ line ++
-      Html.format body ++ line ++
-      Format.group ("</pre>")
-  | .tag name attrs body =>
-    .nest 3 (line.joinSep [
-      Format.group (("<" ++ name) ++ group (line.prefixJoin (attrs.toList.map fun (k, v) => group (k ++ "=" ++ Format.line ++ s!"\"{v}\""))) ++ ">"),
-      Format.group (Html.format body)
-    ]) ++ line ++ Format.group ("</" ++ name ++ ">")
-  | .seq arr => line.joinSep <| arr.toList.map Html.format
+-- Constants with same name and type are re-exported in the old namespace.
+export Lean (Html Html.seq Html.empty Html.append Html.setAttribute Html.setAttribute!
+  Html.labeledGroup)
 
-/--
-Converts HTML into a string that's suitable for sending to browsers, but is also readable.
--/
-public partial def asString (html : Html) (indent : Nat := 0) (breakLines := true) : String :=
-  match html with
-  | .text true str => str.replace "&" "&amp;" |>.replace "<" "&lt;" |>.replace ">" "&gt;"
-  | .text false str => str
-  | .tag "pre" attrs body =>
-    "<pre" ++ attrsAsString attrs ++ ">" ++
-    Html.asString (indent := 0) (breakLines := false) body ++
-    "</pre>" ++ breakline "pre"
-  | .tag "code" attrs body =>
-    "<code" ++ attrsAsString attrs ++ ">" ++
-    Html.asString (indent := 0) (breakLines := false) body ++
-    "</code>" ++ breakline "code"
-  | .tag name attrs (.seq #[]) =>
-    if name ∈ mustClose then
-      "<" ++ name ++ attrsAsString attrs ++ "></" ++ name ++ ">" ++ breakline name
-    else
-      "<" ++ name ++ attrsAsString attrs ++ ">" ++ breakline name
-  | .tag name attrs (.seq #[subElem]) =>
-    "<" ++ name ++ attrsAsString attrs ++ ">" ++ breakline' name ++
-    asString subElem (indent := indent + 2) (breakLines := breakLines) ++
-    s!"</{name}>" ++ breakline name
-  | .tag name attrs body =>
-      "<" ++ name ++ attrsAsString attrs ++ ">" ++ breakline' name ++
-      Html.asString body (indent := indent + 2) (breakLines := breakLines) ++
-      s!"</{name}>" ++ breakline name
-  | .seq elts => String.join (elts.toList.map (Html.asString · (indent := indent) (breakLines := breakLines)))
-where
-  newline i := "\n" ++ String.ofList (List.replicate i ' ')
-  breakline tag := if breakLines && tag ∈ newlineAfter then newline indent else ""
-  breakline' tag := if breakLines && tag ∈ newlineAfter then newline (indent + 2) else ""
-  attrsAsString xs := String.join <| xs.toList.map (fun ⟨k, v⟩ => s!" {k}=\"{escapeAttr v}\"")
-  escapeAttr str := str |>.replace "&" "&amp;" |>.replace "\"" "&quot;"
+-- Constants whose name or type changed become deprecated protected abbrevs in the old namespace.
+namespace Html
+
+@[deprecated Lean.Html.ofString (since := "2026-09-02")]
+public protected abbrev text : Bool → String → Html := Lean.Html.ofString
+
+@[deprecated Lean.Html.element (since := "2026-09-02")]
+public protected abbrev tag : String → Array (String × String) → Html → Html := Lean.Html.element
+
+@[deprecated Lean.Html.text (since := "2026-09-02")]
+public protected abbrev ofString : String → Html := Lean.Html.text
+
+@[deprecated Lean.Html.ofArray (since := "2026-09-02")]
+public protected abbrev fromArray : Array Html → Html := Lean.Html.ofArray
+
+@[deprecated Lean.Html.ofList (since := "2026-09-02")]
+public protected abbrev fromList : List Html → Html := Lean.Html.ofList
+
+@[deprecated Lean.Html.rewritePostM +typeChanged (since := "2026-09-02")]
+public protected abbrev visitM [Monad m]
+    (text : (escape : Bool) → String → m (Option Html) := (fun _ _ => pure none))
+    (tag : (name : String) → (attrs : Array (String × String)) → (contents : Html) → m (Option Html) := fun _ _ _ => pure none)
+    (seq : Array Html → m (Option Html) := fun _ => pure none)
+    (html : Html) : m Html :=
+  html.rewritePostM fun h => match h with
+    | .text s => return (← text true s).getD h
+    | .raw s => return (← text false s).getD h
+    | .element t a c => return (← tag t a c).getD h
+    | .seq a => return (← seq a).getD h
+
+set_option linter.unusedVariables false in
+@[deprecated Lean.Html.render +typeChanged (since := "2026-09-02")]
+public protected abbrev asString (html : Html) (indent : Nat := 0) (breakLines := true) : String :=
+  html.render
+
+end Verso.Output.Html
+
+-- Constants whose name or type changed, and which are commonly used with dot notation,
+-- also get a deprecated alias in the new namespace.
+namespace Lean.Html
+
+@[deprecated Lean.Html.rewritePostM +typeChanged (since := "2026-09-02")]
+public abbrev visitM [Monad m]
+    (text : (escape : Bool) → String → m (Option Html) := (fun _ _ => pure none))
+    (tag : (name : String) → (attrs : Array (String × String)) → (contents : Html) → m (Option Html) := fun _ _ _ => pure none)
+    (seq : Array Html → m (Option Html) := fun _ => pure none)
+    (html : Html) : m Html :=
+  html.rewritePostM fun h => match h with
+    | .text s => return (← text true s).getD h
+    | .raw s => return (← text false s).getD h
+    | .element t a c => return (← tag t a c).getD h
+    | .seq a => return (← seq a).getD h
+
+set_option linter.unusedVariables false in
+@[deprecated Lean.Html.render +typeChanged (since := "2026-09-02")]
+public abbrev asString (html : Html) (indent : Nat := 0) (breakLines := true) : String :=
+  html.render
+
+end Lean.Html
diff --git a/verso/test-projects/custom-genre/SimplePage.lean b/verso/test-projects/custom-genre/SimplePage.lean
index 119d525c0..aab9797c8 100644
--- a/verso/test-projects/custom-genre/SimplePage.lean
+++ b/verso/test-projects/custom-genre/SimplePage.lean
@@ -206,7 +206,7 @@ instance : GenreHtml SimplePage (BuildLogT IO) where
     -- It's important that this not include the metadata in the recursive call, or the generator
     -- will loop (the metadata's presence is what triggers the call to `GenreHtml.part`)
     let part' := .mk title titleString none content' subParts
-    recur part' (fun lvl title => .tag s!"h{lvl}" #[("id", metadata.tag)] title)
+    recur part' (fun lvl title => .element s!"h{lvl}" #[("id", metadata.tag)] title)
   -- There are no genre-specific blocks, so no code is needed here
   block _ _ blkExt := nomatch blkExt
   inline recur
@@ -264,7 +264,7 @@ def render (doc : Part SimplePage) : IO UInt32 := do
 
     IO.println "Writing to index.html"
     IO.FS.withFile "index.html" .write fun h => do
-      h.putStrLn html.asString
+      h.putStrLn html.render
 
 end SimplePage
 
diff --git a/verso/test-projects/website/DemoSiteMain.lean b/verso/test-projects/website/DemoSiteMain.lean
index 0131afc9b..ededd0012 100644
--- a/verso/test-projects/website/DemoSiteMain.lean
+++ b/verso/test-projects/website/DemoSiteMain.lean
@@ -8,6 +8,7 @@ import VersoBlog
 import DemoSite
 
 open Verso Genre Blog Site Syntax
+open Lean (Html)
 
 open Output Html Template Theme in
 def theme : Theme := { Theme.default with