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
+ ]
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 [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"
}
]
}