From 9570f25312ac0a5773f5ee33490ae2d0f2c48655 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Thu, 7 Apr 2022 00:48:12 +0100
Subject: [PATCH] cleanup code

---
 DocGen4/Output.lean | 10 ----------
 Main.lean           |  2 --
 2 files changed, 12 deletions(-)

diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index f4dd4d5..3d901c8 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -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
diff --git a/Main.lean b/Main.lean
index 88a0640..8bb1187 100644
--- a/Main.lean
+++ b/Main.lean
@@ -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"
 ]