diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 32fe8aa..e8cb33f 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -9,6 +9,7 @@ import DocGen4.Output.Base import DocGen4.Output.Index import DocGen4.Output.Module import DocGen4.Output.NotFound +import DocGen4.Output.Find namespace DocGen4 @@ -65,14 +66,21 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let basePath := FilePath.mk "./build/doc/" let indexHtml := ReaderT.run index config let notFoundHtml := ReaderT.run notFound config + FS.createDirAll basePath + FS.createDirAll (basePath / "find") + let mut declList := #[] for (_, mod) in result.moduleInfo.toArray do for decl in mod.members do + let findHtml := ReaderT.run (findRedirectHtml decl.getName) config + let findDir := basePath / "find" / decl.getName.toString + FS.createDirAll findDir + FS.writeFile (findDir / "index.html") findHtml.toString let obj := Json.mkObj [("name", decl.getName.toString), ("description", decl.getDocString.getD "")] declList := declList.push obj let json := Json.arr declList + FS.writeFile (basePath / "searchable_data.bmp") json.compress - FS.createDirAll basePath FS.writeFile (basePath / "index.html") indexHtml.toString FS.writeFile (basePath / "style.css") styleCss FS.writeFile (basePath / "404.html") notFoundHtml.toString diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean new file mode 100644 index 0000000..41b82dd --- /dev/null +++ b/DocGen4/Output/Find.lean @@ -0,0 +1,15 @@ +import DocGen4.Output.Template + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx +open Lean + +def findRedirectHtml (decl : Name) : HtmlM Html := do + let res ← getResult + let url ← declNameToLink decl + let contentString := s!"0;url={url}" + pure $ Html.element "meta" false #[("http-equiv", "refresh"), ("content", contentString)] #[] +end Output +end DocGen4