diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index 619ea7f..947e48a 100644
--- a/DocGen4/Load.lean
+++ b/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,
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 4e3f32d..543e001 100644
--- a/DocGen4/Output.lean
+++ b/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
-
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index 33c8503..01530f4 100644
--- a/DocGen4/Output/DocString.lean
+++ b/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
- 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
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 03c0fdc..b14b6da 100644
--- a/DocGen4/Output/Module.lean
+++ b/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 := [nodes]
diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean
index b071997..9c4c03d 100644
--- a/DocGen4/Process/Analyze.lean
+++ b/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
diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean
index 14d3336..ff6e7f3 100644
--- a/DocGen4/Process/Attributes.lean
+++ b/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
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index c5908ce..cf3df3a 100644
--- a/DocGen4/Process/Base.lean
+++ b/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.
-/
diff --git a/DocGen4/Process/NameInfo.lean b/DocGen4/Process/NameInfo.lean
index cb082bb..8cb0ed8 100644
--- a/DocGen4/Process/NameInfo.lean
+++ b/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 := (name, type, data)
+ let arg := (some name, type, data)
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final)
match e.consumeMData with
diff --git a/Main.lean b/Main.lean
index 5758b8d..e78677d 100644
--- a/Main.lean
+++ b/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
diff --git a/static/search.js b/static/search.js
index 7971a82..809f4bd 100644
--- a/static/search.js
+++ b/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));
}