From 8da2e2a63dc23add4d2dc3ebfdf2837f6166a2f8 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Tue, 15 Feb 2022 19:27:12 +0800 Subject: [PATCH 01/22] feat: basic docstring support --- DocGen4/Output/Definition.lean | 14 +++++++++----- DocGen4/Output/Inductive.lean | 7 ++++++- DocGen4/Output/Structure.lean | 22 +++++++++++++--------- lakefile.lean | 6 ++++++ 4 files changed, 34 insertions(+), 15 deletions(-) diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index 64813d4..273d765 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -1,3 +1,4 @@ +import CMark import DocGen4.Output.Template namespace DocGen4 @@ -23,11 +24,14 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do pure none def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do - let equationsHtml ← equationsToHtml i - if let some equationsHtml := equationsHtml then - pure #[equationsHtml] - else - pure #[] + let equationsHtml? ← equationsToHtml i + let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s) + match equationsHtml?, docstringHtml? with + | some e, some d => pure #[e, d] + | some e, none => pure #[e] + | none , some e => pure #[e] + | none , none => pure #[] + end Output end DocGen4 diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index d8f84df..43f61dd 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -1,3 +1,4 @@ +import CMark import DocGen4.Output.Template namespace DocGen4 @@ -11,7 +12,11 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do pure
  • {shortName} : [←infoFormatToHtml i.type]
    • def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do - pure #[] + let constructorsHtml := + let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s) + match docstringHtml? with + | some d => pure #[constructorsHtml, d] + | none => pure #[constructorsHtml] end Output end DocGen4 diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index 23212ae..4b8a330 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -1,3 +1,4 @@ +import CMark import DocGen4.Output.Template namespace DocGen4 @@ -12,21 +13,24 @@ def fieldToHtml (f : NameInfo) : HtmlM Html := do pure
  • {s!"{shortName} "} : [←infoFormatToHtml f.type]
    • def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do - if Name.isSuffixOf `mk i.ctor.name then - pure #[ - ) + let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s) + match docstringHtml? with + | some d => pure #[structureHtml, d] + | none => pure #[structureHtml] end Output end DocGen4 diff --git a/lakefile.lean b/lakefile.lean index 2f747bb..77e34d7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,4 +4,10 @@ open Lake DSL package «doc-gen4» { -- add configuration options here supportInterpreter := true + dependencies := #[ + { + name := `CMark + src := Source.git "https://github.com/xubaiw/CMark.lean" "925f2ab" + } + ] } From 385a38a0036ef54f54e8f0cd7ff74ca404fe8392 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Wed, 16 Feb 2022 01:06:46 +0800 Subject: [PATCH 02/22] feat: basic mod doc without attributes --- DocGen4/Output.lean | 2 +- DocGen4/Output/Module.lean | 16 +++++++++++-- DocGen4/Process.lean | 49 ++++++++++++++++++++++++++++---------- 3 files changed, 51 insertions(+), 16 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index e8cb33f..1cc370d 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -71,7 +71,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let mut declList := #[] for (_, mod) in result.moduleInfo.toArray do - for decl in mod.members do + for decl in mod.members.filter ModuleMember.isDocInfo do let findHtml := ReaderT.run (findRedirectHtml decl.getName) config let findDir := basePath / "find" / decl.getName.toString FS.createDirAll findDir diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index eef3186..c6b0d76 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Henrik Böving. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +import CMark import DocGen4.Output.Template import DocGen4.Output.Inductive import DocGen4.Output.Structure @@ -101,6 +102,17 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do +def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do + pure +
    + {Html.text (CMark.renderHtml mdoc.doc)} +
    + +def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := + match member with + | ModuleMember.docInfo d => docInfoToHtml module d + | ModuleMember.modDoc d => modDocToHtml module d + def declarationToNavLink (module : Name) : Html :=
    {module.toString} @@ -162,9 +174,9 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do - let docInfos ← module.members.mapM (λ i => docInfoToHtml module.name i) + let docInfos ← module.members.mapM (λ i => moduleMemberToHtml module.name i) templateExtends (baseHtmlArray module.name.toString) $ pure #[ - ←internalNav (module.members.map DocInfo.getName) module.name, + ←internalNav (module.members.filter ModuleMember.isDocInfo |>.map ModuleMember.getName) module.name, Html.element "main" false #[] docInfos ] diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 17f981c..89feadb 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -101,16 +101,17 @@ def getDeclarationRange : DocInfo → DeclarationRange | classInfo i => i.declarationRange | classInductiveInfo i => i.declarationRange -def lineOrder (l r : DocInfo) : Bool := - l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line - end DocInfo +inductive ModuleMember where +| docInfo (info : DocInfo) : ModuleMember +| modDoc (doc : ModuleDoc) : ModuleMember +deriving Inhabited + structure Module where name : Name - doc : Option String -- Sorted according to their line numbers - members : Array DocInfo + members : Array ModuleMember deriving Inhabited partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) := @@ -459,6 +460,29 @@ def getDocString : DocInfo → Option String end DocInfo +namespace ModuleMember + +def getDeclarationRange : ModuleMember → DeclarationRange +| docInfo i => i.getDeclarationRange +| modDoc i => i.declarationRange + +def order (l r : ModuleMember) : Bool := + Position.lt l.getDeclarationRange.pos r.getDeclarationRange.pos + +def isDocInfo : ModuleMember → Bool +| docInfo _ => true +| _ => false + +def getName : ModuleMember → Name +| docInfo i => i.getName +| modDoc i => Name.anonymous + +def getDocString : ModuleMember → Option String +| docInfo i => i.getDocString +| modDoc i => i.doc + +end ModuleMember + structure AnalyzerResult where name2ModIdx : HashMap Name ModuleIdx moduleNames : Array Name @@ -472,13 +496,12 @@ def process : MetaM AnalyzerResult := do let env ← getEnv let mut res := mkHashMap env.header.moduleNames.size for module in env.header.moduleNames do - -- TODO: Check why modules can have multiple doc strings and add that later on - let moduleDoc := match getModuleDoc? env module with - | none => none - | some #[] => none - | some doc => doc.get! 0 + let modDocs := match getModuleDoc? env module with + | none => #[] + | some ds => ds + |>.map (λ doc => ModuleMember.modDoc doc) - res := res.insert module (Module.mk module moduleDoc #[]) + res := res.insert module (Module.mk module modDocs) for cinfo in env.constants.toList do try @@ -487,7 +510,7 @@ def process : MetaM AnalyzerResult := do let some modidx := env.getModuleIdxFor? dinfo.getName | unreachable! let moduleName := env.allImportedModuleNames.get! modidx let module := res.find! moduleName - res := res.insert moduleName {module with members := module.members.push dinfo} + res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)} catch e => IO.println s!"WARNING: Failed to obtain information for: {cinfo.fst}: {←e.toMessageData.toString}" @@ -495,7 +518,7 @@ def process : MetaM AnalyzerResult := do let mut adj := Array.mkArray res.size (Array.mkArray res.size false) -- TODO: This could probably be faster if we did an insertion sort above instead for (moduleName, module) in res.toArray do - res := res.insert moduleName {module with members := module.members.qsort DocInfo.lineOrder} + res := res.insert moduleName {module with members := module.members.qsort ModuleMember.order} let some modIdx := env.getModuleIdx? moduleName | unreachable! let moduleData := env.header.moduleData.get! modIdx for imp in moduleData.imports do From d3ce268d6391d8cff2d7c6a174f7662e735972f8 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Wed, 16 Feb 2022 02:19:40 +0800 Subject: [PATCH 03/22] feat: mod doc heading attributes --- DocGen4/Output/Module.lean | 33 ++++++++++++++++++++++++++++++++- 1 file changed, 32 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index c6b0d76..b218d3e 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -11,6 +11,7 @@ import DocGen4.Output.Class import DocGen4.Output.Definition import DocGen4.Output.Instance import DocGen4.Output.ClassInductive +import Lean.Data.Xml.Parser namespace DocGen4 namespace Output @@ -102,11 +103,41 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
    +open Xml in +partial def addAttributes : Element → Element +| (Element.Element name attrs contents) => + if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then + let id := "".intercalate (contents.map toString).toList + |>.dropWhile (λ c => !(c.isAlphanum ∨ c = '-')) + |>.toLower + |>.replace " " "-" + let anchorAttributes := Std.RBMap.empty + |>.insert "class" "hover-link" + |>.insert "href" s!"#{id}" + let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"] + let newAttrs := attrs + |>.insert "id" id + |>.insert "class" "markdown-heading" + let newContents := contents.map (λ c => match c with + | Content.Element e => Content.Element (addAttributes e) + | _ => c) + |>.push (Content.Element anchor) + ⟨ name, newAttrs, newContents⟩ + else + let newContents := contents.map λ c => match c with + | Content.Element e => Content.Element (addAttributes e) + | _ => c + ⟨ name, attrs, newContents⟩ + def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do - pure + let rendered := toString
    {Html.text (CMark.renderHtml mdoc.doc)}
    + let modified := match Lean.Xml.parse rendered with + | Except.ok parsed => toString $ addAttributes parsed + | _ => rendered + pure (Html.text modified) def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := match member with From 5679be6bbce5093dd3b305b74d68ed3b7ceca773 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Thu, 17 Feb 2022 08:54:06 +0800 Subject: [PATCH 04/22] chore: bump lean version update cmark version --- lakefile.lean | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 77e34d7..ba2f386 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,7 @@ package «doc-gen4» { dependencies := #[ { name := `CMark - src := Source.git "https://github.com/xubaiw/CMark.lean" "925f2ab" + src := Source.git "https://github.com/xubaiw/CMark.lean" "0c59e4f" } ] } diff --git a/lean-toolchain b/lean-toolchain index 4b598af..7c2b6c2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-02-11 +leanprover/lean4:nightly-2022-02-17 From b7c6a98969cf8fcc56218cec3458fcb96b05b664 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Thu, 17 Feb 2022 13:47:38 +0800 Subject: [PATCH 05/22] refactor: separate docstring code --- DocGen4/Output/Definition.lean | 4 +-- DocGen4/Output/DocString.lean | 49 ++++++++++++++++++++++++++++++++++ DocGen4/Output/Inductive.lean | 4 +-- DocGen4/Output/Module.lean | 36 +++---------------------- DocGen4/Output/Structure.lean | 4 +-- 5 files changed, 58 insertions(+), 39 deletions(-) create mode 100644 DocGen4/Output/DocString.lean diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index 273d765..aa0e255 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -1,5 +1,5 @@ -import CMark import DocGen4.Output.Template +import DocGen4.Output.DocString namespace DocGen4 namespace Output @@ -25,7 +25,7 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do let equationsHtml? ← equationsToHtml i - let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s) + let docstringHtml? := i.doc.map docStringToHtml match equationsHtml?, docstringHtml? with | some e, some d => pure #[e, d] | some e, none => pure #[e] diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean new file mode 100644 index 0000000..0bf6683 --- /dev/null +++ b/DocGen4/Output/DocString.lean @@ -0,0 +1,49 @@ +import CMark +import DocGen4.Output.Template +import Lean.Data.Parsec + +open Lean + +namespace DocGen4 +namespace Output + +open Xml Parser Lean Parsec + +def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof + +partial def addAttributes : Element → Element +| (Element.Element name attrs contents) => + -- heading only + if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then + let id := "".intercalate (contents.map toString).toList + |>.dropWhile (λ c => !(c.isAlphanum ∨ c = '-')) + |>.toLower + |>.replace " " "-" + let anchorAttributes := Std.RBMap.empty + |>.insert "class" "hover-link" + |>.insert "href" s!"#{id}" + let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"] + let newAttrs := attrs + |>.insert "id" id + |>.insert "class" "markdown-heading" + let newContents := + contents.map (λ c => match c with + | Content.Element e => Content.Element (addAttributes e) + | _ => c) + |>.push (Content.Element anchor) + ⟨ name, newAttrs, newContents⟩ + else + let newContents := contents.map λ c => match c with + | Content.Element e => Content.Element (addAttributes e) + | _ => c + ⟨ name, attrs, newContents ⟩ + +def docStringToHtml (s : String) : Html := + let rendered := CMark.renderHtml s + let attributed := match manyDocument rendered.mkIterator with + | Parsec.ParseResult.success _ res => "".intercalate (res.map addAttributes |>.map toString).toList + | _ => rendered + Html.text attributed + +end Output +end DocGen4 diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index 43f61dd..490c127 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -1,5 +1,5 @@ -import CMark import DocGen4.Output.Template +import DocGen4.Output.DocString namespace DocGen4 namespace Output @@ -13,7 +13,7 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do let constructorsHtml :=
      [← i.ctors.toArray.mapM ctorToHtml]
    - let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s) + let docstringHtml? := i.doc.map docStringToHtml match docstringHtml? with | some d => pure #[constructorsHtml, d] | none => pure #[constructorsHtml] diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index b218d3e..397a31f 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -3,7 +3,6 @@ Copyright (c) 2021 Henrik Böving. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import CMark import DocGen4.Output.Template import DocGen4.Output.Inductive import DocGen4.Output.Structure @@ -11,6 +10,7 @@ import DocGen4.Output.Class import DocGen4.Output.Definition import DocGen4.Output.Instance import DocGen4.Output.ClassInductive +import DocGen4.Output.DocString import Lean.Data.Xml.Parser namespace DocGen4 @@ -103,41 +103,11 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do -open Xml in -partial def addAttributes : Element → Element -| (Element.Element name attrs contents) => - if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then - let id := "".intercalate (contents.map toString).toList - |>.dropWhile (λ c => !(c.isAlphanum ∨ c = '-')) - |>.toLower - |>.replace " " "-" - let anchorAttributes := Std.RBMap.empty - |>.insert "class" "hover-link" - |>.insert "href" s!"#{id}" - let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"] - let newAttrs := attrs - |>.insert "id" id - |>.insert "class" "markdown-heading" - let newContents := contents.map (λ c => match c with - | Content.Element e => Content.Element (addAttributes e) - | _ => c) - |>.push (Content.Element anchor) - ⟨ name, newAttrs, newContents⟩ - else - let newContents := contents.map λ c => match c with - | Content.Element e => Content.Element (addAttributes e) - | _ => c - ⟨ name, attrs, newContents⟩ - def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do - let rendered := toString + pure
    - {Html.text (CMark.renderHtml mdoc.doc)} + {docStringToHtml mdoc.doc}
    - let modified := match Lean.Xml.parse rendered with - | Except.ok parsed => toString $ addAttributes parsed - | _ => rendered - pure (Html.text modified) def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := match member with diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index 4b8a330..abce904 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -1,5 +1,5 @@ -import CMark import DocGen4.Output.Template +import DocGen4.Output.DocString namespace DocGen4 namespace Output @@ -27,7 +27,7 @@ def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
  • )
    • ) - let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s) + let docstringHtml? := i.doc.map docStringToHtml match docstringHtml? with | some d => pure #[structureHtml, d] | none => pure #[structureHtml] From 5790172eab2a45bb4c98fbf463c7d175876b588c Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Thu, 17 Feb 2022 13:53:29 +0800 Subject: [PATCH 06/22] fix: doc string for all DocInfo --- DocGen4/Output/Module.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 397a31f..9200498 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -81,7 +81,9 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do | DocInfo.definitionInfo i => definitionToHtml i | DocInfo.instanceInfo i => instanceToHtml i | DocInfo.classInductiveInfo i => classInductiveToHtml i - | _ => pure #[] + | i => match i.getDocString with + | some d => pure #[docStringToHtml d] + | _ => pure #[] let attrs := doc.getAttrs let attrsHtml := From 1729f4aa71cc41b74c610fb42709e28bc2e1cbfa Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Thu, 17 Feb 2022 15:26:17 +0800 Subject: [PATCH 07/22] fix: fix docstring heading id --- DocGen4/Output/DocString.lean | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 0bf6683..98b2a2c 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -11,14 +11,28 @@ open Xml Parser Lean Parsec def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof -partial def addAttributes : Element → Element +partial def elementToPlainText : Xml.Element → String | (Element.Element name attrs contents) => + "".intercalate (contents.toList.map contentToPlainText) + where + contentToPlainText c := match c with + | Content.Element el => elementToPlainText el + | Content.Comment _ => "" + | Content.Character s => s + +def dropAllCharWhile (s : String) (p : Char → Bool) : String := + ⟨ s.data.filter p ⟩ + +def textToIdAttribute (s : String) : String := + dropAllCharWhile s (λ c => (c.isAlphanum ∨ c = '-' ∨ c = ' ')) + |>.toLower + |>.replace " " "-" + +partial def addAttributes : Element → Element +| el@(Element.Element name attrs contents) => -- heading only if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then - let id := "".intercalate (contents.map toString).toList - |>.dropWhile (λ c => !(c.isAlphanum ∨ c = '-')) - |>.toLower - |>.replace " " "-" + let id := textToIdAttribute (elementToPlainText el) let anchorAttributes := Std.RBMap.empty |>.insert "class" "hover-link" |>.insert "href" s!"#{id}" From 97ddf05ab6f478267f090ebfc93798766f1eac2a Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Thu, 17 Feb 2022 21:26:02 +0800 Subject: [PATCH 08/22] fix: add root to relative href --- DocGen4/Output/Definition.lean | 6 ++--- DocGen4/Output/DocString.lean | 49 ++++++++++++++++++++++------------ DocGen4/Output/Inductive.lean | 4 +-- DocGen4/Output/Module.lean | 4 +-- DocGen4/Output/Structure.lean | 4 +-- 5 files changed, 41 insertions(+), 26 deletions(-) diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index aa0e255..374c10c 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -25,11 +25,11 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do let equationsHtml? ← equationsToHtml i - let docstringHtml? := i.doc.map docStringToHtml + let docstringHtml? ← i.doc.mapM docStringToHtml match equationsHtml?, docstringHtml? with - | some e, some d => pure #[e, d] + | some e, some d => pure (#[e] ++ d) | some e, none => pure #[e] - | none , some e => pure #[e] + | none , some d => pure d | none , none => pure #[] diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 98b2a2c..c66fa4f 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -28,9 +28,15 @@ def textToIdAttribute (s : String) : String := |>.toLower |>.replace " " "-" -partial def addAttributes : Element → Element -| el@(Element.Element name attrs contents) => - -- heading only +def extendRelativeLink (link : String) (root : String) : String := + -- HACK: better way to detect absolute links + if link.startsWith "http" then + link + else root ++ link + +partial def addAttributes : Element → HtmlM Element +| el@(Element.Element name attrs contents) => do + -- add id and class to if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then let id := textToIdAttribute (elementToPlainText el) let anchorAttributes := Std.RBMap.empty @@ -40,24 +46,33 @@ partial def addAttributes : Element → Element let newAttrs := attrs |>.insert "id" id |>.insert "class" "markdown-heading" - let newContents := - contents.map (λ c => match c with - | Content.Element e => Content.Element (addAttributes e) - | _ => c) + let newContents := (← + contents.mapM (λ c => match c with + | Content.Element e => (addAttributes e).map (Content.Element) + | _ => pure c)) |>.push (Content.Element anchor) - ⟨ name, newAttrs, newContents⟩ + pure ⟨ name, newAttrs, newContents⟩ + -- extend relative href for + else if name = "a" then + let root ← getRoot + let newAttrs := match attrs.find? "href" with + | some href => attrs.insert "href" (extendRelativeLink href root) + | none => attrs + pure ⟨ name, newAttrs, contents⟩ + -- recursively modify else - let newContents := contents.map λ c => match c with - | Content.Element e => Content.Element (addAttributes e) - | _ => c - ⟨ name, attrs, newContents ⟩ + let newContents ← contents.mapM λ c => match c with + | Content.Element e => (addAttributes e).map Content.Element + | _ => pure c + pure ⟨ name, attrs, newContents ⟩ -def docStringToHtml (s : String) : Html := +def docStringToHtml (s : String) : HtmlM (Array Html) := do let rendered := CMark.renderHtml s - let attributed := match manyDocument rendered.mkIterator with - | Parsec.ParseResult.success _ res => "".intercalate (res.map addAttributes |>.map toString).toList - | _ => rendered - Html.text attributed + match manyDocument rendered.mkIterator with + | Parsec.ParseResult.success _ res => + res.mapM λ x => do + pure (Html.text $ toString (← addAttributes x)) + | _ => pure #[Html.text rendered] end Output end DocGen4 diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index 490c127..5535290 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -13,9 +13,9 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do let constructorsHtml :=
      [← i.ctors.toArray.mapM ctorToHtml]
    - let docstringHtml? := i.doc.map docStringToHtml + let docstringHtml? ← i.doc.mapM docStringToHtml match docstringHtml? with - | some d => pure #[constructorsHtml, d] + | some d => pure (#[constructorsHtml] ++ d) | none => pure #[constructorsHtml] end Output diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 9200498..394c509 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -82,7 +82,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do | DocInfo.instanceInfo i => instanceToHtml i | DocInfo.classInductiveInfo i => classInductiveToHtml i | i => match i.getDocString with - | some d => pure #[docStringToHtml d] + | some d => pure (← docStringToHtml d) | _ => pure #[] let attrs := doc.getAttrs @@ -108,7 +108,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do pure
    - {docStringToHtml mdoc.doc} + [←docStringToHtml mdoc.doc]
    def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index abce904..ab6e4d5 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -27,9 +27,9 @@ def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
  • )
    • ) - let docstringHtml? := i.doc.map docStringToHtml + let docstringHtml? ← i.doc.mapM docStringToHtml match docstringHtml? with - | some d => pure #[structureHtml, d] + | some d => pure (#[structureHtml] ++ d) | none => pure #[structureHtml] end Output From 11bb2af57aa47e371432842c3b2510622739de99 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 00:46:02 +0800 Subject: [PATCH 09/22] feat: add auto link --- DocGen4/Output/DocString.lean | 117 +++++++++++++++++++++++----------- 1 file changed, 80 insertions(+), 37 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index c66fa4f..66f5015 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -9,6 +9,8 @@ namespace Output open Xml Parser Lean Parsec +instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩ + def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof partial def elementToPlainText : Xml.Element → String @@ -28,50 +30,91 @@ def textToIdAttribute (s : String) : String := |>.toLower |>.replace " " "-" -def extendRelativeLink (link : String) (root : String) : String := - -- HACK: better way to detect absolute links - if link.startsWith "http" then - link - else root ++ link - -partial def addAttributes : Element → HtmlM Element -| el@(Element.Element name attrs contents) => do - -- add id and class to - if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then - let id := textToIdAttribute (elementToPlainText el) - let anchorAttributes := Std.RBMap.empty - |>.insert "class" "hover-link" - |>.insert "href" s!"#{id}" - let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"] - let newAttrs := attrs - |>.insert "id" id - |>.insert "class" "markdown-heading" - let newContents := (← - contents.mapM (λ c => match c with - | Content.Element e => (addAttributes e).map (Content.Element) - | _ => pure c)) - |>.push (Content.Element anchor) - pure ⟨ name, newAttrs, newContents⟩ - -- extend relative href for - else if name = "a" then - let root ← getRoot - let newAttrs := match attrs.find? "href" with - | some href => attrs.insert "href" (extendRelativeLink href root) - | none => attrs - pure ⟨ name, newAttrs, contents⟩ - -- recursively modify +def possibleNameToLink (s : String) : HtmlM (Option String) := do + let res ← getResult + let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous + if res.name2ModIdx.contains name then + declNameToLink name else - let newContents ← contents.mapM λ c => match c with - | Content.Element e => (addAttributes e).map Content.Element - | _ => pure c - pure ⟨ name, attrs, newContents ⟩ + match (← getCurrentName) with + | some currentName => + match (res.moduleInfo.find! currentName).members.find? (·.getName.toString.endsWith s) with + | some info => + declNameToLink info.getName + | _ => pure none + | _ => pure none + +def extendRelativeLink (s : String) : HtmlM String := do + -- for relative doc links + if s.startsWith "#" then + if let some link ← possibleNameToLink (s.drop 1) then + pure link + else + pure s + -- for absolute and relative urls + else if s.startsWith "http" then + pure s + else pure ((←getRoot) ++ s) + +def possibleNameToAnchor (s : String) : HtmlM Content := do + let link? ← possibleNameToLink s + match link? with + | some link => + let res ← getResult + let attributes := Std.RBMap.empty.insert "href" link + pure $ Content.Element $ Element.Element "a" attributes #[Content.Character s] + | none => pure $ Content.Character s + +partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM Element := + match element with + | el@(Element.Element name attrs contents) => do + -- add id and class to + if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then + let id := textToIdAttribute (elementToPlainText el) + let anchorAttributes := Std.RBMap.empty + |>.insert "class" "hover-link" + |>.insert "href" s!"#{id}" + let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"] + let newAttrs := attrs + |>.insert "id" id + |>.insert "class" "markdown-heading" + let newContents := (← + contents.mapM (λ c => match c with + | Content.Element e => (modifyElement e).map (Content.Element) + | _ => pure c)) + |>.push (Content.Character " ") + |>.push (Content.Element anchor) + pure ⟨ name, newAttrs, newContents⟩ + -- extend relative href for + else if name = "a" then + let root ← getRoot + let newAttrs ← match (attrs.find? "href").map (extendRelativeLink) with + | some href => href.map (attrs.insert "href") + | none => pure attrs + pure ⟨ name, newAttrs, contents⟩ + -- auto link for inline + else if name = "code" then + let mut newContents := #[] + for c in contents do + match c with + | Content.Character s => + newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor) + | _ => newContents := newContents.push c + pure ⟨ name, attrs, newContents⟩ + -- recursively modify + else + let newContents ← contents.mapM λ c => match c with + -- disable auto link for code blocks + | Content.Element e => (modifyElement e (name ≠ "pre")).map Content.Element + | _ => pure c + pure ⟨ name, attrs, newContents ⟩ def docStringToHtml (s : String) : HtmlM (Array Html) := do let rendered := CMark.renderHtml s match manyDocument rendered.mkIterator with | Parsec.ParseResult.success _ res => res.mapM λ x => do - pure (Html.text $ toString (← addAttributes x)) + pure (Html.text $ toString (← modifyElement x)) | _ => pure #[Html.text rendered] end Output From 0b9a9f0bdc96911996aa7f1ccf133e53d8a62287 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 01:39:02 +0800 Subject: [PATCH 10/22] fix: remove intra link in code block --- DocGen4/Output/DocString.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 66f5015..f7005cf 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -33,8 +33,10 @@ def textToIdAttribute (s : String) : String := def possibleNameToLink (s : String) : HtmlM (Option String) := do let res ← getResult let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous + -- with exactly the same name if res.name2ModIdx.contains name then declNameToLink name + -- find similar name in the same module else match (← getCurrentName) with | some currentName => @@ -52,7 +54,7 @@ def extendRelativeLink (s : String) : HtmlM String := do else pure s -- for absolute and relative urls - else if s.startsWith "http" then + else if s.startsWith "http" then pure s else pure ((←getRoot) ++ s) @@ -93,7 +95,7 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM | none => pure attrs pure ⟨ name, newAttrs, contents⟩ -- auto link for inline - else if name = "code" then + else if name = "code" ∧ linkCode then let mut newContents := #[] for c in contents do match c with From 89f5951f2ddfb2be1789e7a51d3bf74d2f1c0193 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 03:10:48 +0800 Subject: [PATCH 11/22] feat: add mathjax equation support --- DocGen4/Output/Template.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index b44aa81..cd6509e 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -50,6 +50,9 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do -- TODO Add more js stuff + -- mathjax + + From 9550d1c92ea518463da25468df8dffeacbbff433 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 03:26:38 +0800 Subject: [PATCH 12/22] refactor: use ## for intra doc --- DocGen4/Output/DocString.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index f7005cf..70e6b0d 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -47,12 +47,15 @@ def possibleNameToLink (s : String) : HtmlM (Option String) := do | _ => pure none def extendRelativeLink (s : String) : HtmlM String := do - -- for relative doc links - if s.startsWith "#" then - if let some link ← possibleNameToLink (s.drop 1) then + -- for intra doc links + if s.startsWith "##" then + if let some link ← possibleNameToLink (s.drop 2) then pure link else - pure s + panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported" + -- for id + else if s.startsWith "#" then + pure s -- for absolute and relative urls else if s.startsWith "http" then pure s From 5dc3ab855f16383d809fb925301e27d8fc5d45d5 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 03:27:00 +0800 Subject: [PATCH 13/22] feat: config mathjax like doc-gen --- DocGen4/Output.lean | 1 + DocGen4/Output/Base.lean | 1 + DocGen4/Output/Template.lean | 1 + static/mathjax-config.js | 17 +++++++++++++++++ 4 files changed, 20 insertions(+) create mode 100644 static/mathjax-config.js diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 1cc370d..734bb34 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -86,6 +86,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do FS.writeFile (basePath / "404.html") notFoundHtml.toString FS.writeFile (basePath / "nav.js") navJs FS.writeFile (basePath / "search.js") searchJs + FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs for (module, content) in result.moduleInfo.toArray do let moduleHtml := ReaderT.run (moduleToHtml content) config let path := moduleNameToFile basePath module diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 485739b..4579f69 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -49,6 +49,7 @@ section Static def styleCss : String := include_str "./static/style.css" def navJs : String := include_str "./static/nav.js" def searchJs : String := include_str "./static/search.js" + def mathjaxConfigJs : String := include_str "./static/mathjax-config.js" end Static def declNameToLink (name : Name) : HtmlM String := do diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index cd6509e..8ed58ee 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -51,6 +51,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do -- mathjax + diff --git a/static/mathjax-config.js b/static/mathjax-config.js new file mode 100644 index 0000000..51adbd6 --- /dev/null +++ b/static/mathjax-config.js @@ -0,0 +1,17 @@ +MathJax = { + tex: { + inlineMath: [['$', '$']], + displayMath: [['$$', '$$']] + }, + options: { + skipHtmlTags: [ + 'script', 'noscript', 'style', 'textarea', 'pre', + 'code', 'annotation', 'annotation-xml', + 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name', + 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields', + 'constructor', 'constructors', 'instances' + ], + ignoreHtmlClass: 'tex2jax_ignore', + processHtmlClass: 'tex2jax_process', + }, +}; \ No newline at end of file From cce4285c96349ebab7dcffe95ba9f4631bb00f9c Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 04:01:31 +0800 Subject: [PATCH 14/22] fix: intersperse code contents --- DocGen4/Output/DocString.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 70e6b0d..d318752 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -103,7 +103,7 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM for c in contents do match c with | Content.Character s => - newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor) + newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor).intersperse (Content.Character " ") | _ => newContents := newContents.push c pure ⟨ name, attrs, newContents⟩ -- recursively modify From d8a5f52c101ac89c3445e028a5475752b64d52b6 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 11:28:44 +0800 Subject: [PATCH 15/22] fix: fix docstring order --- DocGen4/Output/Definition.lean | 9 +++------ DocGen4/Output/Inductive.lean | 5 +---- DocGen4/Output/Module.lean | 15 ++++++++------- DocGen4/Output/Structure.lean | 5 +---- 4 files changed, 13 insertions(+), 21 deletions(-) diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index 374c10c..7261c37 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -25,12 +25,9 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do let equationsHtml? ← equationsToHtml i - let docstringHtml? ← i.doc.mapM docStringToHtml - match equationsHtml?, docstringHtml? with - | some e, some d => pure (#[e] ++ d) - | some e, none => pure #[e] - | none , some d => pure d - | none , none => pure #[] + match equationsHtml? with + | some e => pure #[e] + | none => pure #[] end Output diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index 5535290..ab29718 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -13,10 +13,7 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do let constructorsHtml :=
      [← i.ctors.toArray.mapM ctorToHtml]
    - let docstringHtml? ← i.doc.mapM docStringToHtml - match docstringHtml? with - | some d => pure (#[constructorsHtml] ++ d) - | none => pure #[constructorsHtml] + pure #[constructorsHtml] end Output end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 394c509..5d41123 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -74,17 +74,17 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do pure
    [nodes]
    def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do - let docHtml ← match doc with + let docInfoHtml ← match doc with | DocInfo.inductiveInfo i => inductiveToHtml i | DocInfo.structureInfo i => structureToHtml i | DocInfo.classInfo i => classToHtml i | DocInfo.definitionInfo i => definitionToHtml i | DocInfo.instanceInfo i => instanceToHtml i | DocInfo.classInductiveInfo i => classInductiveToHtml i - | i => match i.getDocString with - | some d => pure (← docStringToHtml d) - | _ => pure #[] - + | i => pure #[] + let docStringHtml ← match doc.getDocString with + | some s => docStringToHtml s + | none => pure #[] let attrs := doc.getAttrs let attrsHtml := if attrs.size > 0 then @@ -101,7 +101,8 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do [attrsHtml] {←docInfoHeader doc} - [docHtml] + [docStringHtml] + [docInfoHtml] @@ -111,7 +112,7 @@ def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do [←docStringToHtml mdoc.doc] -def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := +def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do match member with | ModuleMember.docInfo d => docInfoToHtml module d | ModuleMember.modDoc d => modDocToHtml module d diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index ab6e4d5..fb6105d 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -27,10 +27,7 @@ def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
  • )
    • ) - let docstringHtml? ← i.doc.mapM docStringToHtml - match docstringHtml? with - | some d => pure (#[structureHtml] ++ d) - | none => pure #[structureHtml] + pure #[structureHtml] end Output end DocGen4 From 3687b3466a702f602e9f9f1777cab549ac2d3ca9 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 12:52:01 +0800 Subject: [PATCH 16/22] refactor: clean up docstring module --- DocGen4/Output.lean | 2 +- DocGen4/Output/Module.lean | 7 ++++--- DocGen4/Process.lean | 11 +++++++---- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 734bb34..fc13f4e 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -71,7 +71,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let mut declList := #[] for (_, mod) in result.moduleInfo.toArray do - for decl in mod.members.filter ModuleMember.isDocInfo do + for decl in filterMapDocInfo mod.members do let findHtml := ReaderT.run (findRedirectHtml decl.getName) config let findDir := basePath / "find" / decl.getName.toString FS.createDirAll findDir diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 5d41123..4c76230 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -178,10 +178,11 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do - let docInfos ← module.members.mapM (λ i => moduleMemberToHtml module.name i) + let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i) + let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName templateExtends (baseHtmlArray module.name.toString) $ pure #[ - ←internalNav (module.members.filter ModuleMember.isDocInfo |>.map ModuleMember.getName) module.name, - Html.element "main" false #[] docInfos + ←internalNav memberNames module.name, + Html.element "main" false #[] memberDocs ] end Output diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 0647fb9..6de8304 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -461,10 +461,6 @@ def getDeclarationRange : ModuleMember → DeclarationRange def order (l r : ModuleMember) : Bool := Position.lt l.getDeclarationRange.pos r.getDeclarationRange.pos -def isDocInfo : ModuleMember → Bool -| docInfo _ => true -| _ => false - def getName : ModuleMember → Name | docInfo i => i.getName | modDoc i => Name.anonymous @@ -475,6 +471,13 @@ def getDocString : ModuleMember → Option String end ModuleMember +def filterMapDocInfo (ms : Array ModuleMember) : Array DocInfo := + ms.filterMap filter + where + filter : ModuleMember → Option DocInfo + | ModuleMember.docInfo i => some i + | _ => none + structure AnalyzerResult where name2ModIdx : HashMap Name ModuleIdx moduleNames : Array Name From 5e550c783396a9df550db7d753ea7b880a367abb Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 03:14:58 +0800 Subject: [PATCH 17/22] refactor: docstring between basic and extra info clean up code --- DocGen4/Output/Class.lean | 2 +- DocGen4/Output/ClassInductive.lean | 2 +- DocGen4/Output/Definition.lean | 14 +-- DocGen4/Output/DocString.lean | 147 +++++++++++++++++++---------- DocGen4/Output/Instance.lean | 2 - DocGen4/Output/Module.lean | 13 ++- lakefile.lean | 6 +- 7 files changed, 118 insertions(+), 68 deletions(-) diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean index 7f64cc0..00fd252 100644 --- a/DocGen4/Output/Class.lean +++ b/DocGen4/Output/Class.lean @@ -21,7 +21,7 @@ def classInstancesToHtml (instances : Array Name) : HtmlM Html := do def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do - pure $ (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances) + pure $ (←structureToHtml i.toStructureInfo) end Output end DocGen4 diff --git a/DocGen4/Output/ClassInductive.lean b/DocGen4/Output/ClassInductive.lean index 6113e73..140651e 100644 --- a/DocGen4/Output/ClassInductive.lean +++ b/DocGen4/Output/ClassInductive.lean @@ -7,7 +7,7 @@ namespace DocGen4 namespace Output def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do - pure $ (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances) + pure $ (←inductiveToHtml i.toInductiveInfo) end Output end DocGen4 diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index 7261c37..1152b53 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -10,25 +10,19 @@ open Lean Widget def equationToHtml (c : CodeWithInfos) : HtmlM Html := do pure
  • [←infoFormatToHtml c]
    • -def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do +def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do if let some eqs := i.equations then let equationsHtml ← eqs.mapM equationToHtml - pure + pure #[
    Equations
      [equationsHtml]
    + ] else - pure none - -def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do - let equationsHtml? ← equationsToHtml i - match equationsHtml? with - | some e => pure #[e] - | none => pure #[] - + pure #[] end Output end DocGen4 diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index d318752..7c933b0 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -1,8 +1,9 @@ import CMark import DocGen4.Output.Template import Lean.Data.Parsec +import Unicode.General.GeneralCategory -open Lean +open Lean Unicode namespace DocGen4 namespace Output @@ -11,26 +12,44 @@ open Xml Parser Lean Parsec instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩ +/-- Parse an array of Xml/Html document from String. -/ def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof -partial def elementToPlainText : Xml.Element → String -| (Element.Element name attrs contents) => - "".intercalate (contents.toList.map contentToPlainText) +/-- + Generate id for heading elements, with the following rules: + + 1. Characters in `letter`, `number` and `symbol` unicode categories are preserved. + 2. Any sequences of Characters in `mark`, `punctuation`, `separator` and `other` categories are replaced by a single dash. + 3. Cases (upper and lower) are preserved. + 4. Xml/Html tags are ignored. +-/ +partial def xmlGetHeadingId (el : Xml.Element) : String := + elementToPlainText el |> replaceCharSeq unicodeToDrop "-" where + elementToPlainText el := match el with + | (Element.Element name attrs contents) => + "".intercalate (contents.toList.map contentToPlainText) contentToPlainText c := match c with | Content.Element el => elementToPlainText el | Content.Comment _ => "" | Content.Character s => s + replaceCharSeq pattern replacement s := + s.split pattern + |>.filter (!·.isEmpty) + |> replacement.intercalate + unicodeToDrop char := + charInGeneralCategory char GeneralCategory.mark || + charInGeneralCategory char GeneralCategory.punctuation || + charInGeneralCategory char GeneralCategory.separator || + charInGeneralCategory char GeneralCategory.other -def dropAllCharWhile (s : String) (p : Char → Bool) : String := - ⟨ s.data.filter p ⟩ +/-- + This function try to find the given name, both globally and in current module. -def textToIdAttribute (s : String) : String := - dropAllCharWhile s (λ c => (c.isAlphanum ∨ c = '-' ∨ c = ' ')) - |>.toLower - |>.replace " " "-" - -def possibleNameToLink (s : String) : HtmlM (Option String) := do + For global search, a precise name is need. If the global search fails, the function + tries to find a local one that ends with the given search name. +-/ +def nameToLink? (s : String) : HtmlM (Option String) := do let res ← getResult let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous -- with exactly the same name @@ -46,10 +65,18 @@ def possibleNameToLink (s : String) : HtmlM (Option String) := do | _ => pure none | _ => pure none -def extendRelativeLink (s : String) : HtmlM String := do +/-- + Extend links with following rules: + + 1. if the link starts with `##`, a name search is used and will panic if not found + 2. if the link starts with `#`, it's treated as id link, no modification + 3. if the link starts with `http`, it's an absolute one, no modification + 4. otherwise it's a relative link, extend it with base url +-/ +def extendLink (s : String) : HtmlM String := do -- for intra doc links if s.startsWith "##" then - if let some link ← possibleNameToLink (s.drop 2) then + if let some link ← nameToLink? (s.drop 2) then pure link else panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported" @@ -61,51 +88,70 @@ def extendRelativeLink (s : String) : HtmlM String := do pure s else pure ((←getRoot) ++ s) -def possibleNameToAnchor (s : String) : HtmlM Content := do - let link? ← possibleNameToLink s - match link? with - | some link => - let res ← getResult - let attributes := Std.RBMap.empty.insert "href" link - pure $ Content.Element $ Element.Element "a" attributes #[Content.Character s] - | none => pure $ Content.Character s +/-- Add attributes for heading. -/ +def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do + match el with + | Element.Element name attrs contents => do + let id := xmlGetHeadingId el + let anchorAttributes := Std.RBMap.empty + |>.insert "class" "hover-link" + |>.insert "href" s!"#{id}" + let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"] + let newAttrs := attrs + |>.insert "id" id + |>.insert "class" "markdown-heading" + let newContents := (← + contents.mapM (λ c => match c with + | Content.Element e => (modifyElement e).map (Content.Element) + | _ => pure c)) + |>.push (Content.Character " ") + |>.push (Content.Element anchor) + pure ⟨ name, newAttrs, newContents⟩ +/-- Extend anchor links. -/ +def extendAnchor (el : Element) : HtmlM Element := do + match el with + | Element.Element name attrs contents => + let root ← getRoot + let newAttrs ← match (attrs.find? "href").map extendLink with + | some href => href.map (attrs.insert "href") + | none => pure attrs + pure ⟨ name, newAttrs, contents⟩ + +/-- Automatically add intra documentation link for inline code span. -/ +def autoLink (el : Element) : HtmlM Element := do + match el with + | Element.Element name attrs contents => + let mut newContents := #[] + for c in contents do + match c with + | Content.Character s => + newContents := newContents ++ (← s.splitOn.mapM linkify).intersperse (Content.Character " ") + | _ => newContents := newContents.push c + pure ⟨ name, attrs, newContents ⟩ + where + linkify s := do + let link? ← nameToLink? s + match link? with + | some link => + let res ← getResult + let attributes := Std.RBMap.empty.insert "href" link + pure $ Content.Element $ Element.Element "a" attributes #[Content.Character s] + | none => pure $ Content.Character s + +/-- Core function of modifying the cmark rendered docstring html. -/ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM Element := match element with | el@(Element.Element name attrs contents) => do -- add id and class to if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then - let id := textToIdAttribute (elementToPlainText el) - let anchorAttributes := Std.RBMap.empty - |>.insert "class" "hover-link" - |>.insert "href" s!"#{id}" - let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"] - let newAttrs := attrs - |>.insert "id" id - |>.insert "class" "markdown-heading" - let newContents := (← - contents.mapM (λ c => match c with - | Content.Element e => (modifyElement e).map (Content.Element) - | _ => pure c)) - |>.push (Content.Character " ") - |>.push (Content.Element anchor) - pure ⟨ name, newAttrs, newContents⟩ + addHeadingAttributes el modifyElement -- extend relative href for else if name = "a" then - let root ← getRoot - let newAttrs ← match (attrs.find? "href").map (extendRelativeLink) with - | some href => href.map (attrs.insert "href") - | none => pure attrs - pure ⟨ name, newAttrs, contents⟩ + extendAnchor el -- auto link for inline - else if name = "code" ∧ linkCode then - let mut newContents := #[] - for c in contents do - match c with - | Content.Character s => - newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor).intersperse (Content.Character " ") - | _ => newContents := newContents.push c - pure ⟨ name, attrs, newContents⟩ + else if name = "code" ∧ linkCode = true then + autoLink el -- recursively modify else let newContents ← contents.mapM λ c => match c with @@ -114,6 +160,7 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM | _ => pure c pure ⟨ name, attrs, newContents ⟩ +/-- Convert docstring to Html. -/ def docStringToHtml (s : String) : HtmlM (Array Html) := do let rendered := CMark.renderHtml s match manyDocument rendered.mkIterator with diff --git a/DocGen4/Output/Instance.lean b/DocGen4/Output/Instance.lean index bad10f1..78f098d 100644 --- a/DocGen4/Output/Instance.lean +++ b/DocGen4/Output/Instance.lean @@ -4,7 +4,5 @@ import DocGen4.Output.Definition namespace DocGen4 namespace Output -def instanceToHtml (i : InstanceInfo) : HtmlM (Array Html) := definitionToHtml i - end Output end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 4c76230..942051b 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -74,17 +74,23 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do pure
    [nodes]
    def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do + -- basic info like headers, types, structure fields, etc. let docInfoHtml ← match doc with | DocInfo.inductiveInfo i => inductiveToHtml i | DocInfo.structureInfo i => structureToHtml i | DocInfo.classInfo i => classToHtml i - | DocInfo.definitionInfo i => definitionToHtml i - | DocInfo.instanceInfo i => instanceToHtml i | DocInfo.classInductiveInfo i => classInductiveToHtml i | i => pure #[] + -- rendered doc stirng let docStringHtml ← match doc.getDocString with | some s => docStringToHtml s | none => pure #[] + -- extra information like equations and instances + let extraInfoHtml ← match doc with + | DocInfo.classInfo i => pure #[←classInstancesToHtml i.instances] + | DocInfo.definitionInfo i => equationsToHtml i + | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.instances] + | i => pure #[] let attrs := doc.getAttrs let attrsHtml := if attrs.size > 0 then @@ -101,8 +107,9 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do [attrsHtml] {←docInfoHeader doc} - [docStringHtml] [docInfoHtml] + [docStringHtml] + [extraInfoHtml] diff --git a/lakefile.lean b/lakefile.lean index ba2f386..d0af360 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,11 @@ package «doc-gen4» { dependencies := #[ { name := `CMark - src := Source.git "https://github.com/xubaiw/CMark.lean" "0c59e4f" + src := Source.git "https://github.com/xubaiw/CMark.lean" "0c59e4fa0f8864502dc9e661d437be842d29d708" + }, + { + name := `Unicode + src := Source.git "https://github.com/xubaiw/Unicode.lean" "88ad4aacfcc7ab941a22c54de3e4fef0809cda87" } ] } From 3acfc510b45e1caeb851fb5ecd302a2cdc4a657b Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 03:28:03 +0800 Subject: [PATCH 18/22] fix: no overmatch for intra link --- DocGen4/Output/DocString.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 7c933b0..4470c54 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -59,11 +59,19 @@ def nameToLink? (s : String) : HtmlM (Option String) := do else match (← getCurrentName) with | some currentName => - match (res.moduleInfo.find! currentName).members.find? (·.getName.toString.endsWith s) with + match (res.moduleInfo.find! currentName).members.find? (sameEnd ·.getName.toString s) with | some info => declNameToLink info.getName | _ => pure none | _ => pure none + where + sameEnd n1 n2 := Id.run do + let n1' := n1.splitOn "." |>.reverse + let n2' := n2.splitOn "." |>.reverse + for i in [0:n2'.length] do + if n1'.getD i "" = n2'.get! i then + return true + return false /-- Extend links with following rules: From 794923a997263e3c9445624e101bbfed4c104fcb Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 04:50:04 +0800 Subject: [PATCH 19/22] fix: update Unicode.lean --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index d0af360..cc8dd0e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,7 +11,7 @@ package «doc-gen4» { }, { name := `Unicode - src := Source.git "https://github.com/xubaiw/Unicode.lean" "88ad4aacfcc7ab941a22c54de3e4fef0809cda87" + src := Source.git "https://github.com/xubaiw/Unicode.lean" "3b7b85472d42854a474099928a3423bb97d4fa64" } ] } From 4c2d67cfca5b31940ed6fa6e90545d6cc8058073 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 05:03:44 +0800 Subject: [PATCH 20/22] fix: change same end maching --- DocGen4/Output/DocString.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 4470c54..80cad95 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -65,13 +65,10 @@ def nameToLink? (s : String) : HtmlM (Option String) := do | _ => pure none | _ => pure none where - sameEnd n1 n2 := Id.run do - let n1' := n1.splitOn "." |>.reverse - let n2' := n2.splitOn "." |>.reverse - for i in [0:n2'.length] do - if n1'.getD i "" = n2'.get! i then - return true - return false + sameEnd n1 n2 := + n1.endsWith n2 || + (n2.endsWith (n1.splitOn ".").getLast!) + /-- Extend links with following rules: From ad4d77a9c9b3f8ff4da0a8d640e25b68f1af41c1 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 05:03:44 +0800 Subject: [PATCH 21/22] fix: change same end maching --- DocGen4/Output/DocString.lean | 41 ++++++++++++++++------------------- 1 file changed, 19 insertions(+), 22 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 4470c54..7e8ae54 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -3,13 +3,11 @@ import DocGen4.Output.Template import Lean.Data.Parsec import Unicode.General.GeneralCategory -open Lean Unicode +open Lean Unicode Xml Parser Parsec namespace DocGen4 namespace Output -open Xml Parser Lean Parsec - instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩ /-- Parse an array of Xml/Html document from String. -/ @@ -51,27 +49,26 @@ partial def xmlGetHeadingId (el : Xml.Element) : String := -/ def nameToLink? (s : String) : HtmlM (Option String) := do let res ← getResult - let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous - -- with exactly the same name - if res.name2ModIdx.contains name then - declNameToLink name - -- find similar name in the same module - else - match (← getCurrentName) with - | some currentName => - match (res.moduleInfo.find! currentName).members.find? (sameEnd ·.getName.toString s) with - | some info => - declNameToLink info.getName + if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then + -- with exactly the same name + if res.name2ModIdx.contains name then + declNameToLink name + -- find similar name in the same module + else + match (← getCurrentName) with + | some currentName => + match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with + | some info => + declNameToLink info.getName + | _ => pure none | _ => pure none - | _ => pure none + else + pure none where - sameEnd n1 n2 := Id.run do - let n1' := n1.splitOn "." |>.reverse - let n2' := n2.splitOn "." |>.reverse - for i in [0:n2'.length] do - if n1'.getD i "" = n2'.get! i then - return true - return false + -- check if two names have the same ending components + sameEnd n1 n2 := + List.zip n1.components n2.components + |>.all λ ⟨a, b⟩ => a == b /-- Extend links with following rules: From 2151813fe50fd683f1f19a50e162d25824c84932 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 13:28:48 +0800 Subject: [PATCH 22/22] feat: allow intra link in code block --- DocGen4/Output/DocString.lean | 67 ++++++++++++++++++++++++++--------- 1 file changed, 50 insertions(+), 17 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 7e8ae54..32fe1af 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -8,6 +8,25 @@ open Lean Unicode Xml Parser Parsec namespace DocGen4 namespace Output +/-- Auxiliary function for `splitAround`. -/ +@[specialize] partial def splitAroundAux (s : String) (p : Char → Bool) (b i : String.Pos) (r : List String) : List String := + if s.atEnd i then + let r := (s.extract b i)::r + r.reverse + else + let c := s.get i + if p c then + let i := s.next i + splitAroundAux s p i i (c.toString::s.extract b (i-1)::r) + else + splitAroundAux s p b (s.next i) r + +/-- + Similar to `Stirng.split` in Lean core, but keeps the separater. + e.g. `splitAround "a,b,c" (λ c => c = ',') = ["a", ",", "b", ",", "c"]` +-/ +def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 [] + instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩ /-- Parse an array of Xml/Html document from String. -/ @@ -16,8 +35,8 @@ def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Mis /-- Generate id for heading elements, with the following rules: - 1. Characters in `letter`, `number` and `symbol` unicode categories are preserved. - 2. Any sequences of Characters in `mark`, `punctuation`, `separator` and `other` categories are replaced by a single dash. + 1. Characters in `letter`, `mark`, `number` and `symbol` unicode categories are preserved. + 2. Any sequences of Characters in `punctuation`, `separator` and `other` categories are replaced by a single dash. 3. Cases (upper and lower) are preserved. 4. Xml/Html tags are ignored. -/ @@ -35,11 +54,10 @@ partial def xmlGetHeadingId (el : Xml.Element) : String := s.split pattern |>.filter (!·.isEmpty) |> replacement.intercalate - unicodeToDrop char := - charInGeneralCategory char GeneralCategory.mark || - charInGeneralCategory char GeneralCategory.punctuation || - charInGeneralCategory char GeneralCategory.separator || - charInGeneralCategory char GeneralCategory.other + unicodeToDrop (c : Char) : Bool := + charInGeneralCategory c GeneralCategory.punctuation || + charInGeneralCategory c GeneralCategory.separator || + charInGeneralCategory c GeneralCategory.other /-- This function try to find the given name, both globally and in current module. @@ -53,6 +71,9 @@ def nameToLink? (s : String) : HtmlM (Option String) := do -- with exactly the same name if res.name2ModIdx.contains name then declNameToLink name + -- module name + else if res.moduleNames.contains name then + moduleNameToLink name -- find similar name in the same module else match (← getCurrentName) with @@ -67,7 +88,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do where -- check if two names have the same ending components sameEnd n1 n2 := - List.zip n1.components n2.components + List.zip n1.components' n2.components' |>.all λ ⟨a, b⟩ => a == b /-- @@ -131,7 +152,7 @@ def autoLink (el : Element) : HtmlM Element := do for c in contents do match c with | Content.Character s => - newContents := newContents ++ (← s.splitOn.mapM linkify).intersperse (Content.Character " ") + newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join | _ => newContents := newContents.push c pure ⟨ name, attrs, newContents ⟩ where @@ -139,13 +160,26 @@ def autoLink (el : Element) : HtmlM Element := do let link? ← nameToLink? s match link? with | some link => - let res ← getResult let attributes := Std.RBMap.empty.insert "href" link - pure $ Content.Element $ Element.Element "a" attributes #[Content.Character s] - | none => pure $ Content.Character s - + pure [Content.Element $ Element.Element "a" attributes #[Content.Character s]] + | none => + let sHead := s.dropRightWhile (λ c => c ≠ '.') + let sTail := s.takeRightWhile (λ c => c ≠ '.') + let link'? ← nameToLink? sTail + match link'? with + | some link' => + let attributes := Std.RBMap.empty.insert "href" link' + pure [ + Content.Character sHead, + Content.Element $ Element.Element "a" attributes #[Content.Character sTail] + ] + | none => + pure [Content.Character s] + unicodeToSplit (c : Char) : Bool := + charInGeneralCategory c GeneralCategory.separator || + charInGeneralCategory c GeneralCategory.other /-- Core function of modifying the cmark rendered docstring html. -/ -partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM Element := +partial def modifyElement (element : Element) : HtmlM Element := match element with | el@(Element.Element name attrs contents) => do -- add id and class to @@ -155,13 +189,12 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM else if name = "a" then extendAnchor el -- auto link for inline - else if name = "code" ∧ linkCode = true then + else if name = "code" then autoLink el -- recursively modify else let newContents ← contents.mapM λ c => match c with - -- disable auto link for code blocks - | Content.Element e => (modifyElement e (name ≠ "pre")).map Content.Element + | Content.Element e => (modifyElement e).map Content.Element | _ => pure c pure ⟨ name, attrs, newContents ⟩