[#14935] feat: add Html type

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

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

doc-gen4/DocGen4/Output/DocString.lean

@@ -179,15 +179,15 @@ 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
         match ← nameToLink? sTail with
         | 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,29 +291,29 @@ 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
       let liHtml ← renderLi item funName isTight
       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
 

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

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)
   ]

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

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 }
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-10-01
+leanprover/lean4-pr-releases:pr-release-14935-8eaba5e

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>

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