From 14afcdbeaf52250d993c9974c2148117183ca147 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 26 Jul 2022 13:56:22 +0200
Subject: [PATCH] feat: Degrade --ink to flag

---
 DocGen4/Output.lean | 10 +++++-----
 Main.lean           | 18 ++++--------------
 2 files changed, 9 insertions(+), 19 deletions(-)

diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 3a6bdd7..d92d9d6 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -72,11 +72,11 @@ def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
     let jsonDecls ← Module.toJson mod
     FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress
 
-def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
+def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
   let config : SiteContext := {
     result := result,
     sourceLinker := ←sourceLinker ws
-    leanInkEnabled := inkPath.isSome
+    leanInkEnabled := ink
   }
 
   FS.createDirAll basePath
@@ -100,7 +100,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
     let moduleHtml := moduleToHtml module |>.run config baseConfig
     FS.createDirAll fileDir
     FS.writeFile filePath moduleHtml.toString
-    if let some inkPath := inkPath then
+    if ink then
       if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
         IO.println s!"Inking: {modName.toString}"
         -- path: 'basePath/src/module/components/till/last.html'
@@ -134,9 +134,9 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
 The main entrypoint for outputting the documentation HTML based on an
 `AnalyzerResult`.
 -/
-def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
+def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
   let baseConfig := getSimpleBaseContext hierarchy
-  htmlOutputResults baseConfig result ws inkPath
+  htmlOutputResults baseConfig result ws ink
   htmlOutputIndex baseConfig
 
 end DocGen4
diff --git a/Main.lean b/Main.lean
index 8b074cb..2d083eb 100644
--- a/Main.lean
+++ b/Main.lean
@@ -4,16 +4,6 @@ import Cli
 
 open DocGen4 Lean Cli
 
-def findLeanInk? (p : Parsed) : IO (Option System.FilePath) := do
-  match p.flag? "ink" with
-  | some ink =>
-    let inkPath := System.FilePath.mk ink.value
-    if ←inkPath.pathExists then
-      pure <| some inkPath
-    else
-      throw <| IO.userError "Invalid path to LeanInk binary provided"
-  | none => pure none
-
 def getTopLevelModules (p : Parsed) : IO (List String) :=  do
   let topLevelModules := p.variableArgsAs! String |>.toList
   if topLevelModules.length == 0 then
@@ -29,7 +19,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do
       let (doc, hierarchy) ← load (.loadAllLimitAnalysis relevantModules)
       IO.println "Outputting HTML"
       let baseConfig := getSimpleBaseContext hierarchy
-      htmlOutputResults baseConfig doc ws (←findLeanInk? p)
+      htmlOutputResults baseConfig doc ws (p.hasFlag "ink")
       pure 0
     | Except.error rc => pure rc
 
@@ -51,7 +41,7 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do
     let modules := modules.map String.toName
     let (doc, hierarchy) ← load (.loadAll modules)
     IO.println "Outputting HTML"
-    htmlOutput doc hierarchy ws (←findLeanInk? p)
+    htmlOutput doc hierarchy ws (p.hasFlag "ink")
     pure 0
   | Except.error rc => pure rc
 
@@ -60,7 +50,7 @@ def singleCmd := `[Cli|
   "Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated."
 
   FLAGS:
-    ink : String; "Path to a LeanInk binary to use for rendering the Lean sources."
+    ink; "Render the files with LeanInk in addition"
 
   ARGS:
     module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
@@ -78,7 +68,7 @@ def docGenCmd : Cmd := `[Cli|
   "A documentation generator for Lean 4."
 
   FLAGS:
-    ink : String; "Path to a LeanInk binary to use for rendering the Lean sources."
+    ink; "Render the files with LeanInk in addition"
 
   ARGS:
     ...modules : String; "The modules to generate the HTML for."