From 0b8f7a1397ddb4d4fbd717c09debe1d0c6ca7017 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 19 May 2022 20:54:42 +0200
Subject: [PATCH] doc: Output top level module

---
 DocGen4/Output.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 8d99535..feedfda 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -16,8 +16,12 @@ import DocGen4.Output.SourceLinker
 
 namespace DocGen4
 
-open Lean Std IO System Output
+open Lean IO System Output
 
+/--
+The main entrypoint for outputting the documentation HTML based on an
+`AnalyzerResult`.
+-/
 def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
   let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
   let basePath := FilePath.mk "." / "build" / "doc"