From 7907803093354825833ce6d824d890b9f61d1f39 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 7 Nov 2023 17:28:35 -0700 Subject: [PATCH] Update to doc-gen4 commit `6abc8bb`. --- DocGen4/Load.lean | 1 - DocGen4/Output.lean | 2 -- DocGen4/Output/DocString.lean | 6 ++++-- DocGen4/Output/Module.lean | 5 ++++- DocGen4/Process/Analyze.lean | 6 +++++- DocGen4/Process/Attributes.lean | 10 +++++++++- DocGen4/Process/Base.lean | 6 ++++-- DocGen4/Process/NameInfo.lean | 11 +++++++---- Main.lean | 4 +--- static/search.js | 15 +++++++++++++-- 10 files changed, 47 insertions(+), 19 deletions(-) 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)); }