From 82f63cb6134dc96dea0c8736e755c3a605139770 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 7 Jan 2022 10:56:39 +0100
Subject: [PATCH] feat: parameterize the URL root for links in the HTML

---
 DocGen4/Output.lean | 5 ++---
 Main.lean           | 5 +++--
 README.md           | 5 +++--
 deploy_docs.sh      | 2 +-
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index b64b550..d79c658 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -14,9 +14,8 @@ namespace DocGen4
 
 open Lean Std IO System Output
 
-def htmlOutput (result : AnalyzerResult) : IO Unit := do
-  -- TODO: parameterize this
-  let config := { root := "/", result := result, currentName := none}
+def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
+  let config := { root := root, result := result, currentName := none}
   let basePath := FilePath.mk "./build/doc/"
   let indexHtml := ReaderT.run index config 
   let notFoundHtml := ReaderT.run notFound config
diff --git a/Main.lean b/Main.lean
index bc5c77a..7f527a4 100644
--- a/Main.lean
+++ b/Main.lean
@@ -4,9 +4,10 @@ import Lean
 open DocGen4 Lean IO
 
 def main (args : List String) : IO Unit := do
-  let modules := args
+  let root := args.head!
+  let modules := args.tail!
   let path ← lakeSetupSearchPath (←getLakePath) modules.toArray
   IO.println s!"Loading modules from: {path}"
   let doc ← load $ modules.map Name.mkSimple
   IO.println "Outputting HTML"
-  htmlOutput doc
+  htmlOutput doc root
diff --git a/README.md b/README.md
index d0ff1e1..7c343a5 100644
--- a/README.md
+++ b/README.md
@@ -4,9 +4,10 @@ Document Generator for Lean 4
 ## Usage
 You can call `doc-gen4` from the top of a Lake project like this:
 ```sh
-$ /path/to/doc-gen4 Module
+$ /path/to/doc-gen4 / Module
 ```
-Where `Module` is one or more of the top level modules you want to document.
+Where the `/` is the root URL the HTML will refer to and `Module` is one or
+more of the top level modules you want to document.
 The tool will then proceed to compile the project using lake (if that hasn't happened yet),
 analyze it and put the result in `./build/doc`.
 You could e.g. host the files locally with the built-in Python webserver:
diff --git a/deploy_docs.sh b/deploy_docs.sh
index d9d89bc..2f77858 100755
--- a/deploy_docs.sh
+++ b/deploy_docs.sh
@@ -23,7 +23,7 @@ fi
 
 # generate the docs
 cd $1
-../$2/build/bin/doc-gen4 Mathlib
+../$2/build/bin/doc-gen4 /mathlib4_docs/ Mathlib
 
 if [ "$3" = "true" ]; then
   cd ..