From 5b56be76f2e0e0a4e3a74bc66410cc9cbb17e159 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 21 Jun 2022 20:54:29 +0200 Subject: [PATCH] chore: Cleanup HTML syntax and pretty printing --- DocGen4/LeanInk/Output.lean | 76 ++++++++++++++++---------------- DocGen4/Output/Base.lean | 8 ++-- DocGen4/Output/Module.lean | 8 ++-- DocGen4/Output/Navbar.lean | 16 +++---- DocGen4/Output/ToHtmlFormat.lean | 4 -- Main.lean | 1 - 6 files changed, 54 insertions(+), 59 deletions(-) diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index 190d453..720c4cf 100644 --- a/DocGen4/LeanInk/Output.lean +++ b/DocGen4/LeanInk/Output.lean @@ -33,21 +33,21 @@ def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
- {tyi.name} - : - {tyi.type} - - - - - - + {tyi.name} + : + {tyi.type} + +
+
+ + + def Token.processSemantic (t : Token) : Html := match t.semanticType with - | some "Name.Attribute" => {t.raw} - | some "Name.Variable" => {t.raw} - | some "Keyword" => {t.raw} + | some "Name.Attribute" => {t.raw} + | some "Name.Variable" => {t.raw} + | some "Keyword" => {t.raw} | _ => Html.text t.raw def Token.toHtml (t : Token) : AlectryonM Html := do @@ -63,39 +63,39 @@ def Token.toHtml (t : Token) : AlectryonM Html := do -- TODO: Show rest of token [parts] - + def Contents.toHtml : Contents → AlectryonM Html | .string value => pure {value} - + | .experimentalTokens values => do let values ← values.mapM Token.toHtml pure [values] - + def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do - let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]] + let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]] if h.body != "" then hypParts := hypParts.push - := - {h.body} - + := + {h.body} + hypParts := hypParts.push - : - {h.type} - + : + {h.type} + pure [hypParts] - + def Goal.toHtml (g : Goal) : AlectryonM Html := do let mut hypotheses := #[] @@ -107,21 +107,21 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do
[hypotheses] - +
-
{g.name} - +
{g.name} +
{g.conclusion} - - +
+
def Message.toHtml (m : Message) : AlectryonM Html := do pure
-- TODO: This might have to be done in a fancier way {m.contents} - +
def Sentence.toHtml (s : Sentence) : AlectryonM Html := do let messages := @@ -129,7 +129,7 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do #[
[←s.messages.mapM Message.toHtml] - +
] else #[] @@ -140,7 +140,7 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do #[
[←s.goals.mapM Goal.toHtml] - +
] else #[] @@ -152,12 +152,12 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do [messages] [goals] - - + + def Text.toHtml (t : Text) : AlectryonM Html := t.contents.toHtml @@ -168,10 +168,10 @@ def Fragment.toHtml : Fragment → AlectryonM Html def baseHtml (content : Array Html) : AlectryonM Html := do let banner :=
- Built with doc-gen4, running Lean4. - Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. - Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. - On Mac, use Cmd instead of Ctrl. + Built with doc-gen4, running Lean4. + Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. + Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. + On Mac, use Cmd instead of Ctrl.
pure diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index b23cc6f..9053b09 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -183,13 +183,13 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do match t with | TaggedText.text t => let (front, t, back) := splitWhitespaces $ Html.escape t - let elem := Html.element "a" true #[("href", ←declNameToLink name)] #[t] + let elem := {t} pure #[Html.text front, elem, Html.text back] | _ => -- TODO: Is this ever reachable? - pure #[Html.element "a" true #[("href", ←declNameToLink name)] (←infoFormatToHtml t)] + pure #[[←infoFormatToHtml t]] | _ => - pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] - | _ => pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] + pure #[[←infoFormatToHtml t]] + | _ => pure #[[←infoFormatToHtml t]] end DocGen4.Output diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 8b1a3d4..86d8fba 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -35,7 +35,7 @@ def argToHtml (arg : Arg) : HtmlM Html := do let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "] nodes := nodes.append (←infoFormatToHtml arg.type) nodes := nodes.push r - let inner := Html.element "span" true #[("class", "fn")] nodes + let inner := [nodes] let html := Html.element "span" false #[("class", "decl_args")] #[inner] if implicit then pure {html} @@ -53,7 +53,7 @@ def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do let mut parents := #[] for parent in s.parents do let link ← declNameToHtmlBreakWithinLink parent - let inner := Html.element "span" true #[("class", "fn")] #[link] + let inner := {link} let html:= Html.element "span" false #[("class", "decl_parent")] #[inner] parents := parents.push html nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray @@ -65,7 +65,7 @@ and name. -/ def docInfoHeader (doc : DocInfo) : HtmlM Html := do let mut nodes := #[] - nodes := nodes.push {doc.getKindDescription} + nodes := nodes.push $ Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription] nodes := nodes.push @@ -82,7 +82,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do | _ => nodes := nodes nodes := nodes.push : - nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType) + nodes := nodes.push
[←infoFormatToHtml doc.getType]
pure
[nodes]
/-- diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index bec70af..0c75103 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -29,15 +29,15 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let dirNodes ← (dirs.mapM moduleListDir) let fileNodes ← (files.mapM moduleListFile) let moduleLink ← moduleNameToLink h.getName + let summary := + if (←getResult).moduleInfo.contains h.getName then + {←moduleToHtmlLink h.getName} + else + {h.getName.toString} + pure -
- { - if (←getResult).moduleInfo.contains h.getName then - Html.element "summary" true #[] #[←moduleToHtmlLink h.getName] - else - {h.getName.toString} - } +
+ {summary} [dirNodes] [fileNodes]
diff --git a/DocGen4/Output/ToHtmlFormat.lean b/DocGen4/Output/ToHtmlFormat.lean index 6120511..5a41a25 100644 --- a/DocGen4/Output/ToHtmlFormat.lean +++ b/DocGen4/Output/ToHtmlFormat.lean @@ -89,7 +89,6 @@ syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread syntax "<" rawIdent jsxAttr* "/>" : jsxElement syntax "<" rawIdent jsxAttr* ">" jsxChild* "" : jsxElement -syntax "<" rawIdent jsxAttr* ">" jsxChild* "" : jsxElement syntax jsxText : jsxChild syntax "{" term "}" : jsxChild @@ -135,9 +134,6 @@ macro_rules | `(<$n $attrs* />) => do `(Html.element $(quote (toString n.getId)) true $(← translateAttrs attrs) #[]) | `(<$n $attrs* >$children*) => do - let (tag, children) ← htmlHelper n children m - `(Html.element $(quote tag) false $(← translateAttrs attrs) $children) - | `(<$n $attrs* >$children*) => do let (tag, children) ← htmlHelper n children m `(Html.element $(quote tag) true $(← translateAttrs attrs) $children) diff --git a/Main.lean b/Main.lean index 686e0c9..e354975 100644 --- a/Main.lean +++ b/Main.lean @@ -5,7 +5,6 @@ import Cli open DocGen4 Lean Cli def runDocGenCmd (p : Parsed) : IO UInt32 := do - IO.println s!"{p}" let modules : List String := p.variableArgsAs! String |>.toList let res ← lakeSetup modules match res with