cleanup code
parent
f5b9e02766
commit
9570f25312
|
@ -93,24 +93,14 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
|
|||
let mut declList := #[]
|
||||
for (module, mod) in result.moduleInfo.toArray do
|
||||
for decl in filterMapDocInfo mod.members do
|
||||
-- <<<<<<< HEAD
|
||||
let name := decl.getName.toString
|
||||
-- let findDir := basePath / "find" / ma,e
|
||||
-- let findFile := (findDir / "index.html")
|
||||
let config := { config with depthToRoot := 2 }
|
||||
-- let findHtml := ReaderT.run (findRedirectHtml decl.getName) config
|
||||
-- FS.createDirAll findDir
|
||||
-- FS.writeFile findFile findHtml.toString
|
||||
-- let obj := Json.mkObj [("name", decl.getName.toString), ("description", decl.getDocString.getD "")]
|
||||
-- =======
|
||||
let doc := decl.getDocString.getD ""
|
||||
-- let root := module.getRoot
|
||||
let root := Id.run <| ReaderT.run (getRoot) config
|
||||
let link := root ++ s!"../semantic/{decl.getName.hash}.xml#"
|
||||
let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config
|
||||
let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config
|
||||
let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourceLink", sourceLink)]
|
||||
-- >>>>>>> upstream/main
|
||||
declList := declList.push obj
|
||||
let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config
|
||||
FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml
|
||||
|
|
|
@ -5,7 +5,6 @@ import Cli
|
|||
open DocGen4 Lean Cli
|
||||
|
||||
def runDocGenCmd (p : Parsed) : IO UInt32 := do
|
||||
-- let root := p.positionalArg! "root" |>.as! String
|
||||
let modules : List String := p.variableArgsAs! String |>.toList
|
||||
let res ← lakeSetup modules
|
||||
match res with
|
||||
|
@ -22,7 +21,6 @@ def docGenCmd : Cmd := `[Cli|
|
|||
"A documentation generator for Lean 4."
|
||||
|
||||
ARGS:
|
||||
-- root : String; "The root URL to generate the HTML for (will be relative in the future)"
|
||||
...modules : String; "The modules to generate the HTML for"
|
||||
]
|
||||
|
||||
|
|
Loading…
Reference in New Issue