diff --git a/doc/UsersGuide/Output/HTML.lean b/doc/UsersGuide/Output/HTML.lean index adb7d31ec..6658954b7 100644 --- a/doc/UsersGuide/Output/HTML.lean +++ b/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. diff --git a/doc/UsersGuide/Websites.lean b/doc/UsersGuide/Websites.lean index 116214076..57e48a79a 100644 --- a/doc/UsersGuide/Websites.lean +++ b/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/lean-toolchain b/lean-toolchain index b8f3deceb..3bfd46501 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-08-27 +leanprover/lean4-pr-releases:pr-release-14935-6b54eee diff --git a/src/tests/Tests/GenericCode.lean b/src/tests/Tests/GenericCode.lean index 478481550..4592ee280 100644 --- a/src/tests/Tests/GenericCode.lean +++ b/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 diff --git a/src/tests/Tests/HoverMerge.lean b/src/tests/Tests/HoverMerge.lean index 43fb72a39..a536a4e98 100644 --- a/src/tests/Tests/HoverMerge.lean +++ b/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"⟩ diff --git a/src/tests/Tests/Html.lean b/src/tests/Tests/Html.lean index 515cd0150..3de647da0 100644 --- a/src/tests/Tests/Html.lean +++ b/src/tests/Tests/Html.lean @@ -4,11 +4,12 @@ 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 -/ @@ -16,10 +17,10 @@ open Verso.Output.Html private def testAttrs := {{ }} /-- -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 := {{ }} /-- -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 := {{ }} -/-- 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: "

x & y < z

" -/ #guard_msgs in - #eval Html.asString (.tag "p" #[] (.text false "x & y < z")) (breakLines := false) + #eval Html.asString (.element "p" #[] (.raw "x & y < z")) (breakLines := false) /-- info: "

x

" -/ #guard_msgs in diff --git a/src/tests/Tests/NestedTacticHtml.lean b/src/tests/Tests/NestedTacticHtml.lean index 9eb774e8e..cec6d8b67 100644 --- a/src/tests/Tests/NestedTacticHtml.lean +++ b/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 `` 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 `` 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/src/tests/Tests/Serialization.lean b/src/tests/Tests/Serialization.lean index 70729f8af..f980e86b5 100644 --- a/src/tests/Tests/Serialization.lean +++ b/src/tests/Tests/Serialization.lean @@ -260,30 +260,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 @@ -403,7 +404,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/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index 3faebe463..9cfae33cf 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/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/src/verso-blog/VersoBlog/Basic.lean b/src/verso-blog/VersoBlog/Basic.lean index d72c4ddfc..13fd2eb81 100644 --- a/src/verso-blog/VersoBlog/Basic.lean +++ b/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/src/verso-blog/VersoBlog/Component.lean b/src/verso-blog/VersoBlog/Component.lean index 9d5bbf696..488259a4d 100644 --- a/src/verso-blog/VersoBlog/Component.lean +++ b/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/src/verso-blog/VersoBlog/Generate.lean b/src/verso-blog/VersoBlog/Generate.lean index c9ed0c861..72c3db8f2 100644 --- a/src/verso-blog/VersoBlog/Generate.lean +++ b/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 diff --git a/src/verso-blog/VersoBlog/Template.lean b/src/verso-blog/VersoBlog/Template.lean index 56aba8ad7..7bb365c26 100644 --- a/src/verso-blog/VersoBlog/Template.lean +++ b/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 {{
{{summary}} {{← contents.mapM goB}}
}} | .htmlWrapper name attrs, contents => do - Html.tag name attrs <$> contents.mapM goB + Html.element name attrs <$> contents.mapM goB | .htmlDiv classes, contents => do pure {{
{{← contents.mapM goB}}
}} | .blob html, _ => pure html @@ -194,7 +195,7 @@ def blockHtml (g : Genre) let contents := contents.extract 1 return {{
- {{ .tag s!"h{lvl + 1}" #[] (← first.mapM goI) }} + {{ .element s!"h{lvl + 1}" #[] (← first.mapM goI) }} {{ ← contents.mapM goB }}
}} @@ -353,9 +354,9 @@ def builtinHeader : TemplateM Html := do -- These should come first so later stylesheets can easily override them. out := out ++ {{}} for style in (← read).builtInStyles do - out := out ++ {{"\n"}} + out := out ++ {{"\n"}} for script in (← read).builtInScripts do - out := out ++ {{"\n"}} + out := out ++ {{"\n"}} for js in (← read).jsFiles do out := out ++ {{}} for css in (← read).cssFiles do @@ -368,9 +369,9 @@ def builtinHeader : TemplateM Html := do -- Components for style in (← get).headerCss do - out := out ++ {{"\n"}} + out := out ++ {{"\n"}} for script in (← get).headerJs do - out := out ++ {{"\n"}} + out := out ++ {{"\n"}} pure out diff --git a/src/verso-blog/VersoBlog/Theme.lean b/src/verso-blog/VersoBlog/Theme.lean index c99c7ffc4..6f433fe59 100644 --- a/src/verso-blog/VersoBlog/Theme.lean +++ b/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 => {{
- {{(md : Post.PartMetadata).authors.map ({{{{Html.text true ·}}}}) |>.toArray}} + {{(md : Post.PartMetadata).authors.map ({{{{Html.text ·}}}}) |>.toArray}}
{{md.date.toIso8601String}} @@ -352,7 +353,7 @@ def archiveEntry : Template := do | some md => {{
- {{(md : Post.PartMetadata).authors.map ({{{{Html.text true ·}}}}) |>.toArray}} + {{(md : Post.PartMetadata).authors.map ({{{{Html.text ·}}}}) |>.toArray}}
{{md.date.toIso8601String}} diff --git a/src/verso-html/VersoHtmlMain.lean b/src/verso-html/VersoHtmlMain.lean index 568082fdc..822f6e8cd 100644 --- a/src/verso-html/VersoHtmlMain.lean +++ b/src/verso-html/VersoHtmlMain.lean @@ -44,8 +44,8 @@ private def headContents : Html := {{ - - + + diff --git a/src/verso-literate-code/VersoLiterateCode.lean b/src/verso-literate-code/VersoLiterateCode.lean index 969acb144..6bb217212 100644 --- a/src/verso-literate-code/VersoLiterateCode.lean +++ b/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 }} - | .header n title => .tag s!"h{n + 1}" #[] <| texts title + | .header n title => .element s!"h{n + 1}" #[] <| texts title | .blockquote bs => {{
{{blocks bs}}
}} | .hr => {{
}} - | .html xs => .text false (String.join xs.toList) + | .html xs => .raw (String.join xs.toList) | .code _ _ _ ss => {{
{{String.join ss.toList}}
}} blocks : Array MD4Lean.Block → Html @@ -196,7 +196,7 @@ where | .img src title alt => {{{{String.join 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/src/verso-literate-html/LiterateHtmlMain.lean b/src/verso-literate-html/LiterateHtmlMain.lean index 5623de1cb..b2ee4fa28 100644 --- a/src/verso-literate-html/LiterateHtmlMain.lean +++ b/src/verso-literate-html/LiterateHtmlMain.lean @@ -194,8 +194,8 @@ private def mkHeadContents (litConfig : LiterateConfig) (includeCodeAssets : Boo - - + + }} else .empty let copyButtonTag : Html := if includeCodeAssets then {{ diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index 62ca5ee35..3c8aa18b5 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -424,7 +424,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⟩ @@ -463,7 +464,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, diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean index 92721f64d..7f277c457 100644 --- a/src/verso-manual/VersoManual/Basic.lean +++ b/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 @@ -226,7 +226,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 @@ -329,7 +329,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. -/ @@ -484,10 +484,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 := @@ -653,9 +653,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) → @@ -667,8 +667,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) → @@ -771,7 +771,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 #[] /-- @@ -779,7 +779,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 := {} @@ -815,7 +815,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 #[] /-- @@ -823,7 +823,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 := {} @@ -1558,7 +1558,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 /-- @@ -1598,7 +1598,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/src/verso-manual/VersoManual/Diagrams.lean b/src/verso-manual/VersoManual/Diagrams.lean index 9b6cdaa19..6be570288 100644 --- a/src/verso-manual/VersoManual/Diagrams.lean +++ b/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 {{
- {{Html.text false svgStr}} + {{Html.raw svgStr}}
}} usePackages := ["\\usepackage{svg}"] diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 153f6ab6b..f2e06e587 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -1621,7 +1621,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 let xref ← HtmlT.state let idAttr := xref.htmlId id diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean index 723035fe6..b8c7778ca 100644 --- a/src/verso-manual/VersoManual/Glossary.lean +++ b/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/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index 492ffdc85..ad8320697 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -16,6 +16,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 @@ -263,9 +264,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 @@ -372,7 +373,7 @@ where linkify (path : Path) (id : Option String) (html : Html) := match html with - | .tag "a" _ _ => html + | .element "a" _ _ => html | other => {{{{other}}}} sectionNum num := match num with @@ -456,8 +457,8 @@ public def page {{extraJsFiles.map fun f => ({{}})}} {{extraStylesheets.map (fun url => {{ }})}} - {{extraCss.toArray.map ({{}})}} - {{extraJs.toArray.map ({{}})}} + {{extraCss.toArray.map ({{}})}} + {{extraJs.toArray.map ({{}})}} {{extraHead}} @@ -518,7 +519,7 @@ public def page public def relativize (path : Path) (html : Html) : Html := - html.visitM (m := ReaderT Path Id) (tag := rwTag) |>.run path + html.visitM (m := ReaderT Path Id) (element := rwTag) |>.run path where urlAttr (name : String) : Bool := name ∈ ["href", "src", "data", "poster"] rwAttr (attr : String × String) : ReaderT Path Id (String × String) := do @@ -534,4 +535,4 @@ where -- 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 + return some <| .element tag (← attrs.mapM rwAttr) content diff --git a/src/verso-manual/VersoManual/Html/Config.lean b/src/verso-manual/VersoManual/Html/Config.lean index 128d83014..bef139280 100644 --- a/src/verso-manual/VersoManual/Html/Config.lean +++ b/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/src/verso-manual/VersoManual/Html/SoftHyphenate.lean b/src/verso-manual/VersoManual/Html/SoftHyphenate.lean index 3cd526847..b45ce36f4 100644 --- a/src/verso-manual/VersoManual/Html/SoftHyphenate.lean +++ b/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 "­") + else if let some (.element "wbr" ..) := xs.back? then xs + else xs.push (.raw "­") /-- Adds soft hyphenation opportunities ({lit}`` or {lit}`­`) 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 {{}} 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,7 +66,7 @@ HTML, allowing browsers to break the word at that point. Line break opportunitie {lit}`Verso.Genre.Manual.soft­Hyphenate­Identifiers`. -/ public def softHyphenateTextNodes (html : Html) : Html := - html.visitM (m := Id) (text := rwText) + html.visitM (m := Id) (text := rwText true) (raw := rwText false) where rwText esc str := pure (some (softHyphenateText esc str)) @@ -79,8 +80,8 @@ hyphenation opportunities on transitions from lower-case to upper-case letters, Here, “identifiers” refers to text nodes found within `` tags. -/ public partial def softHyphenateIdentifiers (html : Html) : Html := - html.visitM (m := Id) (tag := rwTag) + html.visitM (m := Id) (element := rwTag) where rwTag - | "code", attrs, content => pure (some (.tag "code" attrs (softHyphenateTextNodes content))) + | "code", attrs, content => pure (some (.element "code" attrs (softHyphenateTextNodes content))) | _, _, _ => pure none diff --git a/src/verso-manual/VersoManual/Index.lean b/src/verso-manual/VersoManual/Index.lean index e0e2b7dbc..0087b2a5a 100644 --- a/src/verso-manual/VersoManual/Index.lean +++ b/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 {{
  • {{← e.toHtml goI}}
    • }} return {{
    {{hdr ++ {{
      {{entries'}}
    }} }}
    }} diff --git a/src/verso-manual/VersoManual/License.lean b/src/verso-manual/VersoManual/License.lean index 41460ad56..5d8f6e89d 100644 --- a/src/verso-manual/VersoManual/License.lean +++ b/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 {{
    - {{.tag s!"h{headerLevel}" #[] dependency }} + {{.element s!"h{headerLevel}" #[] dependency }} {{link.map (fun url => {{{{url}}}}) |>.getD .empty}} {{howUsed.map paragraphedHtml |>.getD .empty}} {{identifier}} @@ -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 {{
    {{hdrHtml}}{{paragraphedHtml txt}}
    }} diff --git a/src/verso-manual/VersoManual/Literate.lean b/src/verso-manual/VersoManual/Literate.lean index 9fd8c6e0a..aa3459664 100644 --- a/src/verso-manual/VersoManual/Literate.lean +++ b/src/verso-manual/VersoManual/Literate.lean @@ -48,7 +48,7 @@ block_extension Block.literateDocstringPart (level : Nat) where let contents := contents.extract 1 pure {{
    - {{.tag s!"h{level + 1}" #[] title}} + {{.element s!"h{level + 1}" #[] title}} {{← contents.mapM goB}}
    }} diff --git a/src/verso-manual/VersoManual/LocalContents.lean b/src/verso-manual/VersoManual/LocalContents.lean index 23c84aefa..c03eba684 100644 --- a/src/verso-manual/VersoManual/LocalContents.lean +++ b/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/src/verso-manual/VersoManual/Row.lean b/src/verso-manual/VersoManual/Row.lean index b46a38f75..175c7db28 100644 --- a/src/verso-manual/VersoManual/Row.lean +++ b/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/src/verso-manual/VersoManual/Table.lean b/src/verso-manual/VersoManual/Table.lean index 18f779df3..c63cb870c 100644 --- a/src/verso-manual/VersoManual/Table.lean +++ b/src/verso-manual/VersoManual/Table.lean @@ -117,8 +117,8 @@ block_extension Block.table (columns : Nat) (header : Bool) (tag : Option String return {{ {{← 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 {{}} else diff --git a/src/verso-search/VersoSearch/DomainSearch.lean b/src/verso-search/VersoSearch/DomainSearch.lean index e8222be8b..52a2f9565 100644 --- a/src/verso-search/VersoSearch/DomainSearch.lean +++ b/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/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean index d7f300902..b12f426d3 100644 --- a/src/verso/Verso/Code/Highlighted.lean +++ b/src/verso/Verso/Code/Highlighted.lean @@ -17,7 +17,7 @@ import VersoUtil.WfRec 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 @@ -503,11 +503,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 "­" - if !str.isEmpty then html := html ++ .text true str + html := html ++ .raw "­" + if !str.isEmpty then html := html ++ .text str return html else return content @@ -606,9 +606,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 @@ -620,11 +620,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 @@ -665,7 +665,7 @@ public partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM g H pure {{ - {{← infos.mapM fun (s, info) => do return {{ + {{← infos.mapM fun (s, info) => do return {{ {{← info.toHtml [] 10 toHtml}} }} }} @@ -690,7 +690,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)}} }} diff --git a/src/verso/Verso/Doc/Html.lean b/src/verso/Verso/Doc/Html.lean index 0d7c01167..35640379a 100644 --- a/src/verso/Verso/Doc/Html.lean +++ b/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 {{ {{← content.mapM toHtml}} }} | .image alt dest => do pure {{ {{alt}}/ }} | .footnote name content => do pure {{
    "["{{name}}"]"{{← content.mapM toHtml}}
    }} - | .linebreak str => pure <| Html.text false str + | .linebreak str => return .raw str | .emph content => do pure {{ {{← content.mapM toHtml }} }} | .bold content => do pure {{ {{← content.mapM toHtml}} }} - | .code str => pure {{ {{str}} }} + | .code str => return {{ {{str}} }} | .math mode str => do let classes := "math " ++ match mode with | .inline => "inline" | .display => "display" pure {{ {{str}} }} @@ -162,7 +163,7 @@ partial def Block.toHtml [Monad m] [GenreHtml g m] [TraverseBlock g] (b : Block }} }} - | .code content => pure #[{{ 
     {{ content }}
    }}] + | .code content => return {{ 
     {{ content }}
    }} | .concat items => Html.seq <$> items.mapM Block.toHtml | .other container content => GenreHtml.block Inline.toHtml Block.toHtml container content diff --git a/src/verso/Verso/Output/Html.lean b/src/verso/Verso/Output/Html.lean index 2ddf8d49a..61272bc43 100644 --- a/src/verso/Verso/Output/Html.lean +++ b/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 +/-! ## Additions to the Lean namespace -/ -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 `"&"` 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 #[] - -/-- -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 := "" - /-- Wrap content in a named group whose visible label should not participate in the document heading outline. @@ -202,31 +70,58 @@ 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 ] +open Verso.Output.Html (mustClose newlineAfter) in /-- -Visit the entire tree, applying rewrites in some monad. Return `none` to signal that no rewrites are -to be performed. +Converts HTML into a string that's suitable for sending to browsers, but is also readable. -/ -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 := +public partial def asString (html : Html) (indent : Nat := 0) (breakLines := true) : String := 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') + | .raw str => str + | .text str => str.replace "&" "&" |>.replace "<" "<" |>.replace ">" ">" + | .element "pre" attrs body => + "" ++ + body.asString (indent := 0) (breakLines := false) ++ + "" ++ breakline "pre" + | .element "code" attrs body => + "" ++ + body.asString (indent := 0) (breakLines := false) ++ + "" ++ breakline "code" + | .element name attrs (.seq #[]) => + if name ∈ mustClose then + "<" ++ name ++ attrsAsString attrs ++ ">" ++ breakline name + else + "<" ++ name ++ attrsAsString attrs ++ ">" ++ breakline name + | .element name attrs (.seq #[subElem]) => + "<" ++ name ++ attrsAsString attrs ++ ">" ++ breakline' name ++ + subElem.asString (indent := indent + 2) (breakLines := breakLines) ++ + s!"" ++ breakline name + | .element name attrs body => + "<" ++ name ++ attrsAsString attrs ++ ">" ++ breakline' name ++ + body.asString (indent := indent + 2) (breakLines := breakLines) ++ + s!"" ++ breakline name + | .seq elts => String.join (elts.toList.map (·.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 "&" "&" |>.replace "\"" """ -public section +/-- The default `DOCTYPE` for HTML5. -/ +public abbrev doctype := "" + +end Lean.Html + +/-! ## JSX-like syntax -/ + +namespace Verso.Output.Html +open Lean declare_syntax_cat tag_name scoped syntax rawIdent : tag_name @@ -242,7 +137,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 +152,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 +186,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]* ) => do + return mkApp (.const ``Html.raw []) (toExpr txt.getString) + | `(html| <%$tk $tag:tag_name $[$extra]* >%$tk' $[$children:html]* ) => 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 +210,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 +228,6 @@ 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] - - -public scoped instance : Coe String Html := ⟨.text true⟩ - -open Std.Format in - -/-- -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 "&" "&" |>.replace "<" "<" |>.replace ">" ">") - | .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 (" group (k ++ "=" ++ Format.line ++ s!"\"{v}\""))) ++ ">") ++ line ++ - Html.format body ++ line ++ - Format.group ("") - | .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 ("") - | .seq arr => line.joinSep <| arr.toList.map Html.format + return h.foldl (init := (.const ``Html.empty [])) (mkApp2 (.const ``Html.append [])) -/-- -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 "&" "&" |>.replace "<" "<" |>.replace ">" ">" - | .text false str => str - | .tag "pre" attrs body => - "" ++ - Html.asString (indent := 0) (breakLines := false) body ++ - "" ++ breakline "pre" - | .tag "code" attrs body => - "" ++ - Html.asString (indent := 0) (breakLines := false) body ++ - "" ++ breakline "code" - | .tag name attrs (.seq #[]) => - if name ∈ mustClose then - "<" ++ name ++ attrsAsString attrs ++ ">" ++ 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!"" ++ breakline name - | .tag name attrs body => - "<" ++ name ++ attrsAsString attrs ++ ">" ++ breakline' name ++ - Html.asString body (indent := indent + 2) (breakLines := breakLines) ++ - s!"" ++ 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 "&" "&" |>.replace "\"" """ +end Verso.Output.Html diff --git a/test-projects/custom-genre/SimplePage.lean b/test-projects/custom-genre/SimplePage.lean index 119d525c0..9c5301543 100644 --- a/test-projects/custom-genre/SimplePage.lean +++ b/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 diff --git a/test-projects/website/DemoSiteMain.lean b/test-projects/website/DemoSiteMain.lean index 0131afc9b..ededd0012 100644 --- a/test-projects/website/DemoSiteMain.lean +++ b/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
    {{cell}}