Update to doc-gen4 commit `6abc8bb`.

DocGen4/Load.lean

@@ -43,7 +43,6 @@ to process for documentation.
 -/
 def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do
   let env ← envOfImports task.getLoad
-  IO.println "Processing modules"
   let config := {
     -- TODO: parameterize maxHeartbeats
     maxHeartbeats := 100000000,

DocGen4/Output.lean

@@ -109,7 +109,6 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
     FS.writeFile filePath moduleHtml.toString
     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'
         -- The last component is the file name, however we are in src/ here so dont drop it this time
         let baseConfig := {baseConfig with depthToRoot := modName.components.length }
@@ -153,4 +152,3 @@ def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Work
   htmlOutputIndex baseConfig
 
 end DocGen4
-

DocGen4/Output/DocString.lean

@@ -22,7 +22,7 @@ namespace Output
       splitAroundAux s p b (s.next i) r
 
 /--
-  Similar to `Stirng.split` in Lean core, but keeps the separater.
+  Similar to `String.split` in Lean core, but keeps the separater.
   e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]`
 -/
 def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
@@ -195,7 +195,9 @@ partial def modifyElement (element : Element) : HtmlM Element :=
     else if name = "a" then
       extendAnchor el
     -- auto link for inline <code></code>
-    else if name = "code" then
+    else if name = "code" ∧
+      -- don't linkify code blocks explicitly tagged with a language other than lean
+      (((attrs.find? "class").getD "").splitOn.all (fun s => s == "language-lean" || !s.startsWith "language-")) then
       autoLink el
     -- recursively modify
     else

DocGen4/Output/Module.lean

@@ -30,7 +30,10 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   | BinderInfo.implicit => ("{", "}", true)
   | BinderInfo.strictImplicit => ("⦃", "⦄", true)
   | BinderInfo.instImplicit => ("[", "]", true)
-  let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "]
+  let mut nodes :=
+    match arg.name with
+    | some name => #[Html.text s!"{l}{name.toString} : "]
+    | none => #[Html.text s!"{l}"]
   nodes := nodes.append (← infoFormatToHtml arg.type)
   nodes := nodes.push r
   let inner := <span class="fn">[nodes]</span>

DocGen4/Process/Analyze.lean

@@ -134,7 +134,11 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
         let module := res.find! moduleName
         res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
     catch e =>
-      IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}"
+      if let some pos := e.getRef.getPos? then
+        let pos := (← getFileMap).toPosition pos
+        IO.println s!"WARNING: Failed to obtain information in file: {pos}, for: {name}, {← e.toMessageData.toString}"
+      else
+        IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}"
 
   -- TODO: This could probably be faster if we did sorted insert above instead
   for (moduleName, module) in res.toArray do

DocGen4/Process/Attributes.lean

@@ -124,7 +124,15 @@ def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (att
   return res
 
 def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes
-def getParametricValues (decl : Name) : MetaM (Array String) := getValues decl parametricAttributes
+def getParametricValues (decl : Name) : MetaM (Array String) := do
+  let mut uniform ← getValues decl parametricAttributes
+  -- This attribute contains an `Option Name` but we would like to pretty print it better
+  if let some depTag := Linter.deprecatedAttr.getParam? (← getEnv) decl then
+    let str := match depTag with
+    | some alt => s!"deprecated {alt.toString}"
+    | none => "deprecated"
+    uniform := uniform.push str
+  return uniform
 
 def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do
   let insts ← getDefaultInstances className

DocGen4/Process/Base.lean

@@ -27,14 +27,16 @@ structure NameInfo where
   doc : Option String
   deriving Inhabited
 
+
 /--
 An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
 -/
 structure Arg where
   /--
-  The name of the argument.
+  The name of the argument. For auto generated argument names like `[Monad α]`
+  this is none
   -/
-  name : Name
+  name : Option Name
   /--
   The pretty printed type of the argument.
   -/

DocGen4/Process/NameInfo.lean

@@ -15,17 +15,20 @@ def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
   let env ← getEnv
   return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n}
 
-partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
+partial def typeToArgsType (e : Expr) : (Array ((Option Name) × Expr × BinderInfo) × Expr) :=
   let helper := fun name type body data =>
     -- Once we hit a name with a macro scope we stop traversing the expression
     -- and print what is left after the : instead. The only exception
     -- to this is instances since these almost never have a name
     -- but should still be printed as arguments instead of after the :.
-    if name.hasMacroScopes && !data.isInstImplicit then
+    if data.isInstImplicit && name.hasMacroScopes then
+      let arg := (none, type, data)
+      let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
+      (#[arg] ++ args, final)
+    else if name.hasMacroScopes then
       (#[], e)
     else
-      let name := name.eraseMacroScopes
+      let arg := (some name, type, data)
-      let arg := (name, type, data)
       let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
       (#[arg] ++ args, final)
   match e.consumeMData with

Main.lean

@@ -16,7 +16,6 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do
   match res with
   | Except.ok ws =>
     let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
-    IO.println "Outputting HTML"
     let baseConfig ← getSimpleBaseContext hierarchy
     htmlOutputResults baseConfig doc ws (p.hasFlag "ink")
     return 0
@@ -33,9 +32,8 @@ def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
   match res with
   | Except.ok ws =>
     let (doc, hierarchy) ← loadCore
-    IO.println "Outputting HTML"
     let baseConfig ← getSimpleBaseContext hierarchy
-    htmlOutputResults baseConfig doc ws (ink := False) 
+    htmlOutputResults baseConfig doc ws (ink := False)
     return 0
   | Except.error rc => pure rc
 

static/search.js

@@ -137,10 +137,21 @@ function handleSearch(dataCenter, err, ev, sr, maxResults, autocomplete) {
   sr.setAttribute("state", "done");
 }
 
+// https://www.joshwcomeau.com/snippets/javascript/debounce/
+const debounce = (callback, wait) => {
+  let timeoutId = null;
+  return (...args) => {
+    window.clearTimeout(timeoutId);
+    timeoutId = window.setTimeout(() => {
+      callback.apply(null, args);
+    }, wait);
+  };
+}
+
 DeclarationDataCenter.init()
   .then((dataCenter) => {
     // Search autocompletion.
-    SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS, true));
+    SEARCH_INPUT.addEventListener("input", debounce(ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS, true), 500));
     if(SEARCH_PAGE_INPUT) {
       SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false))
       document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
@@ -151,7 +162,7 @@ DeclarationDataCenter.init()
     SEARCH_INPUT.dispatchEvent(new Event("input"))
   })
   .catch(e => {
-    SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS,true ));
+    SEARCH_INPUT.addEventListener("input", debounce(ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS, true), 500));
     if(SEARCH_PAGE_INPUT) {
       SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false));
     }