chore: use upstream HTML type

doc/UsersGuide/Output/HTML.lean

@@ -15,6 +15,7 @@ open InlineLean
 open Verso.Doc
 
 open Verso.Output
+open Lean (Html)
 
 open Verso.Code
 
@@ -26,23 +27,21 @@ 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.format}
-
 {docstring Html.asString}
 
 HTML documents are written in double curly braces, in a syntax very much like HTML itself.

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}
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-27
+leanprover/lean4-pr-releases:pr-release-14935-6b54eee

src/tests/Tests/GenericCode.lean

@@ -44,21 +44,21 @@ info: Verso.Doc.Part.mk
 #guard_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")])])
 -/
 #guard_msgs in
   #eval Doc.Genre.none.toHtml (m := Id) {} () () {} {} {} code1.toPart |>.run .empty |>.fst

src/tests/Tests/HoverMerge.lean

@@ -10,7 +10,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
 
@@ -20,64 +21,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.
 #guard takeAttrs #["data-verso-hover"] tok == (#[("data-verso-hover", "5")], tokNoHover)
 
 -- The attribute is found through a wrapping element, such as a link.
-#guard takeAttrs #["data-verso-hover"] (.tag "a" #[("href", "x.html")] tok) ==
-  (#[("data-verso-hover", "5")], .tag "a" #[("href", "x.html")] tokNoHover)
+#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.
 #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.
 #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.
 #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")))
 #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.
-#guard takeAttrs #["data-verso-hover"] (.tag "a" #[("data-verso-hover", "9")] tok) ==
-  (#[("data-verso-hover", "9")], .tag "a" #[] tok)
+#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.
-#guard takeAttrs #["data-verso-hover"] (.seq #[.text true "", tok, .seq #[]]) ==
+#guard takeAttrs #["data-verso-hover"] (.seq #[.text "", tok, .seq #[]]) ==
   (#[("data-verso-hover", "5")], tokNoHover)
 
 -- Adjacent content blocks the search, including whitespace.
-#guard takeAttrs #["data-verso-hover"] (.seq #[tok, .text true "y"]) ==
-  (#[], .seq #[tok, .text true "y"])
+#guard takeAttrs #["data-verso-hover"] (.seq #[tok, .text "y"]) ==
+  (#[], .seq #[tok, .text "y"])
 #guard takeAttrs #["data-verso-hover"] (.seq #[tok, tokNoHover]) == (#[], .seq #[tok, tokNoHover])
-#guard takeAttrs #["data-verso-hover"] (.seq #[.text true " ", tok]) ==
-  (#[], .seq #[.text true " ", tok])
+#guard takeAttrs #["data-verso-hover"] (.seq #[.text " ", tok]) ==
+  (#[], .seq #[.text " ", tok])
 
 -- Adjacent content inside a wrapper blocks the search.
-#guard takeAttrs #["data-verso-hover"] (.tag "a" #[] (.seq #[tok, tokNoHover])) ==
-  (#[], .tag "a" #[] (.seq #[tok, tokNoHover]))
+#guard takeAttrs #["data-verso-hover"] (.element "a" #[] (.seq #[tok, tokNoHover])) ==
+  (#[], .element "a" #[] (.seq #[tok, tokNoHover]))
 
 -- Content without the attributes is unchanged.
 #guard takeAttrs #["data-verso-hover"] tokNoHover == (#[], tokNoHover)
-#guard takeAttrs #["data-verso-hover"] (.text true "x") == (#[], .text true "x")
+#guard takeAttrs #["data-verso-hover"] (.text "x") == (#[], .text "x")
 #guard takeAttrs #["data-verso-hover"] (.seq #[]) == (#[], .seq #[])
 
 def hlTok : Highlighted := .token ⟨.keyword none none none, "rfl"⟩

src/tests/Tests/Html.lean

@@ -4,22 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
 module
-meta import all Verso.Output.Html
+import Verso.Output.Html
+meta import Verso.Output.Html
 
 namespace Verso.Tests.Html
 
-open Verso.Output
+open Lean (Html)
 open Verso.Output.Html
 
 /-! ## Tests for HTML syntax macros -/
 
 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 #[])
 -/
 #guard_msgs in
 #eval testAttrs
@@ -28,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 #[])
 -/
 #guard_msgs in
 #eval testAttrsAntiquotes
@@ -51,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"])])])
 -/
 #guard_msgs in
   #eval test
@@ -80,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") -/
 #guard_msgs in
   #eval leanKwTest
 
@@ -118,7 +118,7 @@ info: |
 
 /-- 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)
+  #eval Html.asString (.element "p" #[] (.raw "x & y &lt; <em>z</em>")) (breakLines := false)
 
 /-- info: "<p class=\"a&amp;b&quot;c\">x</p>" -/
 #guard_msgs in

src/tests/Tests/NestedTacticHtml.lean

@@ -24,7 +24,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
@@ -115,8 +115,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. -/
@@ -126,9 +126,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
@@ -139,12 +139,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"
@@ -156,7 +156,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
 
@@ -167,15 +167,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