diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean index dcd31aa..99a1bc4 100644 --- a/DocGen4/LeanInk/Process.lean +++ b/DocGen4/LeanInk/Process.lean @@ -27,20 +27,20 @@ def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do let ctx ← readThe SiteContext let baseCtx ← readThe SiteBaseContext let outputFn := (docGenOutput · |>.run ctx baseCtx) - return ← LeanInk.Analysis.runAnalysis { + return ← LeanInk.Analysis.runAnalysis { name := "doc-gen4" genOutput := outputFn - } + } def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do execAuxM.run (←readThe SiteContext) (←readThe SiteBaseContext) |>.run config -@[implementedBy enableInitializersExecution] +@[implemented_by enableInitializersExecution] private def enableInitializersExecutionWrapper : IO Unit := pure () def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do let contents ← IO.FS.readFile sourceFilePath - let config := { + let config := { inputFilePath := sourceFilePath inputFileContents := contents lakeFile := none diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index aaa1bd2..a4128bf 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -43,8 +43,8 @@ def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Mis partial def xmlGetHeadingId (el : Xml.Element) : String := elementToPlainText el |> replaceCharSeq unicodeToDrop "-" where - elementToPlainText el := match el with - | (Element.Element _ _ contents) => + elementToPlainText el := match el with + | (Element.Element _ _ contents) => "".intercalate (contents.toList.map contentToPlainText) contentToPlainText c := match c with | Content.Element el => elementToPlainText el @@ -54,10 +54,10 @@ partial def xmlGetHeadingId (el : Xml.Element) : String := s.split pattern |>.filter (!·.isEmpty) |> replacement.intercalate - unicodeToDrop (c : Char) : Bool := + unicodeToDrop (c : Char) : Bool := charInGeneralCategory c GeneralCategory.punctuation || charInGeneralCategory c GeneralCategory.separator || - charInGeneralCategory c GeneralCategory.other + charInGeneralCategory c GeneralCategory.other /-- This function try to find the given name, both globally and in current module. @@ -79,7 +79,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do match (← getCurrentName) with | some currentName => match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with - | some info => + | some info => declNameToLink info.getName | _ => pure none | _ => pure none @@ -88,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.componentsRev n2.componentsRev |>.all λ ⟨a, b⟩ => a == b /-- @@ -106,11 +106,11 @@ def extendLink (s : String) : HtmlM String := do pure link else panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported" - -- for id + -- for id else if s.startsWith "#" then 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) @@ -126,13 +126,13 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme let newAttrs := attrs |>.insert "id" id |>.insert "class" "markdown-heading" - let newContents := (← + let newContents := (← contents.mapM (λ c => match c with | Content.Element e => return Content.Element (← modifyElement e) | _ => pure c)) |>.push (Content.Character " ") |>.push (Content.Element anchor) - pure ⟨ name, newAttrs, newContents⟩ + pure ⟨ name, newAttrs, newContents⟩ /-- Extend anchor links. -/ def extendAnchor (el : Element) : HtmlM Element := do @@ -158,7 +158,7 @@ def autoLink (el : Element) : HtmlM Element := do linkify s := do let link? ← nameToLink? s match link? with - | some link => + | some link => let attributes := Lean.RBMap.empty.insert "href" link pure [Content.Element <| Element.Element "a" attributes #[Content.Character s]] | none => @@ -166,7 +166,7 @@ def autoLink (el : Element) : HtmlM Element := do let sTail := s.takeRightWhile (λ c => c ≠ '.') let link'? ← nameToLink? sTail match link'? with - | some link' => + | some link' => let attributes := Lean.RBMap.empty.insert "href" link' pure [ Content.Character sHead, @@ -174,9 +174,9 @@ def autoLink (el : Element) : HtmlM Element := do ] | none => pure [Content.Character s] - unicodeToSplit (c : Char) : Bool := + unicodeToSplit (c : Char) : Bool := charInGeneralCategory c GeneralCategory.separator || - charInGeneralCategory c GeneralCategory.other + charInGeneralCategory c GeneralCategory.other /-- Core function of modifying the cmark rendered docstring html. -/ partial def modifyElement (element : Element) : HtmlM Element := match element with @@ -195,13 +195,13 @@ partial def modifyElement (element : Element) : HtmlM Element := let newContents ← contents.mapM λ c => match c with | Content.Element e => return Content.Element (← modifyElement e) | _ => pure c - pure ⟨ name, attrs, newContents ⟩ + 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 - | Parsec.ParseResult.success _ res => + | Parsec.ParseResult.success _ res => res.mapM λ x => do pure (Html.text <| toString (← modifyElement x)) | _ => pure #[Html.text rendered] diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index fdf5fdd..b12f125 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -16,7 +16,7 @@ def instancesForToHtml (typeName : Name) : HtmlM Html := do def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do - let shortName := c.name.components'.head!.toString + let shortName := c.name.componentsRev.head!.toString let name := c.name.toString if let some doc := c.doc then let renderedDoc ← docStringToHtml doc diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index e7ec326..85932cd 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -30,8 +30,6 @@ def argToHtml (arg : Arg) : HtmlM Html := do | BinderInfo.implicit => ("{", "}", true) | BinderInfo.strictImplicit => ("⦃", "⦄", true) | BinderInfo.instImplicit => ("[", "]", true) - -- TODO: Can this ever be reached here? What does it mean? - | BinderInfo.auxDecl => unreachable! let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "] nodes := nodes.append (←infoFormatToHtml arg.type) nodes := nodes.push r @@ -146,7 +144,7 @@ Rendering a module doc string, that is the ones with an ! after the opener as HTML. -/ def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do - pure + pure
[←docStringToHtml mdoc.doc]
diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index 44a0c21..6326fbf 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -12,7 +12,7 @@ open Lean Render a single field consisting of its documentation, its name and its type as HTML. -/ def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do - let shortName := f.name.components'.head!.toString + let shortName := f.name.componentsRev.head!.toString let name := f.name.toString if let some doc := f.doc then let renderedDoc ← docStringToHtml doc @@ -37,7 +37,7 @@ def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do [←i.fieldInfo.mapM fieldToHtml] ) else - let ctorShortName := i.ctor.name.components'.head!.toString + let ctorShortName := i.ctor.name.componentsRev.head!.toString (