From 0f7a4a9afc5bed4d5f556cfb872ff425173e1a78 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 21 Jul 2025 14:17:03 +0200 Subject: [PATCH 01/15] WIP: upstream search/quickjump bar When complete, this will enable search for all Verso manuals. --- lakefile.lean | 6 + src/verso-manual/VersoManual.lean | 15 +- src/verso-manual/VersoManual/Basic.lean | 24 + src/verso-manual/VersoManual/Docstring.lean | 36 + src/verso-manual/VersoManual/Glossary.lean | 14 + src/verso-manual/VersoManual/Html.lean | 5 + src/verso-manual/VersoManual/Html/Style.lean | 3 + src/verso-search/VersoSearch.lean | 1 + .../VersoSearch/DomainSearch.lean | 179 +++ src/verso-util/VersoUtil.lean | 1 + .../VersoUtil}/BinFiles.lean | 2 +- .../VersoUtil}/BinFiles/Z85.lean | 0 src/verso/Verso/Output/Html/KaTeX.lean | 2 +- static-web/search/README.txt | 57 + static-web/search/fuzzysort.d.ts | 105 ++ static-web/search/fuzzysort.js | 2 + static-web/search/jsconfig.json | 8 + static-web/search/licenses.md | 41 + static-web/search/search-box.css | 254 ++++ static-web/search/search-box.js | 1165 +++++++++++++++++ static-web/search/search-highlight.css | 76 ++ static-web/search/search-highlight.js | 390 ++++++ static-web/search/search-init.js | 48 + .../search/unicode-input-component.min.js | 2 + static-web/search/unicode-input.min.js | 1 + 25 files changed, 2433 insertions(+), 4 deletions(-) create mode 100644 src/verso-search/VersoSearch/DomainSearch.lean create mode 100644 src/verso-util/VersoUtil.lean rename src/{verso/Verso => verso-util/VersoUtil}/BinFiles.lean (99%) rename src/{verso/Verso => verso-util/VersoUtil}/BinFiles/Z85.lean (100%) create mode 100644 static-web/search/README.txt create mode 100644 static-web/search/fuzzysort.d.ts create mode 100644 static-web/search/fuzzysort.js create mode 100644 static-web/search/jsconfig.json create mode 100644 static-web/search/licenses.md create mode 100644 static-web/search/search-box.css create mode 100644 static-web/search/search-box.js create mode 100644 static-web/search/search-highlight.css create mode 100644 static-web/search/search-highlight.js create mode 100644 static-web/search/search-init.js create mode 100644 static-web/search/unicode-input-component.min.js create mode 100644 static-web/search/unicode-input.min.js diff --git a/lakefile.lean b/lakefile.lean index 2b6a4e8d6..7ea1af13c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,6 +7,12 @@ require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main" package verso where precompileModules := false -- temporarily disabled to work around an issue with nightly-2025-03-30 +@[default_target] +lean_lib VersoUtil where + srcDir := "src/verso-util" + roots := #[`VersoUtil] + + @[default_target] lean_lib Verso where srcDir := "src/verso" diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index 9adeeae4b..49a7e8726 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -270,7 +270,9 @@ def traverse (logError : String → IO Unit) (text : Part Manual) (config : Conf if config.verbose then IO.println "Initializing extensions" let extensionImpls ← readThe ExtensionImpls - state := state.setDomainTitle sectionDomain "Sections or chapters of the manual" + state := state + |>.setDomainTitle sectionDomain "Sections or chapters of the manual" + |>.addQuickJumpMapper sectionDomain sectionDomainMapper for ⟨_, b⟩ in extensionImpls.blockDescrs do if let some descr := b.get? BlockDescr then state := descr.init state @@ -468,6 +470,12 @@ def addSearchIndex (state : TraverseState) (ctx : TraverseContext) (logError : S let indexJs := indexJs ++ "window.searchIndex = elasticlunr ? __versoSearchIndex : null;\n" return { state with extraJsFiles := state.extraJsFiles.push { filename := "searchIndex.js", contents := indexJs } } +def emitSearchBox (dir : System.FilePath) (domains : DomainMappers) : IO Unit := do + ensureDir dir + for (file, contents) in searchBoxCode do + IO.FS.writeBinFile (dir / file) contents + IO.FS.writeFile (dir / "domain-mappers.js") (domains.toJs.pretty (width := 70)) + end def wordCount @@ -487,6 +495,7 @@ def emitHtmlSingle ensureDir dir let (traverseOut, st) ← emitContent dir .empty IO.FS.writeFile (dir.join "-verso-docs.json") (toString st.dedup.docJson) + emitSearchBox (dir / "-verso-search") traverseOut.2.quickJump pure traverseOut where emitContent (dir : System.FilePath) : StateT (State Html) (ReaderT ExtensionImpls IO) (Part Manual × TraverseState) := do @@ -564,6 +573,7 @@ def emitHtmlMulti (logError : String → IO Unit) (config : Config) ensureDir root let (traverseOut, st) ← emitContent root {} IO.FS.writeFile (root.join "-verso-docs.json") (toString st.dedup.docJson) + emitSearchBox (root / "-verso-search") traverseOut.2.quickJump pure traverseOut where /-- @@ -696,7 +706,8 @@ Adds a bundled version of elasticlunr.js to the config. -/ def Config.addSearch (config : Config) : Config := { config with - extraJsFiles := config.extraJsFiles.push {filename := "elasticlunr.min.js", contents := elasticlunr.js} + extraJsFiles := + config.extraJsFiles.push {filename := "elasticlunr.min.js", contents := elasticlunr.js}, licenseInfo := Licenses.elasticlunr.js :: config.licenseInfo } diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean index ea19d6d80..dbd9bfc83 100644 --- a/src/verso-manual/VersoManual/Basic.lean +++ b/src/verso-manual/VersoManual/Basic.lean @@ -11,12 +11,14 @@ import Verso.Doc.Html import Verso.Doc.TeX import MultiVerso import MultiVerso.Slug +import VersoSearch import VersoManual.LicenseInfo import VersoManual.Ext import Verso.Output.Html import Verso.Output.TeX import Verso.BEq + open Lean (Name Json NameMap ToJson FromJson) open Std (HashSet HashMap TreeSet) open Verso.Doc @@ -147,6 +149,7 @@ instance : ForIn m Domains (Name × Domain) := def StringSet := HashSet String +open Verso.Search in structure TraverseState where tags : HashMap Tag InternalId := {} externalTags : HashMap InternalId Link := {} @@ -157,6 +160,7 @@ structure TraverseState where extraJs : HashSet String := {} extraJsFiles : Array JsFile := #[] extraCssFiles : Array (String × String) := #[] + quickJump : DomainMappers := {} licenseInfo : HashSet LicenseInfo := {} private contents : NameMap Json := {} @@ -191,6 +195,8 @@ local instance [BEq α] [Hashable α] : BEq (HashSet α) where local instance [BEq α] [Ord α] : BEq (TreeSet α) where beq := ptrEqThen fun xs ys => xs.size == ys.size && xs.all (ys.contains ·) +local instance [BEq α] [Hashable α] [BEq β] : BEq (HashMap α β) where + beq := ptrEqThen fun xs ys => xs.size == ys.size && xs.all (ys[·]?.isEqSome ·) instance : BEq TraverseState where beq := ptrEqThen fun x y => @@ -208,6 +214,7 @@ instance : BEq TraverseState where x.extraJs == y.extraJs && x.extraJsFiles == y.extraJsFiles && x.extraCssFiles == y.extraCssFiles && + x.quickJump == y.quickJump && ptrEqThen' x.contents y.contents (fun c1 c2 => c1.size == c2.size && c1.all (c2.find? · |>.isEqSome ·)) && @@ -246,6 +253,10 @@ def setDomainTitle (state : TraverseState) (domain : Name) (title : String) : Tr def setDomainDescription (state : TraverseState) (domain : Name) (description : String) : TraverseState := {state with domains := state.domains.insert domain {state.domains.find? domain |>.getD {} with description := some description}} +open Verso.Search in +def addQuickJumpMapper (state : TraverseState) (domain : Name) (domainMapper : DomainMapper) : TraverseState := + { state with quickJump := state.quickJump.insert domain.toString domainMapper } + def htmlId (state : TraverseState) (id : InternalId) : Array (String × String) := if let some {htmlId, ..} := state.externalTags[id]? then #[("id", htmlId.toString)] @@ -759,6 +770,19 @@ def sectionString (ctxt : TraverseContext) : Option String := def sectionDomain := `Verso.Genre.Manual.section +open Verso.Search in +def sectionDomainMapper : DomainMapper where + displayName := "Section" + className := "section-domain" + dataToSearchables := + "(domainData) => + Object.entries(domainData.contents).map(([key, value]) => ({ + searchKey: `${value[0].data.sectionNum} ${value[0].data.title}`, + address: `${value[0].address}#${value[0].id}`, + domainId: 'Verso.Genre.Manual.section', + ref: value, + }))" + instance : TraversePart Manual where inPart p := (·.inPart p) diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index ab65ce9e7..2cd965447 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -773,12 +773,16 @@ def Signature.toHtml : Signature → HighlightHtmlM Html | {wide, narrow} => do return {{
{{← wide.toHtml}}
{{← narrow.toHtml}}
}} +open Verso.Search in +def docDomainMapper : DomainMapper := .withDefaultJs docstringDomain "Documentation" "doc-domain" + open Verso.Genre.Manual.Markdown in @[block_extension Block.docstring] def docstring.descr : BlockDescr := withHighlighting { init st := st |>.setDomainTitle docstringDomain "Lean constant reference" |>.setDomainDescription docstringDomain "Documentation for Lean constants" + |>.addQuickJumpMapper docstringDomain docDomainMapper traverse id info _ := do let .ok (name, declType, _signature, _customLabel) := @@ -1577,11 +1581,16 @@ def optionDocs : BlockRoleExpander | _, more => throwErrorAt more[0]! "Unexpected block argument" +open Verso.Search in +def optionDomainMapper : DomainMapper := + .withDefaultJs optionDomain "Compiler Option" "doc-option-domain" + open Verso.Genre.Manual.Markdown in @[block_extension optionDocs] def optionDocs.descr : BlockDescr where init st := st |>.setDomainTitle optionDomain "Compiler options" + |>.addQuickJumpMapper optionDomain optionDomainMapper traverse id info _ := do let .ok (name, _defaultValue) := FromJson.fromJson? (α := Name × Highlighted) info @@ -1695,6 +1704,18 @@ def Inline.tactic : Inline where name := `Verso.Genre.Manual.tacticInline +open Verso.Search in +def tacticDomainMapper : DomainMapper where + className := "tactic-domain" + displayName := "Tactic" + dataToSearchables := + "(domainData) => + Object.entries(domainData.contents).map(([key, value]) => ({ + searchKey: value[0].data.userName, + address: `${value[0].address}#${value[0].id}`, + domainId: 'Verso.Genre.Manual.doc.tactic', + ref: value, + }))" open Verso.Genre.Manual.Markdown in open Lean Elab Term Parser Tactic Doc in @@ -1703,6 +1724,7 @@ def tactic.descr : BlockDescr := withHighlighting { init st := st |>.setDomainTitle tacticDomain "Tactic Documentation" |>.setDomainDescription tacticDomain "Detailed descriptions of tactics" + |>.addQuickJumpMapper tacticDomain tacticDomainMapper traverse id info _ := do let .ok (tactic, «show») := FromJson.fromJson? (α := TacticDoc × Option String) info @@ -1830,6 +1852,19 @@ def conv : DirectiveExpander | throwError "An explicit 'show' is mandatory for conv docs (for now)" pure #[← ``(Verso.Doc.Block.other (Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?)) #[$(contents ++ userContents),*])] +open Verso.Search in +def convDomainMapper : DomainMapper where + className := "conv-tactic-domain" + displayName := "Conv Tactic" + dataToSearchables := + "(domainData) => + Object.entries(domainData.contents).map(([key, value]) => ({ + searchKey: key, + address: `${value[0].address}#${value[0].id}`, + domainId: 'Verso.Genre.Manual.doc.tactic.conv', + ref: value, + }))" + open Verso.Genre.Manual.Markdown in open Lean Elab Term Parser Tactic Doc in @[block_extension conv] @@ -1837,6 +1872,7 @@ def conv.descr : BlockDescr := withHighlighting { init st := st |>.setDomainTitle convDomain "Conversion Tactics" |>.setDomainDescription convDomain "Tactics for performing targeted rewriting of subterms" + |>.addQuickJumpMapper convDomain convDomainMapper traverse id info _ := do let .ok (name, «show», _docs?) := FromJson.fromJson? (α := Name × String × Option String) info diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean index f0ed5afeb..7bddf5fc9 100644 --- a/src/verso-manual/VersoManual/Glossary.lean +++ b/src/verso-manual/VersoManual/Glossary.lean @@ -95,11 +95,25 @@ def Glossary.addEntry [Monad m] [MonadState TraverseState m] [MonadLiftT IO m] [ | some (.ok (v : Json)) => modify (TraverseState.set · glossaryState <| v.setObjVal! key (ToJson.toJson id)) +open Verso.Search in +def technicalTermDomainMapper : DomainMapper where + displayName := "Terminology" + className := "tech-term-domain" + dataToSearchables := + "(domainData) => + Object.entries(domainData.contents).map(([key, value]) => ({ + searchKey: value[0].data.term, + address: `${value[0].address}#${value[0].id}`, + domainId: 'Verso.Genre.Manual.doc.tech', + ref: value, + }))" + @[inline_extension deftech] def deftech.descr : InlineDescr where init st := st |>.setDomainTitle technicalTermDomain "Terminology" |>.setDomainDescription technicalTermDomain "Definitions of technical terms" + |>.addQuickJumpMapper technicalTermDomain technicalTermDomainMapper traverse id data _contents := do -- A round with internal tags is not needed here because users's don't get to pick IDs diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index 504164bd7..7017a653f 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -537,11 +537,16 @@ def page + + + + {{extraJsFiles.map fun f => ({{}})}} {{extraStylesheets.map (fun url => {{ }})}} {{extraCss.toArray.map ({{}})}} {{extraJs.toArray.map ({{}})}} {{extraHead}} +
diff --git a/src/verso-manual/VersoManual/Html/Style.lean b/src/verso-manual/VersoManual/Html/Style.lean index 9445023a1..583d08bb7 100644 --- a/src/verso-manual/VersoManual/Html/Style.lean +++ b/src/verso-manual/VersoManual/Html/Style.lean @@ -39,6 +39,9 @@ def pageStyle : String := r####" /* How wide should the ToC be on non-mobile? */ --verso-toc-width: 18rem; + /** Selected items (e.g. search results) */ + --verso-selected-color: #def; + /** Variables that control the “burger menu” appearance **/ --verso-burger-height: 1.25rem; --verso-burger-width: 1.25rem; diff --git a/src/verso-search/VersoSearch.lean b/src/verso-search/VersoSearch.lean index a231f71ce..06e59ee43 100644 --- a/src/verso-search/VersoSearch.lean +++ b/src/verso-search/VersoSearch.lean @@ -15,6 +15,7 @@ import Lean.Data.Json import Verso.Doc import VersoSearch.PorterStemmer +import VersoSearch.DomainSearch open Std open Lean diff --git a/src/verso-search/VersoSearch/DomainSearch.lean b/src/verso-search/VersoSearch/DomainSearch.lean new file mode 100644 index 000000000..dbcdcf565 --- /dev/null +++ b/src/verso-search/VersoSearch/DomainSearch.lean @@ -0,0 +1,179 @@ +import Std.Data.HashMap +import VersoUtil.BinFiles + +open Std (HashMap) + +set_option linter.missingDocs true + +namespace Verso.Search + +/-- +Transforms data in a Verso documentation domain into a quick-jump item. +-/ +structure DomainMapper where + /-- + The name to be shown in the search UI, such as `"Compiler Option"` or `"Terminology"`. + -/ + displayName : String + /-- + The HTML class name to apply to results from the domain. + + Use `quickJumpCss` to apply CSS rules based on this class name. + -/ + className : String + /-- + JavaScript code to transform items from the domain's serialization in `xref.json` into searchable + items. + + Searchable items are JavaScript objects with the following fields: + * `searchKey` is the string used for fuzzy matching against the user's input + * `address` is the link target to be used when clicking on the search result + * `domainId` is the domain's name + * `ref` is a representation of the value itself, used for equality comparison in case of duplicate search keys + -/ + dataToSearchables : String + /-- + CSS to be used in the quick-jump box to customize results from the given domain. + -/ + quickJumpCss : Option String := none +deriving Repr, DecidableEq + +/-- +Constructs a domain mapper with default code for the `dataToSearchables` field. + +This default code is suitable when the canonical name of the object is the string that users should search for. +-/ +def DomainMapper.withDefaultJs (domain : Lean.Name) (displayName className : String) (css : Option String := none) : DomainMapper where + displayName := displayName + className := className + quickJumpCss := css + dataToSearchables := + "(domainData) => + Object.entries(domainData.contents).map(([key, value]) => ({ + searchKey: key, + address: `${value[0].address}#${value[0].id}`, + domainId: '" ++ domain.toString ++ "', + ref: value, + }))" + +open Std Format in +/-- +Generates JavaScript code for the provided domain mapper. +-/ +def DomainMapper.toJs (mapper : DomainMapper) : Std.Format := + nest 2 <| group <| + text "{" ++ line ++ + nest 2 (group ("dataToSearchables:" ++ line ++ mapper.dataToSearchables)) ++ "," ++ line ++ + nest 2 (group ("className:" ++ line ++ text mapper.className.quote)) ++ "," ++ line ++ + nest 2 (group ("displayName:" ++ line ++ text mapper.displayName.quote)) ++ line ++ + text "}" + +-- Objects could be included as literals, rather than defined, but that makes it more difficult to +-- debug the resulting JS code if needed. +section +private def isValidFirstChar (c : Char) : Bool := + c.isAlpha || c == '_' || c == '$' + +private def isValidIdChar (c : Char) : Bool := + c.isAlphanum || c == '_' || c == '$' + +private def jsReservedWords : List String := [ + "abstract", "arguments", "await", "boolean", "break", "byte", "case", "catch", + "char", "class", "const", "continue", "debugger", "default", "delete", "do", + "double", "else", "enum", "eval", "export", "extends", "false", "final", + "finally", "float", "for", "function", "goto", "if", "implements", "import", + "in", "instanceof", "int", "interface", "let", "long", "native", "new", + "null", "package", "private", "protected", "public", "return", "short", + "static", "super", "switch", "synchronized", "this", "throw", "throws", + "transient", "true", "try", "typeof", "var", "void", "volatile", "while", + "with", "yield" +] + + +private def isReservedWord (s : String) : Bool := + jsReservedWords.contains s + + +private def charToHex (c : Char) : String := + let code := c.toNat + let hex := Nat.toDigits 16 code + let hexString := hex.asString + -- Pad to at least 2 characters + if hexString.length = 1 then "0" ++ hexString else hexString + +/-- +Mangles a domain's name to that for its mapper, to be used in JS code. +-/ +private def jsName (domainName : String) : String := Id.run do + if domainName.isEmpty then return "_" + + let first := domainName.get! 0 + let mut out : String := + if isValidFirstChar first then + first.toString + else if first.isDigit then + "_".push first + else + "_x" ++ charToHex first + + let mut iter := domainName.iter.next + while h : iter.hasNext do + let c := iter.curr' h + iter := iter.next' h + if isValidIdChar c then + out := out.push c + else if c == '.' then + out := out ++ "_DOT_" + else + out := out ++ "_x" ++ charToHex c + + return if isReservedWord out then + out.push '_' + else + out +end + +/-- +A mapping from Verso domain names to their search customizations. +-/ +abbrev DomainMappers : Type := HashMap String DomainMapper + +open Std.Format in +/-- +Generates code for the provided collection of domain mappers, constructing a JS constant named +`domainMappers` that's suitable for the quick-jump feature. +-/ +def DomainMappers.toJs (mappers : DomainMappers) : Std.Format := + let ms := mappers.fold (init := nil) fun code dom m => code ++ line ++ line ++ gen dom m + let ms' := mappers.keys.map fun dom => nest 2 <| group <| text dom.quote ++ ":" ++ line ++ jsName dom + ms ++ line ++ line ++ + group (nest 2 ("export const domainMappers = {" ++ (text "," ++ line).joinSep ms') ++ line ++ "};") +where + gen (dom : String) (m : DomainMapper) := + text typeComment ++ line ++ + nest 2 (group (text "const " ++ text (jsName dom) ++ " = " ++ m.toJs ++ ";")) + + typeComment := "/**\n * @type {DomainMapper}\n */" + +/-- +Collects the CSS customizations for each domain. +-/ +def DomainMappers.quickJumpCss (mappers : DomainMappers) : String := + mappers.fold (init := "") fun css _ m => + match m.quickJumpCss with + | none => css + | some x => css ++ x ++ "\n" + + +section +open Verso.BinFiles + +/-- +The search box code +-/ +def searchBoxCode : Array (String × ByteArray):= + (include_bin_dir "../../../static-web/search").filterMap fun (name, contents) => + if name.endsWith "domain-mappers.js" then none + else some (name.stripPrefix "../../../static-web/search/", contents) + +end diff --git a/src/verso-util/VersoUtil.lean b/src/verso-util/VersoUtil.lean new file mode 100644 index 000000000..9fd583fd0 --- /dev/null +++ b/src/verso-util/VersoUtil.lean @@ -0,0 +1 @@ +import VersoUtil.BinFiles diff --git a/src/verso/Verso/BinFiles.lean b/src/verso-util/VersoUtil/BinFiles.lean similarity index 99% rename from src/verso/Verso/BinFiles.lean rename to src/verso-util/VersoUtil/BinFiles.lean index 326e25710..e8bc24016 100644 --- a/src/verso/Verso/BinFiles.lean +++ b/src/verso-util/VersoUtil/BinFiles.lean @@ -5,7 +5,7 @@ Author: David Thrane Christiansen -/ import Lean.Elab.Eval import Lean.Elab.Term -import Verso.BinFiles.Z85 +import VersoUtil.BinFiles.Z85 open Lean Elab Term open Lean Environment diff --git a/src/verso/Verso/BinFiles/Z85.lean b/src/verso-util/VersoUtil/BinFiles/Z85.lean similarity index 100% rename from src/verso/Verso/BinFiles/Z85.lean rename to src/verso-util/VersoUtil/BinFiles/Z85.lean diff --git a/src/verso/Verso/Output/Html/KaTeX.lean b/src/verso/Verso/Output/Html/KaTeX.lean index 50722d8f0..7c54fb894 100644 --- a/src/verso/Verso/Output/Html/KaTeX.lean +++ b/src/verso/Verso/Output/Html/KaTeX.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import Verso.BinFiles +import VersoUtil.BinFiles open Verso.BinFiles diff --git a/static-web/search/README.txt b/static-web/search/README.txt new file mode 100644 index 000000000..a4ddf6f6c --- /dev/null +++ b/static-web/search/README.txt @@ -0,0 +1,57 @@ +# Search bar for Verso manuals + +To type check: `tsc -p ./jsconfig.json`. + +## Libraries + +I've added a few libraries to develop faster. + +I picked up `fuzzysort` for fuzzy sorting from the github page +(https://github.com/farzher/fuzzysort) where he has a minified version next to +the implementation. + +I picked up `unicode-input.min.js` from +https://cdn.skypack.dev/@leanprover/unicode-input - had to download it from the +network tab in the browser. It's a dependency of `unicode-input-component.js`. + +I picked up `unicode-input-component.js` from +https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input-component/src/index.ts, +but that needs to changed some in order for it to work without compiling, so if +it needs to be updated look at the diff to understand what's required. + +# Research + +The Lean search bar has some properties that make it hard to use already +existing libraries for search bars directly. Almost all online search bars +require multiple libraries - I haven't been able to find one that didn't. And we +don't want dependents on this component to have to install node/npm/tons of +libraries in order to use it. It should be simple. + +Additionally, the data is in a complex format, and has to be able to run +locally, so doing serverside search is off the table. + +## Fuzzy search js library investigation + +Looking at fuzzy search libraries. The important things are: + +- Size - it should be small. +- Correctness - it should work. +- Single word/multiword? +- Offload to web worker? + +#### https://www.npmjs.com/package/fuzzysort + +Looks slick. Same kind of search as in Sublime Text. Probably makes more sense +for programming things than the other things here. + +## Combobox libraries + +Maybe have a look at +https://www.digitala11y.com/accessible-ui-component-libraries-roundup/ + +https://webaim.org/ is a good place to look + +### https://www.w3.org/WAI/ARIA/apg/patterns/combobox/examples/combobox-autocomplete-both/ + +I've found this w3 aria example, which I'm going to use and adjust to our needs. +That's a good place to start. diff --git a/static-web/search/fuzzysort.d.ts b/static-web/search/fuzzysort.d.ts new file mode 100644 index 000000000..7516a89e9 --- /dev/null +++ b/static-web/search/fuzzysort.d.ts @@ -0,0 +1,105 @@ +declare namespace Fuzzysort { + interface Result { + /** + * 1 is a perfect match. 0.5 is a good match. 0 is no match. + */ + readonly score: number; + + /** Your original target string */ + readonly target: string; + + highlight(highlightOpen?: string, highlightClose?: string): string; + highlight(callback: HighlightCallback): (string | T)[]; + + indexes: ReadonlyArray; + } + interface Results extends ReadonlyArray { + /** Total matches before limit */ + readonly total: number; + } + + interface KeyResult extends Result { + /** Your original object */ + readonly obj: T; + } + interface KeyResults extends ReadonlyArray> { + /** Total matches before limit */ + readonly total: number; + } + + interface KeysResult extends ReadonlyArray { + /** + * 1 is a perfect match. 0.5 is a good match. 0 is no match. + */ + readonly score: number; + + /** Your original object */ + readonly obj: T; + } + interface KeysResults extends ReadonlyArray> { + /** Total matches before limit */ + readonly total: number; + } + + interface Prepared { + /** Your original target string */ + readonly target: string; + } + + interface Options { + /** Don't return matches worse than this (higher is faster) */ + threshold?: number; + + /** Don't return more results than this (lower is faster) */ + limit?: number; + + /** If true, returns all results for an empty search */ + all?: boolean; + } + interface KeyOptions extends Options { + key: string | ((obj: T) => string) | ReadonlyArray; + } + interface KeysOptions extends Options { + keys: ReadonlyArray string) | ReadonlyArray>; + scoreFn?: (keysResult: KeysResult) => number; + } + + interface HighlightCallback { + (match: string, index: number): T; + } + + interface Fuzzysort { + single(search: string, target: string | Prepared): Result | null; + + go( + search: string, + targets: ReadonlyArray, + options?: Options + ): Results; + go( + search: string, + targets: ReadonlyArray, + options: KeyOptions + ): KeyResults; + go( + search: string, + targets: ReadonlyArray, + options: KeysOptions + ): KeysResults; + + /** + * Help the algorithm go fast by providing prepared targets instead of raw strings + */ + prepare(target: string): Prepared; + + /** + * Free memory caches if you're done using fuzzysort for now + */ + cleanup(): void; + } +} + +declare module "fuzzysort" { + const fuzzysort: Fuzzysort.Fuzzysort; + export = fuzzysort; +} diff --git a/static-web/search/fuzzysort.js b/static-web/search/fuzzysort.js new file mode 100644 index 000000000..5f61751ef --- /dev/null +++ b/static-web/search/fuzzysort.js @@ -0,0 +1,2 @@ +// https://github.com/farzher/fuzzysort v3.1.0 +((r,e)=>{"function"==typeof define&&define.amd?define([],e):"object"==typeof module&&module.exports?module.exports=e():r.fuzzysort=e()})(this,c=>{var f=r=>{"number"==typeof r?r=""+r:"string"!=typeof r&&(r="");var e=u(r);return x(r,{t:e.i,o:e.v,u:e.l})};class M{get["indexes"](){return this.p.slice(0,this.p.g).sort((r,e)=>r-e)}set["indexes"](r){return this.p=r}["highlight"](r,e){return((r,e="",f="")=>{for(var t="function"==typeof e?e:void 0,i=r.target,a=i.length,o=r.indexes,n="",v=0,u=0,s=!1,l=[],c=0;c{var f=new M;return f.target=r,f.obj=e.obj??Q,f.h=e.h??O,f.p=e.p??[],f.t=e.t??"",f.o=e.o??Q,f.k=e.k??Q,f.u=e.u??0,f},e=r=>r===O?0:10===r?O:1{"number"==typeof r?r=""+r:"string"!=typeof r&&(r=""),r=r.trim();var e=u(r),f=[];if(e.S)for(var t,i=r.split(/\s+/),i=[...new Set(i)],a=0;a{var e;return 999{var e;return 999{if(!1===f&&r.S)return C(r,e,t);for(var f=r.i,i=r.v,a=i[0],o=e.o,n=i.length,v=o.length,u=0,s=0,l=0;;){if(a===o[s]){if(q[l++]=s,++u===n)break;a=i[u]}if(v<=++s)return Q}var u=0,c=!1,p=0,b=e.k,d=(b===Q&&(b=e.k=N(e.target)),0);if((s=0===q[0]?0:b[q[0]-1])!==v)for(;;)if(v<=s){if(u<=0)break;if(200<++d)break;--u;var w=z[--p],s=b[w]}else if(i[u]===o[s]){if(z[p++]=s,++u===n){c=!0;break}++s}else s=b[s];var g=n<=1?-1:e.t.indexOf(f,q[0]),h=!!~g,y=h&&(0===g||e.k[g-1]===g);if(h&&!y)for(var k=0;k{for(var e=0,f=0,t=1;t{for(var t=new Set,i=0,a=Q,o=0,n=r._,v=n.length,u=0,s=()=>{for(let r=u-1;0<=r;r--)e.k[S[2*r+0]]=S[2*r+1]},l=!1,c=0;ci){if(f)for(c=0;cr.replace(/\p{Script=Latin}+/gu,r=>r.normalize("NFD")).replace(/[\u0300-\u036f]/g,""),u=r=>{for(var e=(r=v(r)).length,f=r.toLowerCase(),t=[],i=0,a=!1,o=0;o{for(var e=r.length,f=[],t=0,i=!1,a=!1,o=0;o{for(var e=(r=v(r)).length,f=s(r),t=[],i=f[0],a=0,o=0;o{var f=r[e];if(void 0!==f)return f;if("function"==typeof e)return e(r);for(var t=e,i=(t=Array.isArray(e)?t:e.split(".")).length,a=-1;r&&++a"object"==typeof r&&"number"==typeof r.u,K=1/0,O=-K,P=[],Q=(P.total=0,null),R=f(""),T=(o=[],n=0,t=r=>{for(var e=o[i=0],f=1;f>1]=o[i],f=1+(i<<1)}for(var a=i-1>>1;0>1)o[i]=o[a];o[i]=e},(r={}).add=r=>{var e=n;o[n++]=r;for(var f=e-1>>1;0>1)o[e]=o[f];o[e]=r},r.m=r=>{var e;if(0!==n)return e=o[0],o[0]=o[--n],t(),e},r.M=r=>{if(0!==n)return o[0]},r.C=r=>{o[0]=r,t()},r);return{single:(r,e)=>{var f;return!r||!e||(r=D(r),J(e)||(e=L(e)),((f=r.l)&e.u)!==f)?Q:F(r,e)},go:(r,e,f)=>{if(!r)return f?.all?((r,e)=>{var f=[],t=(f.total=r.length,e?.limit||K);if(e?.key)for(var i=0;i=t)return f}else if(e?.keys)for(var i=0;i=0;--u){var o=I(a,e.keys[u]);if(!o){v[u]=R;continue}if(!J(o))o=L(o);o.h=O;o.p.g=0;v[u]=o}v.obj=a;v.h=O;f.push(v);if(f.length>=t)return f}else for(var i=0;i=t)return f}return f})(e,f):P;var t=D(r),i=t.l,a=t.S,o=A(f?.threshold||0),n=f?.limit||K,v=0,u=0,s=e.length;function l(r){vT.M().h&&T.C(r))}if(f?.key)for(var c=f.key,p=0;pO&&(_=(B[r]+E[r])/4)>B[r]&&(B[r]=_),E[r]>B[r]&&(B[r]=E[r]);if(a){for(let r=0;r{a.clear(),l.clear()}}}); diff --git a/static-web/search/jsconfig.json b/static-web/search/jsconfig.json new file mode 100644 index 000000000..0ba50acaf --- /dev/null +++ b/static-web/search/jsconfig.json @@ -0,0 +1,8 @@ +{ + "compilerOptions": { + "typeRoots": ["."], + "lib": ["ES2024", "DOM", "DOM.Iterable"], + "target": "ES2024", + "noEmit": true + } +} \ No newline at end of file diff --git a/static-web/search/licenses.md b/static-web/search/licenses.md new file mode 100644 index 000000000..76bb76b9d --- /dev/null +++ b/static-web/search/licenses.md @@ -0,0 +1,41 @@ +# 3rd party copyright statement + +The following third party software is included in the search box, and is +provided under the following license terms. + +## W3 combobox + +By obtaining and/or copying this work, you (the licensee) agree that you have +read, understood, and will comply with the following terms and conditions. + +Permission to copy, modify, and distribute this work, with or without +modification, for any purpose and without fee or royalty is hereby granted, +provided that you include the following on ALL copies of the work or portions +thereof, including modifications: + + The full text of this NOTICE in a location viewable to users of the redistributed or derivative work. + Any pre-existing intellectual property disclaimers, notices, or terms and conditions. If none exist, the W3C software and document short notice should be included. + Notice of any changes or modifications, through a copyright statement on the new code or document such as "This software or document includes material copied from or derived from [title and URI of the W3C document]. Copyright © [$year-of-document] World Wide Web Consortium. https://www.w3.org/copyright/software-license-2023/" + +## Fuzzysort + +MIT License + +Copyright (c) 2018 Stephen Kamenar + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +the Software, and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/static-web/search/search-box.css b/static-web/search/search-box.css new file mode 100644 index 000000000..1a66ab3f0 --- /dev/null +++ b/static-web/search/search-box.css @@ -0,0 +1,254 @@ +/** + * Copyright (c) 2024 Lean FRO LLC. All rights reserved. + * Released under Apache 2.0 license as described in the file LICENSE. + * Author: Jakob Ambeck Vase + */ + + :root { + --selected-color: var(--verso-selected-color, #def); +} + +@media screen and (700px < width) { + :root { + --search-bar-width: 24rem; + } +} + +@media screen and (width <= 700px) { + :root { + --search-bar-width: 12rem; + } +} + +#search-wrapper .combobox-list { + position: relative; +} + +#search-wrapper .combobox .group { + display: flex; + cursor: pointer; +} + +#search-wrapper .combobox .cb_edit { + background-color: white; + color: black; + box-sizing: border-box; + padding: 0; + margin: 0; + vertical-align: bottom; + border: none; + border-bottom: 1px solid gray; + position: relative; + cursor: pointer; + width: var(--search-bar-width); + outline: none; + font-size: .9rem; + padding: .3rem .5rem; + font-family: system-ui, sans-serif; + /* Fix firefox eating spaces in textContent */ + white-space: -moz-pre-space; +} + +#search-wrapper .combobox .group.focus .cb_edit, +#search-wrapper .combobox .group .cb_edit:hover { + background-color: var(--selected-color); + outline: auto; +} + +/* Make the `placeholder` attribute visible even though the search + box is a div. */ +#search-wrapper .cb_edit:empty:before { + content: attr(placeholder); + pointer-events: none; + color: #888; + font-family: sans-serif; + display: block; +} + +#search-wrapper ul[role="listbox"] { + margin: 0; + padding: 0; + position: absolute; + top: calc(100%); + width: var(--search-bar-width); + list-style: none; + background-color: white; + display: none; + box-sizing: border-box; + border: 2px currentcolor solid; + max-height: 20rem; + overflow: scroll; + overflow-x: hidden; + font-size: .9rem; + z-index: 100; +} + +/* Applies to all `li` in the box, including "no results" and "showing x/y" */ +#search-wrapper ul[role="listbox"] li { + font-family: sans-serif; + padding: .2rem; + margin: 0; +} + +#search-wrapper .search-result { + display: flex; + flex-direction: column; + gap: .2rem; + + font-weight: 400; + cursor: pointer; + + /* Make the 'Showing 1/2 results' visible when navigating with keyboard. */ + scroll-margin-bottom: 1.2rem; +} + +/* Couple the domain tighter with the search term on smaller screens, + otherwise it's easy to get lost in the results. */ +@media screen and (max-width: 700px) { + #search-wrapper .search-result { + gap: 0; + padding: .3rem .2rem; + } +} + +#search-wrapper .search-result.doc-domain, +#search-wrapper .search-result.option-domain, +#search-wrapper .search-result.syntax-domain, +#search-wrapper .search-result.lake-option-domain, +#search-wrapper .search-result.lake-toml-table-domain, +#search-wrapper .search-result.lake-toml-field-domain, +#search-wrapper .search-result.elan-option-domain, +#search-wrapper .search-result.env-var-domain, +#search-wrapper .search-result.lake-command-domain, +#search-wrapper .search-result.error-explanation-domain, +#search-wrapper .search-result.elan-command-domain { + font-family: var(--verso-code-font-family); +} + +#search-wrapper .search-result.full-text { + font-family: var(--verso-text-font-family); +} +#search-wrapper .search-result.full-text .header { + display: block; +} +#search-wrapper .search-result.full-text .header, +#search-wrapper .search-result.full-text .header em { + font-style: normal; + font-family: var(--verso-structure-font-family); + font-weight: bold; +} + +#search-wrapper .search-result.tactic-domain, +#search-wrapper .search-result.conv-tactic-domain { + font-family: var(--verso-code-font-family); + font-weight: bold; +} + +#search-wrapper .search-result.tech-term-domain { + font-family: var(--verso-text-font-family); +} + +#search-wrapper .search-result.section-domain { + font-family: var(--verso-structure-font-family); + font-weight: bold; +} + +#search-wrapper [role="listbox"].focus li[aria-selected="true"], +#search-wrapper .search-result:hover { + background-color: var(--selected-color); + padding-bottom: calc(.2rem - 1px); + padding-top: calc(.2rem - 1px); + border-bottom: 1px solid currentColor; + border-top: 1px solid currentColor; +} + +/* Couple the domain tighter with the search term on smaller screens, + otherwise it's easy to get lost in the results. */ +@media screen and (max-width: 700px) { +#search-wrapper [role="listbox"].focus li[aria-selected="true"], +#search-wrapper .search-result:hover { + padding-bottom: calc(.3rem - 1px); + padding-top: calc(.3rem - 1px); + } +} + +#search-wrapper .search-result p { + margin: 0; + font-family: inherit; + font-weight: inherit; + font-style: inherit; +} + +#search-wrapper .search-result em { + font-style: normal; + text-decoration: underline; +} + +#search-wrapper .search-result .domain em { + font-style: italic; +} + +#search-wrapper .search-result .domain { + text-align: right; + color: #777; + font-style: italic; + font-family: var(--verso-structure-font-family); + font-weight: normal; + font-size: .7rem; +} + +#search-wrapper .search-result .domain.text-context { + /* For full-text search results, truncate on the left with an ellipsis */ + text-overflow: ellipsis; + direction: rtl; + white-space: nowrap; + overflow: hidden; +} + +#search-wrapper .search-result .domain .context-elem { + display: inline-block; +} + +#search-wrapper .search-result .domain .context-elem:not(:last-child)::after { + content: "»"; + margin: 0 0.25em; +} + +/* Couple the domain tighter with the search term on smaller screens, + otherwise it's easy to get lost in the results. */ +@media screen and (max-width: 700px) { + #search-wrapper .search-result .domain { + text-align: left; + } +} + +#search-wrapper .more-results { + text-align: center; + color: #777; + font-size: .7rem; +} + +#search-wrapper .domain-filter label { + display: flex; + gap: .5rem +} + +#search-wrapper .domain-filter input { + flex-basis: 2rem; +} + +/* Page layout */ +#search-wrapper { + width: fit-content; + z-index: 1; + position: absolute; + top: 0; + right: 0; + bottom: 0; + padding: 0 .5rem; + display: flex; + flex-direction: column; + justify-content: center; + align-items: center; + background-color: white; +} diff --git a/static-web/search/search-box.js b/static-web/search/search-box.js new file mode 100644 index 000000000..59cdd9c4c --- /dev/null +++ b/static-web/search/search-box.js @@ -0,0 +1,1165 @@ +/** + * Copyright (c) 2024 Lean FRO LLC. All rights reserved. + * Released under Apache 2.0 license as described in the file LICENSE. + * Author: Jakob Ambeck Vase + * + * This software or document includes material copied from or derived from https://www.w3.org/WAI/ARIA/apg/patterns/combobox/examples/combobox-autocomplete-both/. + * Copyright © 2024 World Wide Web Consortium. https://www.w3.org/copyright/software-license-2023/ + */ + +// Enable typescript +// @ts-check + +import { Range } from "./unicode-input.min.js"; +import { InputAbbreviationRewriter } from "./unicode-input-component.min.js"; + +// Hacky way to import the fuzzysort library and get the types working. It's just `window.fuzzysort`. +const fuzzysort = /** @type {{fuzzysort: Fuzzysort.Fuzzysort}} */ ( + /** @type {unknown} */ (window) +).fuzzysort; + +const searchIndex = /** @type {{searchIndex: TextSearchIndex}} */ ( + /** @type {unknown} */ (window) +).searchIndex; + + +/** Whether to search word prefixes or whole words in full-text searches. Should match the setting in search-highlight.js. + * @type {boolean} + */ +const expandMatches = true; + +/** + * Type definitions to help if you have typescript enabled. + * + * @typedef {{searchKey: string, address: string, domainId: string, ref?: any}} Searchable + * @typedef {(domainData: any) => Searchable[]} DomainDataToSearchables + * @typedef {{t: 'text', v: string} | {t: 'highlight', v: string}} MatchedPart + * @typedef {(searchable: Searchable, matchedParts: MatchedPart[], document: Document) => HTMLElement} CustomResultRender + * @typedef {{dataToSearchables: DomainDataToSearchables, customRender?: CustomResultRender, displayName: string, className: string}} DomainMapper + * @typedef {Record} DomainMappers + * @typedef {{ref: string, score: number, doc: {id: string, header: string, context: string, contents: string}}} TextMatch + * @typedef {{item: Searchable, fuzzysortResult: Fuzzysort.Result, htmlItem: HTMLLIElement}|{terms: string, textItem: TextMatch, htmlItem: HTMLLIElement}} SearchResult + * @typedef {{run: (tokens: string[]) => string[]}} ElasticLunrPipeline + * @typedef {{bool?: "AND"|"OR", fields?:Record, expand?: boolean}} SearchConfig + * @typedef {{search: ((term: string, config: SearchConfig) => TextMatch[]), pipeline: ElasticLunrPipeline}|undefined|null} TextSearchIndex + * @typedef {{original: string, stem: string, start: number, end: number}} TextToken + * @typedef {{start: number, end: number, index: number, matches: TextToken[]}} TextSnippet + */ + +/** + * @param {TextSnippet} s1 + * @param {TextSnippet} s2 + * @return {number} + */ +const compareSnippets = (s1, s2) => { + // First compare by number of unique terms + let terms1 = new Set(s1.matches.map((x) => x.stem)); + let terms2 = new Set(s2.matches.map((x) => x.stem)); + let terms = terms1.size - terms2.size; + if (terms !== 0) { + return terms; + } + + // Then by number of matches + let matches = s1.matches.length - s2.matches.length; + if (matches !== 0) { + return matches; + } + + // Finally by index + return s1.index - s2.index; +}; + +/** + * @param {string} text + * @return {TextToken[]} + */ +const tokenizeText = (text) => { + /** @type {TextToken[]} */ + const toks = []; + const regex = /\S+/g; + let match; + while ((match = regex.exec(text)) !== null) { + let stems = searchIndex.pipeline.run([match[0]]); + for (const stem of stems) { + toks.push({ + original: match[0], + start: match.index, + end: match.index + match[0].length, + stem: stem.toLowerCase() + }); + } + } + return toks; +} + +/** + * @type {RegExp} + */ +const wordChar = /\p{L}/u + +/** + * @param {string} text + * @param {number} i + * @return {number} + */ +const wordStartBefore = (text, i) => { + while (i > 0) { + if (!wordChar.test(text[i])) return i + 1; /* Adjust due to start indices being inclusive */ + i--; + } + return i; +} + +/** + * @param {string} text + * @param {number} i + * @return {number} + */ +const wordEndAfter = (text, i) => { + while (i < text.length) { + if (!wordChar.test(text[i])) return i; /* This is used as the (exclusive) end index in a slice, so one greater is correct */ + i++; + } + return i; +} + +/** + * @param {string} text + * @param {string} query + * @param {{contextLength?: number, maxSnippets?: number}} options + * @return {Element|null} +*/ +const highlightTextResult = (text, query, options = {}) => { + const { + contextLength = 50, // characters of context around each match + maxSnippets = 3 // maximum number of snippets to return + } = options; + + const terms = searchIndex.pipeline.run(query.trim().toLowerCase().split(/\s+/).filter(term => term.length > 0)); + const toks = tokenizeText(text); + const matches = expandMatches ? toks.filter(t => terms.some(tm => t.stem.startsWith(tm))) : toks.filter(t => terms.includes(t.stem)); + + if (matches.length === 0) { + return null; // No matches found + } + + // Group nearby matches into snippets + /** @type {TextSnippet[]} */ + const snippets = []; + let currentSnippet = null; + for (const match of matches) { + if (!currentSnippet || match.start > currentSnippet.end + contextLength * 2) { + // Start new snippet + currentSnippet = { + start: wordStartBefore(text, Math.max(0, match.start - contextLength)), + end: wordEndAfter(text, Math.min(text.length, match.end + contextLength)), + index: snippets.length, + matches: [match] + }; + snippets.push(currentSnippet); + } else { + // Extend current snippet + currentSnippet.end = wordEndAfter(text, Math.min(text.length, match.end + contextLength)); + currentSnippet.matches.push(match); + } + } + + // Limit number of snippets. First, sort them by quality (which takes unique term occurrences and + // total term count into consideration), then take the N best, then put them back in document order. + const limitedSnippets = snippets.sort(compareSnippets).slice(0, maxSnippets).sort((s1, s2) => s1.index - s2.index); + + // Generate highlighted text for each snippet + const highlightedSnippets = limitedSnippets.map((snippet) => { + let snippetText = text.substring(snippet.start, snippet.end); + + // Adjust match positions relative to snippet start + const relativeMatches = snippet.matches.map(match => ({ + term: match.original, + start: match.start - snippet.start, + end: match.end - snippet.start + })); + + // Sort matches by position (descending) to avoid position shifts during replacement + relativeMatches.sort((a, b) => b.start - a.start); + + // Apply highlighting + for (const match of relativeMatches) { + const before = snippetText.substring(0, match.start); + const highlighted = `${match.term}`; + const after = snippetText.substring(match.end); + snippetText = before + highlighted + after; + } + + // Add ellipses + const prefix = snippet.start > 0 ? ' …' : ''; + const suffix = snippet.end < text.length ? '… ' : ''; + + const elem = document.createElement("span"); + elem.appendChild(document.createTextNode(prefix)); + const m = document.createElement("span"); + m.innerHTML = snippetText; + elem.appendChild(m); + elem.appendChild(document.createTextNode(suffix)); + return elem; + }); + + const elem = document.createElement("span"); + elem.append(...highlightedSnippets); + return elem; +} + +/** + * Maps data from Lean to an object with search terms as keys and a list of results as values. + * + * @param {any} json + * @param {DomainMappers} domainMappers + * @return {Record} + */ +const dataToSearchableMap = (json, domainMappers) => + Object.entries(json) + .flatMap(([key, value]) => + key in domainMappers + ? domainMappers[key].dataToSearchables(value) + : undefined + ) + .reduce((acc, cur) => { + if (cur == null) { + return acc; + } + + if (!acc.hasOwnProperty(cur.searchKey)) { + acc[cur.searchKey] = []; + } + acc[cur.searchKey].push(cur); + return acc; + }, {}); + +/** + * Maps from a data item to a HTML LI element + * + * @param {DomainMappers} domainMappers + * @param {Searchable} searchable + * @param {MatchedPart[]} matchedParts + * @param {Document} document + * @return {HTMLLIElement} + */ +const searchableToHtml = ( + domainMappers, + searchable, + matchedParts, + document +) => { + const domainMapper = domainMappers[searchable.domainId]; + + const li = document.createElement("li"); + li.role = "option"; + li.className = `search-result ${domainMapper.className}`; + li.title = `${domainMapper.displayName} ${searchable.searchKey}`; + + if (domainMapper.customRender != null) { + li.appendChild( + domainMapper.customRender(searchable, matchedParts, document) + ); + } else { + const searchTerm = document.createElement("p"); + for (const { t, v } of matchedParts) { + if (t === "text") { + searchTerm.append(v); + } else { + const emEl = document.createElement("em"); + searchTerm.append(emEl); + emEl.textContent = v; + } + } + li.appendChild(searchTerm); + } + + const domainName = document.createElement("p"); + li.appendChild(domainName); + domainName.className = "domain"; + domainName.textContent = domainMapper.displayName; + + return li; +}; + +/** + * Maps from a data item to a HTML LI element + * @param {string} term + * @param {TextMatch} match + * @param {Document} document + * @return {HTMLLIElement|null} + */ +const textResultToHtml = ( + term, + match, + document +) => { + const li = document.createElement("li"); + li.role = "option"; + li.className = `search-result full-text`; + li.title = "Full-text search result" + // DEBUG: + // li.title = `Full-text search result (${match.score}) (${match.ref})`; + + const searchTerm = document.createElement("p"); + let inHeader = true; + let headerHl = highlightTextResult(match.doc.header, term, {contextLength: 30}); // Only abbreviate huge headers + if (!headerHl) { + inHeader = false; + headerHl = document.createElement("span"); + headerHl.append(document.createTextNode(match.doc.header)); + } + headerHl.className = "header"; + searchTerm.append(headerHl); + let contentHl = highlightTextResult(match.doc.contents, term, {contextLength: 10}); + if (!contentHl) { + if (!inHeader) { + // Exclude this result. It'd be cleaner to do this elsewhere, but duplicating the string + // processing would be expensive. + return null; + } + contentHl = document.createElement("span"); + contentHl.appendChild(document.createTextNode("...")); + for (const t of term.split(/\s+/)) { + const tm = document.createElement("em"); + tm.appendChild(document.createTextNode(t)); + contentHl.appendChild(tm); + contentHl.appendChild(document.createTextNode("...")); + } + } + searchTerm.append(contentHl); + li.appendChild(searchTerm); + + const domainName = document.createElement("p"); + li.appendChild(domainName); + domainName.className = "domain"; + if (match.doc.context.trim() == "") { + domainName.textContent = "Full-text search"; + } else { + // This is a slight abuse of "domain", but it seems to work well + let context = match.doc.context.replaceAll("\t", " » "); + domainName.append(document.createTextNode(context)); + domainName.classList.add('text-context'); + } + + return li; +}; + +/** + * @param {SearchResult} result + * @returns string + */ +const resultToText = (result) => { + if ("fuzzysortResult" in result) { + return result.fuzzysortResult.target; + } else { + return result.terms; + } +} + +/** + * @template T + * @template Y + * @param {T | null | undefined} v + * @param {(t: T) => Y} fn + * @returns Y | undefined + */ +const opt = (v, fn) => (v != null ? fn(v) : undefined); + +/** + * This is a modified version of the combobox at https://www.w3.org/WAI/ARIA/apg/patterns/combobox/examples/combobox-autocomplete-both/ + * + * The license for the combobox is in `licenses.md`. + */ +class SearchBox { + /** + * @type {HTMLDivElement} + */ + comboboxNode; + + /** + * @type {HTMLButtonElement | null} + */ + buttonNode; + + /** + * @type {HTMLElement} + */ + listboxNode; + + /** + * @type {boolean} + */ + comboboxHasVisualFocus; + + /** + * @type {boolean} + */ + listboxHasVisualFocus; + + /** + * @type {boolean} + */ + hasHover; + + /** + * @type {SearchResult | null} + */ + currentOption; + + /** + * @type {SearchResult | null} + */ + firstOption; + + /** + * @type {SearchResult | null} + */ + lastOption; + + /** + * @type {SearchResult[]} + */ + filteredOptions; + + /** + * @type {string} + */ + filter; + + /** + * @type {Fuzzysort.Prepared[]} + */ + preparedData; + + /** + * Map from search term to list of results + * + * @type {Record} + */ + mappedData; + + /** @type {HTMLLIElement} */ + noResultsElement = document.createElement("li"); + + /** @type {HTMLLIElement[]} */ + domainFilters; + + /** @type {DomainMappers} */ + domainMappers; + + /** @type {InputAbbreviationRewriter} */ + imeRewriter; + + /** + * @param {HTMLDivElement} comboboxNode + * @param {HTMLButtonElement | null} buttonNode + * @param {HTMLElement} listboxNode + * @param {DomainMappers} domainMappers + * @param {Record} mappedData + */ + constructor( + comboboxNode, + buttonNode, + listboxNode, + domainMappers, + mappedData + ) { + this.comboboxNode = comboboxNode; + this.buttonNode = buttonNode; + this.listboxNode = listboxNode; + this.domainMappers = domainMappers; + this.mappedData = mappedData; + this.preparedData = Object.keys(this.mappedData).map((name) => + fuzzysort.prepare(name) + ); + + // Add IME + this.imeRewriter = new InputAbbreviationRewriter( + { + abbreviationCharacter: "\\", + customTranslations: [], + eagerReplacementEnabled: true, + }, + comboboxNode + ); + + // Initialize with a full-text result's query, if one is being presented + const query = new URLSearchParams(window.location.search).get('terms')?.trim(); + comboboxNode.textContent = query ? query : ""; + + + + this.comboboxHasVisualFocus = false; + this.listboxHasVisualFocus = false; + + this.hasHover = false; + + this.currentOption = null; + this.firstOption = null; + this.lastOption = null; + + this.filteredOptions = []; + this.filter = ""; + + this.comboboxNode.addEventListener( + "keydown", + this.onComboboxKeyDown.bind(this) + ); + this.comboboxNode.addEventListener( + "keyup", + this.onComboboxKeyUp.bind(this) + ); + this.comboboxNode.addEventListener( + "click", + this.onComboboxClick.bind(this) + ); + this.comboboxNode.addEventListener( + "focus", + this.onComboboxFocus.bind(this) + ); + this.comboboxNode.addEventListener("blur", this.onComboboxBlur.bind(this)); + + document.body.addEventListener( + "pointerup", + this.onBackgroundPointerUp.bind(this), + true + ); + + // initialize pop up menu + + this.listboxNode.addEventListener( + "pointerover", + this.onListboxPointerover.bind(this) + ); + this.listboxNode.addEventListener( + "pointerout", + this.onListboxPointerout.bind(this) + ); + + this.domainFilters = []; + const docDomainFilter = document.createElement("li"); + docDomainFilter.innerHTML = ``; + docDomainFilter.classList.add("domain-filter"); + // TODO more work on the domain filters + // this.domainFilters.push(docDomainFilter); + + this.setValue(query ? query : ""); + + // Open Button + + const button = this.comboboxNode.nextElementSibling; + + if (button && button.tagName === "BUTTON") { + button.addEventListener("click", this.onButtonClick.bind(this)); + } + + this.noResultsElement.textContent = "No results"; + } + + /** + * @param {HTMLLIElement | null | undefined} option + */ + setActiveDescendant(option) { + if (option && this.listboxHasVisualFocus) { + this.comboboxNode.setAttribute("aria-activedescendant", option.id); + option.scrollIntoView({ behavior: "instant", block: "nearest" }); + } else { + this.comboboxNode.setAttribute("aria-activedescendant", ""); + } + } + + /** + * @param {string} itemAddress + * @param {string|null} query + */ + confirmResult(itemAddress, query=null) { + query = query ? "?terms=" + encodeURIComponent(query) : ""; + const [addr, id] = itemAddress.split('#', 2); + itemAddress = id? addr + query + '#' + id : addr + query; + + const base = document.querySelector('base'); + if (base) { + let baseNoSlash = base.href.endsWith("/") ? base.href.slice(0, -1) : base.href; + let itemAddressNoSlash = itemAddress.startsWith("/") ? itemAddress.slice(1) : itemAddress; + window.location.assign(baseNoSlash + '/' + itemAddressNoSlash); + } else { + window.location.assign(itemAddress); + } + } + + /** + * @param {string} value + */ + setValue(value) { + this.filter = value; + this.comboboxNode.textContent = this.filter; + this.imeRewriter.setSelections([new Range(this.filter.length, 0)]); + } + + /** + * @param {SearchResult} option + */ + setOption(option) { + if (option) { + this.currentOption = option; + this.setCurrentOptionStyle(this.currentOption); + this.setActiveDescendant(this.currentOption.htmlItem); + } + } + + setVisualFocusCombobox() { + this.listboxNode.classList.remove("focus"); + this.comboboxNode.parentElement?.classList.add("focus"); // set the focus class to the parent for easier styling + this.comboboxHasVisualFocus = true; + this.listboxHasVisualFocus = false; + this.setActiveDescendant(null); + } + + setVisualFocusListbox() { + this.comboboxNode.parentElement?.classList.remove("focus"); + this.comboboxHasVisualFocus = false; + this.listboxHasVisualFocus = true; + this.listboxNode.classList.add("focus"); + this.setActiveDescendant(this.currentOption?.htmlItem); + } + + removeVisualFocusAll() { + this.comboboxNode.parentElement?.classList.remove("focus"); + this.comboboxHasVisualFocus = false; + this.listboxHasVisualFocus = false; + this.listboxNode.classList.remove("focus"); + this.currentOption = null; + this.setActiveDescendant(null); + } + + // ComboboxAutocomplete Events + + filterOptions() { + const currentOptionText = opt(this.currentOption, resultToText); + const filter = this.filter; + + // Empty the listbox + this.listboxNode.textContent = ""; + + this.listboxNode.append(...this.domainFilters); + + if (filter.length === 0) { + this.filteredOptions = []; + this.firstOption = null; + this.lastOption = null; + this.currentOption = null; + return null; + } + + let results = fuzzysort.go(filter, this.preparedData, { + limit: 30, + threshold: 0.25, + }); + + const textResults = searchIndex ? searchIndex.search(filter, {expand: expandMatches, bool: "AND", fields: {header: {boost: 1.25}, contents: {boost: 1}, context: {boost: 0.1} }}) : []; + + // Normalize the scores for text results by capping at a threshold, to better integrate with fuzzysearch results + const bestPossibleText = 0.8; + const maxTextScore = textResults.reduce((max, item) => Math.max(max, item.score), -Infinity); + if (maxTextScore > bestPossibleText) { + const factor = bestPossibleText / maxTextScore; + for (const res of textResults) { + res.score = res.score * factor; + } + } + + if (results.length === 0 && textResults.length === 0) { + this.filteredOptions = []; + this.firstOption = null; + this.lastOption = null; + this.currentOption = null; + this.listboxNode.appendChild(this.noResultsElement); + return null; + } + + /** + * @type {SearchResult|null} + */ + let newCurrentOption = null; + + /** @type {(Fuzzysort.Result|TextMatch) []} */ + let allResults = []; + allResults.push(...textResults); + allResults.push(...results); + allResults.sort((x, y) => y.score - x.score); + allResults = allResults.slice(0, 30); + + this.filteredOptions = []; + this.firstOption = null; + this.lastOption = null; + for (let i = 0; i < allResults.length; i++) { + const result = allResults[i]; + if ("target" in result) { + const dataItems = this.mappedData[result.target]; + for (let j = 0; j < dataItems.length; j++) { + const searchable = dataItems[j]; + const option = searchableToHtml( + this.domainMappers, + dataItems[j], + result + .highlight((v) => ({ v })) + .map((v) => + typeof v === "string" + ? { t: "text", v } + : { t: "highlight", v: v.v } + ), + document + ); + option.title = option.title; // DEBUG: show scores + ` (${result.score})`; + /** @type {SearchResult} */ + const searchResult = { + item: searchable, + fuzzysortResult: result, + htmlItem: option, + }; + + option.addEventListener("click", this.onOptionClick(searchResult)); + option.addEventListener( + "pointerover", + this.onOptionPointerover.bind(this) + ); + option.addEventListener( + "pointerout", + this.onOptionPointerout.bind(this) + ); + this.filteredOptions.push(searchResult); + this.listboxNode.appendChild(option); + if (i === 0 && j === 0) { + this.firstOption = searchResult; + } + if (i === allResults.length - 1 && j === dataItems.length - 1) { + this.lastOption = searchResult; + } + if (currentOptionText === resultToText(searchResult)) { + newCurrentOption = searchResult; + } + } + } else { + const option = textResultToHtml(filter, result, document); + if (option) { + /** @type {SearchResult} */ + const searchResult = { + terms: filter, + textItem: result, + htmlItem: option + }; + option.addEventListener("click", this.onOptionClick(searchResult)); + option.addEventListener( + "pointerover", + this.onOptionPointerover.bind(this) + ); + option.addEventListener( + "pointerout", + this.onOptionPointerout.bind(this) + ); + this.filteredOptions.push(searchResult); + this.listboxNode.appendChild(option); + if (i === 0) { + this.firstOption = searchResult; + } + if (i === allResults.length - 1) { + this.lastOption = searchResult; + } + if (currentOptionText === resultToText(searchResult)) { + newCurrentOption = searchResult; + } + } + } + } + + const moreResults = document.createElement("li"); + moreResults.textContent = `Showing ${allResults.length}/${results.total + textResults.length} results`; + moreResults.className = `more-results`; + this.listboxNode.appendChild(moreResults); + + if (newCurrentOption) { + this.currentOption = newCurrentOption; + } + if (!this.currentOption) { + this.currentOption = this.firstOption; + } + + return newCurrentOption ?? this.firstOption; + } + + /** + * @param {SearchResult | null} option + */ + setCurrentOptionStyle(option) { + for (const opt of this.filteredOptions) { + const el = opt.htmlItem; + if (opt === option) { + el.setAttribute("aria-selected", "true"); + if ( + this.listboxNode.scrollTop + this.listboxNode.offsetHeight < + el.offsetTop + el.offsetHeight + ) { + this.listboxNode.scrollTop = + el.offsetTop + el.offsetHeight - this.listboxNode.offsetHeight; + } else if (this.listboxNode.scrollTop > el.offsetTop + 2) { + this.listboxNode.scrollTop = el.offsetTop; + } + } else { + el.removeAttribute("aria-selected"); + } + } + } + + /** + * @param {SearchResult} currentOption + * @param {SearchResult} lastOption + */ + getPreviousOption(currentOption, lastOption) { + if (currentOption !== this.firstOption) { + var index = this.filteredOptions.indexOf(currentOption); + return this.filteredOptions[index - 1]; + } + return lastOption; + } + + /** + * @param {SearchResult | null} currentOption + * @param {SearchResult} firstOption + */ + getNextOption(currentOption, firstOption) { + if (currentOption != null && currentOption !== this.lastOption) { + var index = this.filteredOptions.indexOf(currentOption); + return this.filteredOptions[index + 1]; + } + return firstOption; + } + + /* MENU DISPLAY METHODS */ + + doesOptionHaveFocus() { + return this.comboboxNode.getAttribute("aria-activedescendant") !== ""; + } + + isOpen() { + return this.listboxNode.style.display === "block"; + } + + isClosed() { + return this.listboxNode.style.display !== "block"; + } + + open() { + this.listboxNode.style.display = "block"; + this.comboboxNode.setAttribute("aria-expanded", "true"); + this.buttonNode?.setAttribute("aria-expanded", "true"); + } + + /** + * @param {boolean} [force] + */ + close(force) { + if ( + force || + (!this.comboboxHasVisualFocus && + !this.listboxHasVisualFocus && + !this.hasHover) + ) { + this.setCurrentOptionStyle(null); + this.listboxNode.style.display = "none"; + this.comboboxNode.setAttribute("aria-expanded", "false"); + this.buttonNode?.setAttribute("aria-expanded", "false"); + this.setActiveDescendant(null); + } + } + + /* combobox Events */ + + /** + * @param {KeyboardEvent} event + * @returns void + */ + onComboboxKeyDown(event) { + let eventHandled = false; + const altKey = event.altKey; + + if (event.ctrlKey || event.shiftKey) { + return; + } + + switch (event.key) { + case "Enter": + if (this.listboxHasVisualFocus) { + this.setValue(opt(this.currentOption, resultToText) ?? ""); + if (this.currentOption) { + if("fuzzysortResult" in this.currentOption) { + this.confirmResult(this.currentOption.item.address); + } else { + this.confirmResult(this.currentOption.textItem.doc.id, this.currentOption.terms); + } + } + } + this.close(true); + this.setVisualFocusCombobox(); + eventHandled = true; + break; + + case "Down": + case "ArrowDown": + if (this.filteredOptions.length > 0 && this.firstOption != null) { + if (altKey) { + this.open(); + } else { + this.open(); + if ( + this.listboxHasVisualFocus + ) { + this.setOption( + this.getNextOption(this.currentOption, this.firstOption) + ); + this.setVisualFocusListbox(); + } else { + this.setOption(this.firstOption); + this.setVisualFocusListbox(); + } + } + } + eventHandled = true; + break; + + case "Up": + case "ArrowUp": + if ( + this.filteredOptions.length > 0 && + this.currentOption != null && + this.lastOption != null + ) { + if (this.listboxHasVisualFocus) { + this.setOption( + this.getPreviousOption(this.currentOption, this.lastOption) + ); + } else { + this.open(); + if (!altKey) { + this.setOption(this.lastOption); + this.setVisualFocusListbox(); + } + } + } + eventHandled = true; + break; + + case "Esc": + case "Escape": + if (this.isOpen()) { + this.close(true); + this.filter = this.comboboxNode.textContent; + this.filterOptions(); + this.setVisualFocusCombobox(); + } else { + this.setValue(""); + this.comboboxNode.textContent = ""; + } + eventHandled = true; + break; + + case "Tab": + this.close(true); + break; + + case "Home": + this.imeRewriter.setSelections([new Range(0, 0)]); + eventHandled = true; + break; + + case "End": + var length = this.comboboxNode.textContent.length; + this.imeRewriter.setSelections([new Range(length, 0)]); + eventHandled = true; + break; + + default: + break; + } + + if (eventHandled) { + event.stopImmediatePropagation(); + event.preventDefault(); + } + } + + /** + * @param {KeyboardEvent} event + * @returns void + */ + onComboboxKeyUp(event) { + let eventHandled = false; + + if (event.key === "Escape" || event.key === "Esc") { + return; + } + + switch (event.key) { + case "Left": + case "ArrowLeft": + case "Right": + case "ArrowRight": + case "Home": + case "End": + this.setCurrentOptionStyle(null); + this.setVisualFocusCombobox(); + eventHandled = true; + break; + + default: + if (this.comboboxNode.textContent !== this.filter) { + this.filter = this.comboboxNode.textContent; + this.setVisualFocusCombobox(); + this.setCurrentOptionStyle(null); + eventHandled = true; + const option = this.filterOptions(); + if (option) { + if (this.isClosed() && this.comboboxNode.textContent.length) { + this.open(); + } + + this.setCurrentOptionStyle(option); + this.setOption(option); + } else { + this.close(); + this.setActiveDescendant(null); + } + } + + break; + } + + if (eventHandled) { + event.stopImmediatePropagation(); + event.preventDefault(); + } + } + + onComboboxClick() { + if (this.isOpen()) { + this.close(true); + } else { + this.open(); + } + } + + onComboboxFocus() { + this.filter = this.comboboxNode.textContent; + this.filterOptions(); + this.setVisualFocusCombobox(); + this.setCurrentOptionStyle(null); + } + + onComboboxBlur() { + this.removeVisualFocusAll(); + // Remove empty space created by browser after user deletes entered text. + // Makes the placeholder appear again. + if (this.comboboxNode.textContent.trim().length === 0) { + this.comboboxNode.textContent = ""; + } + } + + /** + * @param {PointerEvent} event + * @returns void + */ + onBackgroundPointerUp(event) { + const node = /** @type {Node | null} */ (event.target); + if ( + !this.comboboxNode.contains(node) && + !this.listboxNode.contains(node) && + (this.buttonNode == null || !this.buttonNode.contains(node)) + ) { + this.comboboxHasVisualFocus = false; + this.setCurrentOptionStyle(null); + this.removeVisualFocusAll(); + setTimeout(this.close.bind(this, true), 100); + } + } + + onButtonClick() { + if (this.isOpen()) { + this.close(true); + } else { + this.open(); + } + this.comboboxNode.focus(); + this.setVisualFocusCombobox(); + } + + /* Listbox Events */ + + onListboxPointerover() { + this.hasHover = true; + } + + onListboxPointerout() { + this.hasHover = false; + setTimeout(this.close.bind(this, false), 300); + } + + // Listbox Option Events + + /** + * @param {SearchResult} result + * @returns MouseEventHandler + */ + onOptionClick(result) { + /** + * @returns void + */ + return () => { + this.comboboxNode.textContent = resultToText(result); + if ("fuzzysortResult" in result) { + this.confirmResult(result.item.address); + } else { + this.confirmResult(result.textItem.doc.id, resultToText(result)); + } + this.close(true); + }; + } + + onOptionPointerover() { + this.hasHover = true; + this.open(); + } + + onOptionPointerout() { + this.hasHover = false; + setTimeout(this.close.bind(this, false), 300); + } +} + +/** + * @typedef {{ + * searchWrapper: HTMLElement; + * data: any; + * domainMappers: Record; + * }} RegisterSearchArgs + * @param {RegisterSearchArgs} args + */ +export const registerSearch = ({ searchWrapper, data, domainMappers }) => { + const comboboxNode = /** @type {HTMLDivElement} */ ( + searchWrapper.querySelector("div[contenteditable]") + ); + + const buttonNode = searchWrapper.querySelector("button"); + const listboxNode = /** @type {HTMLElement | null} */ ( + searchWrapper.querySelector('[role="listbox"]') + ); + if (comboboxNode != null && listboxNode != null) { + new SearchBox( + comboboxNode, + buttonNode, + listboxNode, + domainMappers, + dataToSearchableMap(data, domainMappers) + ); + } +}; diff --git a/static-web/search/search-highlight.css b/static-web/search/search-highlight.css new file mode 100644 index 000000000..32cb3f706 --- /dev/null +++ b/static-web/search/search-highlight.css @@ -0,0 +1,76 @@ +.text-search-results { + background-color: var(--verso-selected-color); +} + +.text-search-results.focused { + outline: auto; +} + +#highlight-controls { + position: fixed; + bottom: 10px; + right: 10px; + z-index: 99; /* The search box dropdown is 100, and should cover this */ + display: flex; + gap: 4px; + background: white; + border: 1px solid #ccc; + border-radius: 4px; + padding: 4px; + box-shadow: 0 2px 4px rgba(0,0,0,0.1); + box-sizing: border-box; + font-size: .9rem; + font-family: system-ui, sans-serif; + min-width: 400px; + max-width: var(--verso-content-max-width, 47rem); + width: 50%; + display: flex; +} + +@media screen and (max-width: 700px) { + #highlight-controls { + width: 100%; + bottom: 0px; + right: 0px; + border-radius: 4px 4px 0 0; + } +} + + +#highlight-prev, #highlight-next, #highlight-close { + padding: 6px 8px; + border-radius: 2px; + cursor: pointer; + background: #f8f9fa; + border: 1px solid #ddd; +} + +@media screen and (max-width: 700px) { + /* Touch-friendly sizing */ + #highlight-prev, #highlight-next, #highlight-close { + min-width: var(--verso-burger-width, 1.5rem); + min-height: var(--verso-burger-height, 1.5rem); + } +} + +#highlight-close { + margin-left: 4px; +} + +#highlight-current-count { + padding: 6px 8px; + background: #f8f9fa; + border: 1px solid #ddd; + border-radius: 2px; + min-width: 40px; + text-align: center; + flex: 1 1 100%; +} + +#highlight-current-count:has(#highlight-current:not(:empty)) { + cursor: pointer; +} + +#highlight-current:not(:empty) { + margin-inline: 0 8px; +} diff --git a/static-web/search/search-highlight.js b/static-web/search/search-highlight.js new file mode 100644 index 000000000..fd70a5ecb --- /dev/null +++ b/static-web/search/search-highlight.js @@ -0,0 +1,390 @@ + +/** + * @typedef {{ref: string, score: number, doc: {id: string, header: string, context: string, contents: string}}} TextMatch + * @typedef {{run: (tokens: string[]) => string[]}} ElasticLunrPipeline + * @typedef {{bool?: "AND"|"OR", fields?:Record}} SearchConfig + * @typedef {{search: ((term: string, config: SearchConfig) => TextMatch[]), pipeline: ElasticLunrPipeline}|undefined|null} TextSearchIndex + * @typedef {{original: string, stem: string, start: number, end: number}} TextToken + */ + +/** Whether to search word prefixes or whole words in full-text searches. Should match the setting in search-box.js. + * @type {boolean} + */ +const expandHlMatches = true; + + +const searchIndex = /** @type {{searchIndex: TextSearchIndex}} */ ( + /** @type {unknown} */ (window) +).searchIndex; + + +/** Tokenizes the given string, computing stems. + * @param {string} text + * @return {TextToken[]} + */ +const tokenizeText = (text) => { + const toks = []; + const regex = /[^\s(),."“”—:]+/g; + let match; + while ((match = regex.exec(text)) !== null) { + let stems = searchIndex.pipeline.run([match[0]]); + for (const stem of stems) { + toks.push({ + original: match[0], + start: match.index, + end: match.index + match[0].length, + stem: stem.toLowerCase() + }); + } + } + return toks; +} + +function highlightSearchTerms() { + // Get search terms from URL query string + const urlParams = new URLSearchParams(window.location.search); + const searchQuery = urlParams.get('terms'); + + if (!searchQuery) { + return; // No search terms found + } + + // Stem the terms + const searchTerms = {}; + const regex = /\S+/g; + let match; + while ((match = regex.exec(searchQuery)) !== null) { + let stems = searchIndex.pipeline.run([match[0]]); + for (const stem of stems) { + searchTerms[stem.toLowerCase()] = match[0]; + } + } + + // Function to highlight text in a text node + function highlightTextNode(textNode) { + let text = textNode.textContent; + + const toks = tokenizeText(text); + for (const t of toks.reverse()) { + if (expandHlMatches) { + // We're doing full-text search with matching prefixes. Find the longest matching stem in the results and use it. + let bestStem = ""; + for (termStem in searchTerms) { + if (termStem.length <= bestStem.length) continue; + if (t.stem.startsWith(termStem)) bestStem = termStem; + } + if (bestStem.length > 0) { + text = text.slice(0, t.start) + `${text.slice(t.start, t.end)}` + text.slice(t.end); + } + } else { + // We're doing full-text search with whole words only. Look the stem up directly. + if (searchTerms.hasOwnProperty(t.stem)) { + text = text.slice(0, t.start) + `${text.slice(t.start, t.end)}` + text.slice(t.end); + } + } + } + + // Create a temporary container + const tempDiv = document.createElement('div'); + tempDiv.innerHTML = text; + + // Replace the text node with highlighted content + const fragment = document.createDocumentFragment(); + while (tempDiv.firstChild) { + fragment.appendChild(tempDiv.firstChild); + + } + const parent = textNode.parentNode; + parent.replaceChild(fragment, textNode); + parent.querySelectorAll('.text-search-results').forEach((e) => { + e.addEventListener('click', () => { + const i = allHighlights.indexOf(e); + if (i >= 0) { + currentHighlightIndex = i; + updateNavigationState(); + } + }); + }); + } + + /** Function to traverse DOM and find text nodes + * @param {any} node + */ + function traverseNodes(node) { + if (node.nodeType === Node.TEXT_NODE) { + highlightTextNode(node); + } else if (node.nodeType === Node.ELEMENT_NODE) { + // Skip script, style, and already highlighted elements + if (node.tagName && + !['SCRIPT', 'STYLE', 'NOSCRIPT'].includes(node.tagName.toUpperCase()) && + !node.classList.contains('text-search-results') && + // Don't highlight search terms in invisible hovers + !node.classList.contains('hover-info') && + // Don't highlight search terms in doc box labels + !(node.classList.contains('label') && node.parentNode && node.parentNode.classList.contains('namedocs'))) { + + // Process child nodes (in reverse order to handle DOM changes) + const children = Array.from(node.childNodes); + for (let i = children.length - 1; i >= 0; i--) { + traverseNodes(children[i]); + } + } + } + } + + // Start traversal from
+ document.querySelectorAll('main section').forEach(traverseNodes); + + // Update highlights array after highlighting + updateHighlightsArray(); +} + +// Function to remove all highlights +function removeHighlights() { + const highlightedElements = document.querySelectorAll('span.text-search-results'); + highlightedElements.forEach(span => { + const parent = span.parentNode; + parent.replaceChild(document.createTextNode(span.textContent), span); + parent.normalize(); // Merge adjacent text nodes + }); + updateHighlightsArray(); +} + +/** The index of the current highlight + * @type {number} + */ +let currentHighlightIndex = -1; +/** All highlight elements. + * @type {HTMLElement[]} + */ +let allHighlights = []; + +/** Update highlights array and reset navigation + */ +function updateHighlightsArray() { + allHighlights = Array.from(document.querySelectorAll('span.text-search-results')); + currentHighlightIndex = -1; + updateNavigationState(); +} + +/** Navigate to next highlight + */ +function nextHighlight() { + if (allHighlights.length === 0) return; + + currentHighlightIndex = (currentHighlightIndex + 1) % allHighlights.length; + scrollToHighlight(currentHighlightIndex); +} + +/** Navigate to previous highlight + */ +function prevHighlight() { + if (allHighlights.length === 0) return; + + currentHighlightIndex = currentHighlightIndex <= 0 ? + allHighlights.length - 1 : currentHighlightIndex - 1; + scrollToHighlight(currentHighlightIndex); +} + +/** Scroll to a specific highlight + * @param {number} index The index of the highlight element in allHighlights + */ +function scrollToHighlight(index) { + if (index >= 0 && index < allHighlights.length) { + // Ensure visibility by opening collapsed examples + let here = allHighlights[index]; + if (here) { + while (here = here.parentElement) { + if (here.nodeName.toLowerCase() == "details") { + here.setAttribute('open', 'open'); + break; + } + } + } + + // Scroll to it + allHighlights[index].scrollIntoView({ + behavior: 'smooth', + block: 'center' + }); + + updateNavigationState(); + } +} + +/** Update navigation button states based on the contents of the document. + */ +function updateNavigationState() { + const prevBtn = document.getElementById('highlight-prev'); + const nextBtn = document.getElementById('highlight-next'); + const countSpan = document.getElementById('highlight-count'); + const currentSpan = document.getElementById('highlight-current'); + const currentCount = document.getElementById('highlight-current-count'); + + if (prevBtn && nextBtn && countSpan) { + const hasHighlights = allHighlights.length > 0; + prevBtn.disabled = !hasHighlights; + nextBtn.disabled = !hasHighlights; + + if (hasHighlights && currentHighlightIndex >= 0) { + countSpan.textContent = `${currentHighlightIndex + 1}/${allHighlights.length}`; + currentSpan.textContent = allHighlights[currentHighlightIndex].textContent; + let resName = allHighlights[currentHighlightIndex].title; + resName = resName.charAt(0).toLowerCase() + resName.slice(1); + currentCount.title = 'Go to ' + resName; + document.querySelectorAll('.text-search-results').forEach((e) => e.classList.remove('focused')); + let here = allHighlights[currentHighlightIndex]; + here.classList.add('focused'); + while (here = here.parentElement) { + if (here.nodeName.toLowerCase() == "details") { + here.setAttribute('open', 'open'); + break; + } + } + } else { + countSpan.textContent = hasHighlights ? `0/${allHighlights.length}` : '0/0'; + currentSpan.textContent = ''; + currentCount.title = ''; + } + } +} + +/** Toggle highlights + */ +function toggleHighlights() { + const existingHighlights = document.querySelectorAll('span.text-search-results'); + if (existingHighlights.length > 0) { + removeHighlights(); + } else { + highlightSearchTerms(); + } +} + +/** Scroll to first highlight after a specific element + * @param {string} elementId + */ +function scrollToFirstHighlightAfter(elementId) { + let targetElement = document.getElementById(elementId); + if (!targetElement) { + targetElement = document.body; + } + + const highlights = document.querySelectorAll('span.text-search-results'); + if (highlights.length === 0) { + return false; + } + + // Find the first highlight that comes after the target element in document order + const targetPosition = targetElement.compareDocumentPosition ? + targetElement : null; + + if (!targetPosition) { + return false; + } + + for (let highlight of highlights) { + const position = targetElement.compareDocumentPosition(highlight); + // Check if highlight comes after target element + if (position & Node.DOCUMENT_POSITION_FOLLOWING) { + highlight.scrollIntoView({ + behavior: 'smooth', + block: 'center' + }); + currentHighlightIndex = allHighlights.indexOf(highlight); + updateNavigationState(); + return true; + } + } + + return false; +} + +/** Checks whether there's a search query in the URL */ +function hasSearchQuery() { + const urlParams = new URLSearchParams(window.location.search); + const searchQuery = urlParams.get('terms'); + return searchQuery && searchQuery.trim().length > 0; +} + +/** Creates control buttons (only if search query exists) + */ +function createControlButtons() { + if (!hasSearchQuery()) { + return; + } + + const container = document.createElement('div'); + container.id = 'highlight-controls'; + + // Previous button + const prevBtn = document.createElement('button'); + prevBtn.id = 'highlight-prev'; + prevBtn.textContent = '◀'; + prevBtn.title = 'Previous match'; + prevBtn.addEventListener('click', prevHighlight); + + const currentSpan = document.createElement('span'); + currentSpan.id = 'highlight-current'; + + // Count display + const countSpan = document.createElement('span'); + countSpan.id = 'highlight-count'; + countSpan.textContent = '0/0'; + + const currentCount = document.createElement('span'); + currentCount.id = 'highlight-current-count'; + currentCount.appendChild(currentSpan); + currentCount.appendChild(countSpan); + currentCount.addEventListener('click', () => scrollToHighlight(currentHighlightIndex)); + + // Next button + const nextBtn = document.createElement('button'); + nextBtn.id = 'highlight-next'; + nextBtn.textContent = '▶'; + nextBtn.title = 'Next match'; + nextBtn.addEventListener('click', nextHighlight); + + // Toggle button + const toggleBtn = document.createElement('button'); + toggleBtn.id = 'highlight-close'; + toggleBtn.textContent = '✖'; + toggleBtn.title = 'Close search'; + toggleBtn.addEventListener('click', toggleHighlights); + toggleBtn.addEventListener('click', () => container.remove()); + + container.appendChild(prevBtn); + container.appendChild(currentCount); + container.appendChild(nextBtn); + container.appendChild(toggleBtn); + + document.body.appendChild(container); +} + +// Run the highlighter when DOM is ready +if (document.readyState === 'loading') { + document.addEventListener('DOMContentLoaded', function() { + highlightSearchTerms(); + createControlButtons(); + updateHighlightsArray(); + + // Check for hash in URL and scroll to first highlight after it + if (window.location.hash) { + const elementId = window.location.hash.substring(1); + setTimeout(() => { + scrollToFirstHighlightAfter(elementId); + }, 100); // Small delay to ensure highlighting is complete + } + }); +} else { + highlightSearchTerms(); + createControlButtons(); + updateHighlightsArray(); + + // Check for hash in URL and scroll to first highlight after it + if (window.location.hash) { + const elementId = window.location.hash.substring(1); + setTimeout(() => { + scrollToFirstHighlightAfter(elementId); + }, 100); // Small delay to ensure highlighting is complete + } +} diff --git a/static-web/search/search-init.js b/static-web/search/search-init.js new file mode 100644 index 000000000..d38ee26c3 --- /dev/null +++ b/static-web/search/search-init.js @@ -0,0 +1,48 @@ +/** + * Copyright (c) 2024 Lean FRO LLC. All rights reserved. + * Released under Apache 2.0 license as described in the file LICENSE. + * Author: David Thrane Christiansen + */ + +import {domainMappers} from './domain-mappers.js'; +import {registerSearch} from './search-box.js'; + +let siteRoot = typeof __versoSiteRoot !== 'undefined' ? __versoSiteRoot : ""; + +// The search box itself. TODO: add to template +// autocorrect is a safari-only attribute. It is required to prevent autocorrect on iOS. +const searchHTML = `
+
+
+ +
+
    +
    +
    +`; + +// Initialize search box +const data = fetch(siteRoot + "/xref.json").then((data) => data.json()) +window.addEventListener("load", () => { + const main = document.querySelector("header"); + main.insertAdjacentHTML("beforeend", searchHTML); + const searchWrapper = document.querySelector(".combobox-list"); + data.then((data) => { + registerSearch({searchWrapper, data, domainMappers}); + }); +}); diff --git a/static-web/search/unicode-input-component.min.js b/static-web/search/unicode-input-component.min.js new file mode 100644 index 000000000..4124f3b1a --- /dev/null +++ b/static-web/search/unicode-input-component.min.js @@ -0,0 +1,2 @@ +/** This has been updated to fix the tab issue raised in https://github.com/leanprover/vscode-lean4/pull/572 */ +var A=Object.defineProperty,d=(o,u,s)=>(typeof u!="symbol"&&(u+=""),u in o?A(o,u,{enumerable:!0,configurable:!0,writable:!0,value:s}):o[u]=s);import l from"./unicode-input.min.js";function R(o){return o&&o.__esModule&&Object.prototype.hasOwnProperty.call(o,"default")?o.default:o}function _(o,u,s){return s={path:u,exports:{},require:function(p,c){return I(p,c??s.path)}},o(s,s.exports),s.exports}function I(){throw new Error("Dynamic requires are not currently supported by @rollup/plugin-commonjs")}var g=_(function(o,u){Object.defineProperty(u,"__esModule",{value:!0}),u.InputAbbreviationRewriter=void 0;function s(i,e,n=0){if(i===e)return n;if(!i.contains(e))return;let r=0;for(const t of Array.from(i.childNodes)){const a=s(t,e,n);if(a!==void 0)return r+=a,r;r+=t.textContent?.length??0}return}function p(i,e,n){let r,t;return e&&(r=s(i,e.node,e.offset)),n&&(t=s(i,n.node,n.offset)),r===void 0?t===void 0?void 0:new l.Range(t,0):t===void 0?new l.Range(r,0):(tr?{found:!1,remainingOffset:e-r}:{found:!0,node:i,offset:e}}for(const r of Array.from(i.childNodes)){const t=w(r,e);if(t.found)return t;e=t.remainingOffset}return{found:!1,remainingOffset:e}}function b(i,e){const n=w(i,e);if(!n.found)return;const r=window.getSelection();if(r===null)return;const t=document.createRange();t.setStart(n.node,n.offset),t.collapse(!0),r.removeAllRanges(),r.addRange(t)}function m(i,e){e.sort((t,a)=>t.range.offset-a.range.offset);let n="",r=0;for(const t of e)n+=i.slice(r,t.range.offset),n+=t.update(i.slice(t.range.offset,t.range.offsetEnd+1)),r=t.range.offset+t.range.length;return n+=i.slice(r),n}class v{constructor(e,n){d(this,"config");d(this,"textInput");d(this,"rewriter");d(this,"isInSelectionChange",!1);if(this.config=e,this.textInput=n,!n.isContentEditable)throw new Error;const r=new l.AbbreviationProvider(e);this.rewriter=new l.AbbreviationRewriter(e,r,this),n.addEventListener("beforeinput",async t=>{const a=t,f=a.getTargetRanges()[0];if(f===void 0)return;const h=p(n,{node:f.startContainer,offset:f.startOffset},{node:f.endContainer,offset:f.endOffset});if(h===void 0)return;const S=a.data??"",y={range:h,newText:S};this.rewriter.changeInput([y])}),n.addEventListener("input",async t=>{await this.rewriter.triggerAbbreviationReplacement(),await this.updateSelection(),this.updateState()}),document.addEventListener("selectionchange",async()=>{if(this.isInSelectionChange)return;this.isInSelectionChange=!0,await this.updateSelection(),this.updateState(),this.isInSelectionChange=!0}),n.addEventListener("keydown",async t=>{t.key==="Tab"&&this.rewriter.getTrackedAbbreviations().size>0&&(await this.rewriter.replaceAllTrackedAbbreviations(),this.updateState(),t.stopImmediatePropagation(),t.preventDefault())})}resetAbbreviations(){this.rewriter.resetTrackedAbbreviations(),this.updateState()}async updateSelection(){const e=this.getSelection();if(e===void 0)return;await this.rewriter.changeSelections([e])}getSelection(){return c(this.textInput)}updateState(){const e=this.getInput(),n=this.textInput.innerHTML,r=Array.from(this.rewriter.getTrackedAbbreviations()).map(f=>({range:f.range,update:h=>`${h}`})),t=m(e,r);if(n===t)return;const a=this.getSelection();this.setInputHTML(t),a!==void 0&&this.setSelections([a])}async replaceAbbreviations(e){const n=e.map(r=>({range:r.range,update:t=>r.newText}));return this.setInputHTML(m(this.getInput(),n)),!0}selectionMoveMode(){return{kind:"MoveAllSelections"}}collectSelections(){const e=this.getSelection();return e===void 0?[]:[e]}setSelections(e){const n=e[0];if(n===void 0)return;b(this.textInput,n.offset)}setInputHTML(e){this.textInput.innerHTML=e}getInput(){return this.textInput.innerText}}u.InputAbbreviationRewriter=v}),T=R(g),C=g.InputAbbreviationRewriter;export default T;export{C as InputAbbreviationRewriter,g as __moduleExports}; diff --git a/static-web/search/unicode-input.min.js b/static-web/search/unicode-input.min.js new file mode 100644 index 000000000..397ffd95c --- /dev/null +++ b/static-web/search/unicode-input.min.js @@ -0,0 +1 @@ +var w=Object.defineProperty,l=(a,e,r)=>(typeof e!="symbol"&&(e+=""),e in a?w(a,e,{enumerable:!0,configurable:!0,writable:!0,value:r}):a[e]=r),g=typeof globalThis!="undefined"?globalThis:typeof window!="undefined"?window:typeof global!="undefined"?global:typeof self!="undefined"?self:{};function C(a){return a&&a.__esModule&&Object.prototype.hasOwnProperty.call(a,"default")?a.default:a}function d(a,e,r){return r={path:e,exports:{},require:function(p,t){return _(p,t??r.path)}},a(r,r.exports),r.exports}function _(){throw new Error("Dynamic requires are not currently supported by @rollup/plugin-commonjs")}var I=d(function(a,e){Object.defineProperty(e,"__esModule",{value:!0})});const k="\u2016$CURSOR\u2016\u208A",x="\u2016$CURSOR\u2016",y="\u230A$CURSOR\u230B",R="\u2308$CURSOR\u2309",A="\u230A$CURSOR\u230B\u208A",S="\u2308$CURSOR\u2309\u208A",G="\u03B1",O="\u03B2",E="\u03C7",T="\u2193",U="\u03B5",P="\u03B3",L="\u2229",B="\u03BC",j="\xAC",z="\u2218",D="\u03A0",N="\u25B8",H="\u2192",$="\u2191",K="\u2228",V="\xD7",F="\u2190",Z="\xD8",X="\u{1D538}",W="\u2102",J="\u0394",Y="\u{1D53D}",Q="\u0393",tt="\u210D",nt="\u22C2",ot="\u22C2\u2080",st="\u{1D542}",ct="\u039B",et="\u2115",rt="\u03A0",it="\u211A",at="\u211D",lt="\u03A3",bt="\u22C3",ft="\u22C3\u2080",ut="\u2124",pt="\u03B2",Mt="\u03B3",gt="\u03B4",dt="\u03B5",ht="\u03B6",mt="\u03B7",qt="\u03B8",vt="\u03B9",wt="\u03BA",Ct="\u03BB",_t="\u03BC",It="\u03BD",kt="\u03BE",xt="\u03C0",yt="\u03C1",Rt="\u03C2",At="\u03C3",St="\u03C4",Gt="\u03C6",Ot="\u03C7",Et="\u03C8",Tt="\u03C9",Ut="\xC7",Pt="\xE7",Lt="\u2209",Bt="\u2669",jt="\xAC",zt="\u{1018E}",Dt="\u2209",Nt="\u220C",Ht="\u220B",$t="\u27F9",Kt="\u27F9",Vt="\u266E",Ft="\u2115",Zt="\u20A6",Xt="\u2207",Wt="\u2249",Jt="\u2116",Yt="\u21CD",Qt="\u21CE",tn="\u21CF",nn="\u22AF",on="\u22AE",sn="\u2247",cn="\u2197",en="\xAC",rn="\u2262",an="\u2260",ln="\u2204",bn="\u2260",fn="\u2271",un="\u2271",pn="\u2271",Mn="\u226F",gn="\u219A",dn="\u21AE",hn="\u2270",mn="\u2270",qn="\u2270",vn="\u226E",wn="\u2224",Cn="\u2226",_n="\u22E0",In="\u2280",kn="\u219B",xn="\u2224",yn="\u2244",Rn="\u2241",An="\u2288",Sn="\u2288",Gn="\u2284",On="\u22E1",En="\u2281",Tn="\u2289",Un="\u2289",Pn="\u2285",Ln="\u22EC",Bn="\u22EA",jn="\u22ED",zn="\u22EB",Dn="\u22AD",Nn="\u22AC",Hn="\u2196",$n="\u2260",Kn="\u2243",Vn="\u2256",Fn="\u2255",Zn="\u22DD",Xn="\u22DC",Wn="\u22A2",Jn="\u2013",Yn="\u2204",Qn="\u2203",to="\u2203",no="\u2205",oo="\u2205",so="\u2014",co="\u03B5",eo="\u03B5",ro="\u20AC",io="\u03B7",ao="\u2113",lo="\u2245",bo="\u2209",fo="\u2229",uo="\u22BA",po="\u2229",Mo="\u222B",go="\u2124",ho="\u207B\xB9",mo="\u2206",qo="\u2293",vo="\u2A05",wo="\u221E",Co="\u2194",_o="\u2192",Io="\u0131",ko="\u03B9",xo="\u223C",yo="\u27F6",Ro="\u03E9",Ao="\u21A9",So="\u21AA",Go="\u20B4",Oo="\u0371",Eo="\u2665",To="\u210F",Uo="\u2227",Po="\u2227",Lo="\u2220",Bo="\u221F",jo="\u212B",zo="\u2200",Do="\u2200\u1DA0",No="\u2200\u1D50",Ho="\u03B1",$o="\u2135",Ko="\u2135\u2080",Vo="\u204E",Fo="\u2217",Zo="\u224D",Xo="\u2336",Wo="\u224A",Jo="\u2248",Yo="\xE5",Qo="\xE6",ts="\u20B3",ns="\u060B",os="\u2210",ss="\u2A0D",cs="\xAA",es="\xBA",rs="\u2228",is="\u2295",as="\u1D52\u1D48",ls="\u1D52\u1D48",bs="\u1D43\u1D52\u1D56",fs="\u1D43\u1D52\u1D56",us="\u1D50\u1D52\u1D56",ps="\u1D50\u1D52\u1D56",Ms="\u1D52\u1D56",gs="\u1D52\u1D56",ds="\u2297",hs="\u229A",ms="\u0153",qs="\u{1F6D1}",vs="\u2126",ws="\u2125",Cs="\u03C9",_s="\u03BF",Is="\u2296",ks="\u2299",xs="\u222E",ys="\u222F",Rs="\u2298",As="\u2297",Ss="\u2297",Gs="\u2A02",Os="\u2A02",Es="\u2202",Ts="\u222F",Us="\u25B9",Ps="\u25B9",Ls="\u25BF",Bs="\u22B4",js="\u25C3",zs="\u225C",Ds="\u22B5",Ns="\u25B9",Hs="\u25B5",$s="\u2B1D",Ks="\u25C2",Vs="\u219E",Fs="\u21A0",Zs="\u25C3",Xs="\u2040",Ws="\xD7",Js="\u03B8",Ys="\u2234",Qs="\u2248",tc="\u223C",nc="\u2121",oc="\u20B8",sc="\u266A",cc="\xB5",ec="\u2044",rc="\u0E3F",ic="\u271D",ac="\u2052",lc="\u20A1",bc="\u2117",fc="\u20A9",uc="\u20A6",pc="\u2116",Mc="\u20B1",gc="\u2031",dc="\u20A4",hc="\u2045",mc="\u211E",qc="\u203B",vc="\u2046",wc="\u203D",Cc="\u212E",_c="\u25E6",Ic="\u20AE",kc="\u03C4",xc="\u22A4",yc="\u2192",Rc="\u2192\u2080",Ac="\u2192\u2080",Sc="\u2192\u2080",Gc="\u2192\u2080",Oc="\u2192\u2080",Ec="\u2192\u2081",Tc="\u2192\u2081",Uc="\u2192\u2081",Pc="\u2192\u2081",Lc="\u2192\u2081",Bc="\u2192\u2081\u209B",jc="\u2192\u2081\u209B",zc="\u2192\u2081\u209B",Dc="\u2192\u2081\u209B",Nc="\u2192\u2081\u209B",Hc="\u2192\u2090",$c="\u2192\u2090",Kc="\u2192\u2090",Vc="\u2192\u2090",Fc="\u2192\u2090",Zc="\u2192\u1D47",Xc="\u2192\u1D47",Wc="\u2192\u1D47",Jc="\u2192\u2097",Yc="\u2192\u2097",Qc="\u2192\u2097",te="\u2192\u2097",ne="\u2192\u2097",oe="\u2192\u2098",se="\u2192\u2098",ce="\u2192\u2098",ee="\u2192\u2098",re="\u2192\u2098",ie="\u2192\u209A",ae="\u2192\u209A",le="\u2192\u209A",be="\u2192\u209A",fe="\u2192\u209B",ue="\u2192\u209B",pe="\u2192\u209B",Me="\u2192\u209B",ge="\u2192\u209B",de="\u21E8",he="\u21E8",me="\uFFE2",qe="\u22D6",ve="\u22D6",we="\u2A7F",Ce="\u2A7F",_e="\u2259",Ie="\xB0",ke="\u03EF",xe="\u03B4",ye="\u2251",Re="\u2250",Ae="\u2214",Se="\u22A1",Ge="\u2B1D",Oe="\u20AB",Ee="\u2193",Te="\u21CA",Ue="\u21C3",Pe="\u21C2",Le="\u20AF",Be="\u2198",je="\u2199",ze="\u2021",De="\u2021",Ne="\u22F1",He="\u21AF",$e="\u25C6",Ke="\u25C7",Ve="\u2680",Fe="\xF7",Ze="\u22C7",Xe="\xF7",We="\u2300",Je="\u2662",Ye="\u22C4",Qe="\u03DD",tr="\u25C6",nr="\u2020",or="\u2020",sr="\u2138",cr="\u22A3",er="\xF0",rr="\u2223",ir="\u2293",ar="\u2208",lr="\u2208",br="\u2221",fr="\u21A6",ur="\u2642",pr="\u2720",Mr="\u20BC",gr="\u2212",dr="\u20A5",hr="\xB5",mr="\u2223",qr="\xD7",vr="\u22B8",wr="\u2127",Cr="\u22A7",_r="\u2213",Ir="\u{1F6C7}",kr="\u220F",xr="\u221D",yr="\u227E",Rr="\u227C",Ar="\u22E8",Sr="\u22E8",Gr="\u227E",Or="\u227A",Er="\u207B\xB9'",Tr="\u207B\xB9'",Ur="\u2032",Pr="\u21A3",Lr="\u{1D4AB}",Br="\xA3",jr="\xA3",zr="\u25B0",Dr="\u25B1",Nr="\u3250",Hr="\u2202",$r="\xB6",Kr="\u2225",Vr="\u25B0",Fr="\xB1",Zr="\u27C2",Xr="\u2030",Wr="\u214C",Jr="\u20B1",Yr="\u20A7",Qr="\xB6",ti="\u22D4",ni="\u03C8",oi="\u03C6",si="\u2270",ci="\u2266",ei="\u2264",ri="\u2264",ii="\u2270",ai="\u219D",li="\u21A2",bi="\u2190",fi="\u21BD",ui="\u21BC",pi="\u21C7",Mi="\u21C6",gi="\u2194",di="\u21CB",hi="\u21AD",mi="\u22CB",qi="\u2272",vi="\u22D6",wi="\u22DA",Ci="\u22DA",_i="\u2276",Ii="\u2272",ki="\u2264",xi="\u2294",yi="\u231F",Ri="\u2194",Ai="\u231E",Si="\u301A",Gi="\u226A",Oi="\u27C5",Ei="\u03BB",Ti="\u03BB",Ui="\u03BB",Pi="\u20BE",Li="\u27E8",Bi="\u20A4",ji="\u2308",zi="\u2026",Di="\u201C",Ni="\u300A",Hi="\u230A",$i="\u29CF",Ki="\u25C1",Vi="\u22E6",Fi="\u2268",Zi="\u2268",Xi="\u22E6",Wi="\xAC",Ji="\u27F5",Yi="\u27F7",Qi="\u27F6",ta="\u21AB",na="\u21AC",oa="\u2727",sa="\u2018",ca="\u22C9",ea="\u2268",ra="\u2271",ia="\u2267",aa="\u2265",la="\u2265",ba="\u2271",fa="\u2190",ua="\u2265",pa="\u2293",Ma="\u201E",ga="\u201A",da="\u20B2",ha="\u03EB",ma="\u03B3",qa="\u22D9",va="\u226B",wa="\u2137",Ca="\u22E7",_a="\u2269",Ia="\u2269",ka="\u22E7",xa="\u2273",ya="\u22D7",Ra="\u22DB",Aa="\u22DB",Sa="\u2277",Ga="\u2273",Oa="\u2269",Ea="\u201C",Ta="\u2018",Ua="\u221A",Pa="\u2284",La="\u2282",Ba="\u2285",ja="\u2283",za="\u228F",Da="\u2290",Na="\u2286",Ha="\u2288",$a="\u2286",Ka="\u2286",Va="\u228A",Fa="\u228A",Za="\u2286",Xa="\u2282",Wa="\u2286",Ja="\u2289",Ya="\u2287",Qa="\u2287",tl="\u228B",nl="\u228B",ol="\u2287",sl="\u2283",cl="\u22C3\u2080",el="\u22C2\u2080",rl="\u2294",il="\u2A06",al="\u221B",ll="\u221C",bl="\u221A",fl="\u227F",ul="\u227D",pl="\u227D",Ml="\u22E9",gl="\u22E9",dl="\u227F",hl="\u227B",ml="\u2211",ql="\u2933",vl="\u22E2",wl="\u2291",Cl="\u22E3",_l="\u2292",Il="\u25A1",kl="\u21DD",xl="\u25A0",yl="\u25A1",Rl="\u25A2",Al="\u2293",Sl="\u2294",Gl="\u221A",Ol="\u2291",El="\u228F",Tl="\u2292",Ul="\u2290",Pl="\u25FE",Ll="\u207B\xB9",Bl="\u2206",jl="\u2726",zl="\u2736",Dl="\u2734",Nl="\u2739",Hl="\u03DB",$l="\u22C6",Kl="\u03C6",Vl="\u22C6",Fl="\u20B7",Zl="\u2219",Xl="\u2660",Wl="\u2222",Jl="\xA7",Yl="\u2198",Ql="\\",tb="\u03FB",nb="\u03E1",ob="\u2223",sb="\u03F8",cb="\u03ED",eb="\u03E3",rb="\u266F",ib="\u03C3",ab="\u2243",lb="\u223C",bb="\uFE68",fb="\u2210",ub="\u2216",pb="\u2323",Mb="\u2323",gb="\u2022",db="\u2199",hb="\u25C0",mb="\u25C0",qb="\u25C1",vb="\u03A4",wb="\u0398",Cb="\xDE",_b="\u222A",Ib="\u203F",kb="\u2BD1",xb="\u222A",yb="\u2195",Rb="\u231C",Ab="\u2196",Sb="\u231D",Gb="\u2197",Ob="\u03C5",Eb="\u2191",Tb="\u2195",Ub="\u21BF",Pb="\u228E",Lb="\u21BE",Bb="\u21C8",jb="\u22C0",zb="\xC5",Db="\xC6",Nb="\u0391",Hb="\u22C1",$b="\u2A01",Kb="\u2A02",Vb="\u0152",Fb="\u03A9",Zb="\u039F",Xb="\u2124",Wb="\u22C2",Jb="\u22C2",Yb="\u0399",Qb="\u2111",tf="\u22C3",nf="\u22C3",of="\u22C3",sf="\u03A5",cf="\u21D1",ef="\u21D5",rf="\u03BB",af="\u03EA",lf="\u0393",bf="\u2A05",ff="\u03B1",uf="\u0391",pf="\u03B2",Mf="\u0392",gf="\u03B3",df="\u0393",hf="\u03B4",mf="\u0394",qf="\u03B5",vf="\u0395",wf="\u03B6",Cf="\u0396",_f="\u03B8",If="\u03C4",kf="\u0398",xf="\u03A4",yf="\u03B9",Rf="\u0399",Af="\u03BA",Sf="\u039A",Gf="\u039B",Of="\u03BC",Ef="\u039C",Tf="\u03BD",Uf="\u039D",Pf="\u03BE",Lf="\u039E",Bf="\u03C1",jf="\u03A1",zf="\u03C3",Df="\u03A3",Nf="\u03C5",Hf="\u03A5",$f="\u03C6",Kf="\u03A6",Vf="\u03C7",Ff="\u03A7",Zf="\u03C8",Xf="\u03A8",Wf="\u03C9",Jf="\u03A9",Yf="\u2A05",Qf="\u2A06",tu="\u2A06",nu="\u039B",ou="\u039B",su="\u21D0",cu="\u21D4",eu="\u2709",ru="\u21DA",iu="\u22D8",au="\u21D0",lu="\u21D4",bu="\u21D2",fu="\u2A05",uu="\u2A06",pu="\u2A05",Mu="\u2A06",gu="\u21B0",du="\u2016",hu="\u2102",mu="\u03A7",qu="\u22D2",vu="\u22D3",wu="\u231C",Cu="\u2308",_u="\xA4",Iu="\u22DE",ku="\u22DF",xu="\u227C",yu="\u22CE",Ru="\u22CF",Au="\u21B6",Su="\u21B7",Gu="\u231D",Ou="\u2309",Eu="\u222A",Tu="\u231C",Uu="\u231E",Pu="\u230A",Lu="\u231F",Bu="\u230B",ju="\u2663",zu="\u231E",Du="\u{1F6A7}",Nu="\u2245",Hu="\u2B1D",$u="\u1D9C",Ku="\u1D9C",Vu="\u2201",Fu="\u2201",Zu="\u2218",Xu="\u2102",Wu="\u2254",Ju="\u20A1",Yu="\xA9",Qu="\u22EF",tp="\u2B1D",np="\u25CF",op="\u25CB",sp="\u25EF",cp="\u2257",ep="\u21BA",rp="\u21BB",ip="\xAE",ap="\u24C8",lp="\u229B",bp="\u229A",fp="\u229D",up="\u2218",pp="\u25CF",Mp="\xB7",gp="\xA2",dp="\u20B5",hp="\u2103",mp="\u0229",qp="\u2713",vp="\u03C7",wp="\u20A2",Cp="\u2621",_p="\u2229",Ip="\u220E",kp="\u2001",xp="\u29F8",yp="\u29F8",Rp="\u22A0",Ap="\u2115",Sp="\u2124",Gp="\u211A",Op="\xA6",Ep="\u211D",Tp="\u2102",Up="\u2119",Pp="\u{1D539}",Lp="\u2140",Bp="\u{1D7D8}",jp="\u{1D7D9}",zp="\u{1D7DA}",Dp="\u{1D7DB}",Np="\u{1D7DC}",Hp="\u{1D7DD}",$p="\u{1D7DE}",Kp="\u{1D7DF}",Vp="\u{1D7E0}",Fp="\u{1D7E1}",Zp="\u{1D7EC}",Xp="\u{1D7ED}",Wp="\u{1D7EE}",Jp="\u{1D7EF}",Yp="\u{1D7F0}",Qp="\u{1D7F1}",tM="\u{1D7F2}",nM="\u{1D7F3}",oM="\u{1D7F4}",sM="\u{1D7F5}",cM="\u2022",eM="\u25E6",rM="\u2023",iM="\u224F",aM="\u2022",lM="\u2623",bM="\u21D4",fM="\u22C2",uM="\u25EF",pM="\u2210",MM="\u22C3",gM="\u2A05",dM="\u2A05",hM="\u2A06",mM="\u2A06",qM="\u2A05",vM="\u2A05",wM="\u2A06",CM="\u2605",_M="\u2A06",IM="\u25BD",kM="\u25B3",xM="\u22C1",yM="\u22C0",RM="\u03B2",AM="\u2136",SM="\u226C",GM="\u2235",OM="\u224C",EM="\u220D",TM="\u2035",UM="\u22CD",PM="\u223D",LM="\u22BC",BM="\u2726",jM="\u25AA",zM="\u263B",DM="\u25BE",NM="\u25C2",HM="\u25B8",$M="\u25B4",KM="\u22A5",VM="\u22C8",FM="\u229F",ZM="\u25EB",XM="\u25EB",WM="\u229E",JM="\u22A0",YM="\u2294",QM="\u25AC",tg="\u25AD",ng="\u211D",og="\xAE",sg="\u25AC",cg="\u27C6",eg="\u211A",rg="\u2622",ig="\u301B",ag="\u27E9",lg="\u2019",bg="\uFDFC",fg="\u21A3",ug="\u2192",pg="\u21C1",Mg="\u21C0",gg="\u21C4",dg="\u21CC",hg="\u21C9",mg="\u22CC",qg="\u2253",vg="\u20BD",wg="\u20A8",Cg="\u03C1",_g="\u25B7",Ig="\u2309",kg="\u230B",xg="\u22CA",yg="\u201D",Rg="\u300B",Ag="\u2964",Sg="\u03BB",Gg="\u220F\u1DA0",Og="\u2211\u1DA0",Eg="\xBD",Tg="\u2153",Ug="\xBC",Pg="\u2155",Lg="\u2159",Bg="\u215B",jg="\u215F",zg="\u2154",Dg="\u2156",Ng="\xBE",Hg="\u2157",$g="\u215C",Kg="\u2158",Vg="\u215A",Fg="\u215D",Zg="\u215E",Xg="\xBC",Wg="\u2322",Jg="\xBB",Yg="\u203A",Qg="\u2640",td="\u03E5",nd="\u213B",od="\u2252",sd="\u266D",cd="\xAB",ed="\u2039",rd="\u2200",id="\u039E",ad="\u2115",ld="\u039D",bd="\u0396",fd="\u211A",ud="\u211D",pd="\u211C",Md="\u03A1",gd="\u21D2",dd="\u21DB",hd="\u21B1",md="\u03E4",qd="\u2639",vd="\u03E8",wd="\u0370",Cd="\u03E6",_d="\u03DE",Id="\u039A",kd="\u2090",xd="\u2091",yd="\u2095",Rd="\u1D62",Ad="\u2C7C",Sd="\u2096",Gd="\u2097",Od="\u2098",Ed="\u2099",Td="\u2092",Ud="\u209A",Pd="\u1D63",Ld="\u209B",Bd="\u209C",jd="\u1D64",zd="\u1D65",Dd="\u2093",Nd="\u2080",Hd="\u2081",$d="\u2082",Kd="\u2083",Vd="\u2084",Fd="\u2085",Zd="\u2086",Xd="\u2087",Wd="\u2088",Jd="\u2089",Yd="\u03FA",Qd="\u03E0",th="\u03F7",nh="\u03EC",oh="\u03E2",sh="\u03DA",ch="\u03A3",eh="\u22D0",rh="\u22D1",ih="\u263A",ah="\u03A8",lh="\u03A6",bh="\u03A0",fh="\u03A0\u2080",uh="\u03A0\u2080",ph="\u03A0\u2080",Mh="\u03A0\u2080",gh="\u{1D400}",dh="\u{1D401}",hh="\u{1D402}",mh="\u{1D403}",qh="\u{1D404}",vh="\u{1D405}",wh="\u{1D406}",Ch="\u{1D407}",_h="\u{1D408}",Ih="\u{1D409}",kh="\u{1D40A}",xh="\u{1D40B}",yh="\u{1D40C}",Rh="\u{1D40D}",Ah="\u{1D40E}",Sh="\u{1D40F}",Gh="\u{1D410}",Oh="\u{1D411}",Eh="\u{1D412}",Th="\u{1D413}",Uh="\u{1D414}",Ph="\u{1D415}",Lh="\u{1D416}",Bh="\u{1D417}",jh="\u{1D418}",zh="\u{1D419}",Dh="\u{1D41A}",Nh="\u{1D41B}",Hh="\u{1D41C}",$h="\u{1D41D}",Kh="\u{1D41E}",Vh="\u{1D41F}",Fh="\u{1D420}",Zh="\u{1D421}",Xh="\u{1D422}",Wh="\u{1D423}",Jh="\u{1D424}",Yh="\u{1D425}",Qh="\u{1D426}",tm="\u{1D427}",nm="\u{1D428}",om="\u{1D429}",sm="\u{1D42A}",cm="\u{1D42B}",em="\u{1D42C}",rm="\u{1D42D}",im="\u{1D42E}",am="\u{1D42F}",lm="\u{1D430}",bm="\u{1D431}",fm="\u{1D432}",um="\u{1D433}",pm="\u{1D434}",Mm="\u{1D435}",gm="\u{1D436}",dm="\u{1D437}",hm="\u{1D438}",mm="\u{1D439}",qm="\u{1D43A}",vm="\u{1D43B}",wm="\u{1D43C}",Cm="\u{1D43D}",_m="\u{1D43E}",Im="\u{1D43F}",km="\u{1D440}",xm="\u{1D441}",ym="\u{1D442}",Rm="\u{1D443}",Am="\u{1D444}",Sm="\u{1D445}",Gm="\u{1D446}",Om="\u{1D447}",Em="\u{1D448}",Tm="\u{1D449}",Um="\u{1D44A}",Pm="\u{1D44B}",Lm="\u{1D44C}",Bm="\u{1D44D}",jm="\u{1D44E}",zm="\u{1D44F}",Dm="\u{1D450}",Nm="\u{1D451}",Hm="\u{1D452}",$m="\u{1D453}",Km="\u{1D454}",Vm="\u{1D456}",Fm="\u{1D457}",Zm="\u{1D458}",Xm="\u{1D459}",Wm="\u{1D45A}",Jm="\u{1D45B}",Ym="\u{1D45C}",Qm="\u{1D45D}",tq="\u{1D45E}",nq="\u{1D45F}",oq="\u{1D460}",sq="\u{1D461}",cq="\u{1D462}",eq="\u{1D463}",rq="\u{1D464}",iq="\u{1D465}",aq="\u{1D466}",lq="\u{1D467}",bq="\u{1D468}",fq="\u{1D469}",uq="\u{1D46A}",pq="\u{1D46B}",Mq="\u{1D46C}",gq="\u{1D46D}",dq="\u{1D46E}",hq="\u{1D46F}",mq="\u{1D470}",qq="\u{1D471}",vq="\u{1D472}",wq="\u{1D473}",Cq="\u{1D474}",_q="\u{1D475}",Iq="\u{1D476}",kq="\u{1D477}",xq="\u{1D478}",yq="\u{1D479}",Rq="\u{1D47A}",Aq="\u{1D47B}",Sq="\u{1D47C}",Gq="\u{1D47D}",Oq="\u{1D47E}",Eq="\u{1D47F}",Tq="\u{1D480}",Uq="\u{1D481}",Pq="\u{1D482}",Lq="\u{1D483}",Bq="\u{1D484}",jq="\u{1D485}",zq="\u{1D486}",Dq="\u{1D487}",Nq="\u{1D488}",Hq="\u{1D489}",$q="\u{1D48A}",Kq="\u{1D48B}",Vq="\u{1D48C}",Fq="\u{1D48D}",Zq="\u{1D48E}",Xq="\u{1D48F}",Wq="\u{1D490}",Jq="\u{1D491}",Yq="\u{1D492}",Qq="\u{1D493}",tv="\u{1D494}",nv="\u{1D495}",ov="\u{1D496}",sv="\u{1D497}",cv="\u{1D498}",ev="\u{1D499}",rv="\u{1D49A}",iv="\u{1D49B}",av="\u{1D49C}",lv="\u212C",bv="\u{1D49E}",fv="\u{1D49F}",uv="\u2130",pv="\u2131",Mv="\u{1D4A2}",gv="\u210B",dv="\u2110",hv="\u{1D4A5}",mv="\u{1D4A6}",qv="\u2112",vv="\u2133",wv="\u{1D4A9}",Cv="\u{1D4AA}",_v="\u{1D4AB}",Iv="\u{1D4AC}",kv="\u211B",xv="\u{1D4AE}",yv="\u{1D4AF}",Rv="\u{1D4B0}",Av="\u{1D4B1}",Sv="\u{1D4B2}",Gv="\u{1D4B3}",Ov="\u{1D4B4}",Ev="\u{1D4B5}",Tv="\u{1D4B6}",Uv="\u{1D4B7}",Pv="\u{1D4B8}",Lv="\u{1D4B9}",Bv="\u212F",jv="\u{1D4BB}",zv="\u210A",Dv="\u{1D4BD}",Nv="\u{1D4BE}",Hv="\u{1D4BF}",$v="\u{1D4C0}",Kv="\u{1D4C1}",Vv="\u{1D4C2}",Fv="\u{1D4C3}",Zv="\u2134",Xv="\u{1D4C5}",Wv="\u{1D4C6}",Jv="\u{1D4C7}",Yv="\u{1D4C8}",Qv="\u{1D4C9}",tw="\u{1D4CA}",nw="\u{1D4CB}",ow="\u{1D4CC}",sw="\u{1D4CD}",cw="\u{1D4CE}",ew="\u{1D4CF}",rw="\u{1D4D0}",iw="\u{1D4D1}",aw="\u{1D4D2}",lw="\u{1D4D3}",bw="\u{1D4D4}",fw="\u{1D4D5}",uw="\u{1D4D6}",pw="\u{1D4D7}",Mw="\u{1D4D8}",gw="\u{1D4D9}",dw="\u{1D4DA}",hw="\u{1D4DB}",mw="\u{1D4DC}",qw="\u{1D4DD}",vw="\u{1D4DE}",ww="\u{1D4DF}",Cw="\u{1D4E0}",_w="\u{1D4E1}",Iw="\u{1D4E2}",kw="\u{1D4E3}",xw="\u{1D4E4}",yw="\u{1D4E5}",Rw="\u{1D4E6}",Aw="\u{1D4E7}",Sw="\u{1D4E8}",Gw="\u{1D4E9}",Ow="\u{1D4EA}",Ew="\u{1D4EB}",Tw="\u{1D4EC}",Uw="\u{1D4ED}",Pw="\u{1D4EE}",Lw="\u{1D4EF}",Bw="\u{1D4F0}",jw="\u{1D4F1}",zw="\u{1D4F2}",Dw="\u{1D4F3}",Nw="\u{1D4F4}",Hw="\u{1D4F5}",$w="\u{1D4F6}",Kw="\u{1D4F7}",Vw="\u{1D4F8}",Fw="\u{1D4F9}",Zw="\u{1D4FA}",Xw="\u{1D4FB}",Ww="\u{1D4FC}",Jw="\u{1D4FD}",Yw="\u{1D4FE}",Qw="\u{1D4FF}",tC="\u{1D500}",nC="\u{1D501}",oC="\u{1D502}",sC="\u{1D503}",cC="\u{1D504}",eC="\u{1D505}",rC="\u212D",iC="\u{1D507}",aC="\u{1D508}",lC="\u{1D509}",bC="\u{1D50A}",fC="\u210C",uC="\u2111",pC="\u{1D50D}",MC="\u{1D50E}",gC="\u{1D50F}",dC="\u{1D510}",hC="\u{1D511}",mC="\u{1D512}",qC="\u{1D513}",vC="\u{1D514}",wC="\u211C",CC="\u{1D516}",_C="\u{1D517}",IC="\u{1D518}",kC="\u{1D519}",xC="\u{1D51A}",yC="\u{1D51B}",RC="\u{1D51C}",AC="\u2128",SC="\u{1D51E}",GC="\u{1D51F}",OC="\u{1D520}",EC="\u{1D521}",TC="\u{1D522}",UC="\u{1D523}",PC="\u{1D524}",LC="\u{1D525}",BC="\u{1D526}",jC="\u{1D527}",zC="\u{1D528}",DC="\u{1D529}",NC="\u{1D52A}",HC="\u{1D52B}",$C="\u{1D52C}",KC="\u{1D52D}",VC="\u{1D52E}",FC="\u{1D52F}",ZC="\u{1D530}",XC="\u{1D531}",WC="\u{1D532}",JC="\u{1D533}",YC="\u{1D534}",QC="\u{1D535}",t_="\u{1D536}",n_="\u{1D537}",o_="\xA5",s_="\u03F1",c_="\u03F0",e_="\u03D7",r_="\u2205",i_="\u03D6",a_="\u03D5",l_="\u2032",b_="\u221D",f_="\u03D1",u_="\u22B2",p_="\u22B3",M_="\u03D0",g_="\u03C2",d_="\u22BB",h_="\u2228",m_="\u011B",q_="\u011A",v_="\u22A2",w_="\u22EE",C_="\u010F",__="\u22A8",I_="\u010E",k_="\u010D",x_="\u010C",y_="\u03DF",R_="\u20AD",A_="\u012F",S_="\u012E",G_="\u212A",O_="\u03BA",E_="\u03E7",T_="\u26A0",U_="\u20A9",P_="\u2227",L_="\u2118",B_="\u2240",j_="\u03EE",z_="\u0394",D_="\u03DC",N_="\u25C7",H_="\u21D3",$_="\xD0",K_="\u03B6",V_="\u0397",F_="\u0395",Z_="\u0392",X_="\u25A1",W_="\u224E",J_="\u{1D538}",Y_="\u{1D539}",Q_="\u2102",tI="\u{1D53B}",nI="\u{1D53C}",oI="\u{1D53D}",sI="\u{1D53E}",cI="\u210D",eI="\u{1D540}",rI="\u{1D541}",iI="\u{1D542}",aI="\u{1D543}",lI="\u{1D544}",bI="\u2115",fI="\u{1D546}",uI="\u2119",pI="\u211A",MI="\u211D",gI="\u{1D54A}",dI="\u{1D54B}",hI="\u{1D54C}",mI="\u{1D54D}",qI="\u{1D54E}",vI="\u{1D54F}",wI="\u{1D550}",CI="\u2124",_I="\u{1D552}",II="\u{1D553}",kI="\u{1D554}",xI="\u{1D555}",yI="\u{1D556}",RI="\u{1D557}",AI="\u{1D558}",SI="\u{1D559}",GI="\u{1D55A}",OI="\u{1D55B}",EI="\u{1D55C}",TI="\u{1D55D}",UI="\u{1D55E}",PI="\u{1D55F}",LI="\u{1D560}",BI="\u{1D561}",jI="\u{1D562}",zI="\u{1D563}",DI="\u{1D564}",NI="\u{1D565}",HI="\u{1D566}",$I="\u{1D567}",KI="\u{1D568}",VI="\u{1D569}",FI="\u{1D56A}",ZI="\u{1D56B}",XI="\u211D\u22650",WI="\u211D\u22650",JI="\u211D\u22650\u221E",YI="\u2115\u221E",QI="\u2124\u221A",tk="\u2124\u221A",nk="\u2045",ok="\u2045",sk="\u2046",ck="\u2046",ek="\u{1D4DD}",rk="\u{1D4DD}",ik="\u2A2F",ak="\u2A2F",lk="\u2A2F",bk="\u2A3F",fk="\u2210",uk="\xD7\u1DA0",pk="\u2203\u1DA0",Mk="\u037F",gk="\u22A2",dk="\u22A9",hk="\u2016",mk="\u22AA";var qk={"0":"\u2080","1":"\u2081","2":"\u2082","3":"\u2083","4":"\u2084","5":"\u2085","6":"\u2086","7":"\u2087","8":"\u2088","9":"\u2089","{}":"{$CURSOR}","{}_":"{$CURSOR}_","{{}}":"\u2983$CURSOR\u2984","[]":"[$CURSOR]","[]_":"[$CURSOR]_","[[]]":"\u27E6$CURSOR\u27E7","<>":"\u27E8$CURSOR\u27E9","()":"($CURSOR)","()_":"($CURSOR)_","([])'":"\u27EE$CURSOR\u27EF","f<>":"\u2039$CURSOR\u203A","f<<>>":"\xAB$CURSOR\xBB","[--]":"\u2045$CURSOR\u2046",nnnorm:k,norm:x,floor:y,ceil:R,nfloor:A,nceil:S,"\\":"\\",a:G,b:O,c:E,d:T,e:U,g:P,i:L,m:B,n:j,o:z,p:D,t:N,r:H,u:$,v:K,x:V,"-":"\u207B\xB9","~":"\u223C",".":"\xB7","*":"\u22C6","?":"\xBF",l:F,"<":"\u27E8",">":"\u27E9",O:Z,"&":"\u214B",A:X,C:W,D:J,F:Y,G:Q,H:tt,I:nt,I0:ot,K:st,L:ct,N:et,P:rt,Q:it,R:at,S:lt,U:bt,U0:ft,Z:ut,"#":"\u266F",":":"\u2236","|":"\u2223","!":"\xA1",be:pt,ga:Mt,de:gt,ep:dt,ze:ht,et:mt,th:qt,io:vt,ka:wt,la:Ct,mu:_t,nu:It,xi:kt,pi:xt,rh:yt,vsi:Rt,si:At,ta:St,ph:Gt,ch:Ot,ps:Et,om:Tt,"`A":"\xC0","'A":"\xC1","^{A}":"\xC2","~A":"\xC3",'"A':"\xC4",cC:Ut,"`E":"\xC8","'E":"\xC9","^{E}":"\xCA",'"E':"\xCB","`I":"\xCC","'I":"\xCD","^{I}":"\xCE",'"I':"\xCF","~N":"\xD1","`O":"\xD2","'O":"\xD3","^{O}":"\xD4","~O":"\xD5",'"O':"\xD6","/O":"\xD8","`U":"\xD9","'U":"\xDA","^{U}":"\xDB",'"U':"\xDC","'Y":"\xDD","`a":"\xE0","'a":"\xE1","^{a}":"\xE2","~a":"\xE3",'"a':"\xE4",cc:Pt,"`e":"\xE8","'e":"\xE9","^{e}":"\xEA",'"e':"\xEB","`i":"\xEC","'i":"\xED","^{i}":"\xEE",'"i':"\xEF","~{n}":"\xF1","`o":"\xF2","'o":"\xF3","^{o}":"\xF4","~o":"\xF5",'"o':"\xF6","/o":"\xF8","`u":"\xF9","'u":"\xFA","^{u}":"\xFB",'"u':"\xFC","'y":"\xFD",'"y':"\xFF","/L":"\u0141",notin:Lt,note:Bt,not:jt,nomisma:zt,nin:Dt,nni:Nt,ni:Ht,nattrans:$t,nat_trans:Kt,natural:Vt,nat:Ft,naira:Zt,nabla:Xt,napprox:Wt,numero:Jt,nLeftarrow:Yt,nLeftrightarrow:Qt,nRightarrow:tn,nVDash:nn,nVdash:on,ncong:sn,nearrow:cn,neg:en,nequiv:rn,neq:an,nexists:ln,ne:bn,ngeqq:fn,ngeqslant:un,ngeq:pn,ngtr:Mn,nleftarrow:gn,nleftrightarrow:dn,nleqq:hn,nleqslant:mn,nleq:qn,nless:vn,nmid:wn,nparallel:Cn,npreceq:_n,nprec:In,nrightarrow:kn,nshortmid:xn,nsimeq:yn,nsim:Rn,nsubseteqq:An,nsubseteq:Sn,nsubset:Gn,nsucceq:On,nsucc:En,nsupseteqq:Tn,nsupseteq:Un,nsupset:Pn,ntrianglelefteq:Ln,ntriangleleft:Bn,ntrianglerighteq:jn,ntriangleright:zn,nvDash:Dn,nvdash:Nn,nwarrow:Hn,eqn:$n,equiv:Kn,eqcirc:Vn,eqcolon:Fn,eqslantgtr:Zn,eqslantless:Xn,entails:Wn,en:Jn,exn:Yn,exists:Qn,ex:to,emptyset:no,empty:oo,em:so,epsilon:co,eps:eo,euro:ro,eta:io,ell:ao,iso:lo,in:"\u2208",inn:bo,inter:fo,intercal:uo,intersection:po,integral:Mo,"integral-":"\u2A0D",int:go,inv:ho,increment:mo,inf:qo,infi:vo,infty:wo,iff:Co,imp:_o,imath:Io,iota:ko,"=n":"\u2260","==n":"\u2262","===":"\u2263","==>":"\u27F9","==":"\u2261","=:":"\u2255","=o":"\u2257","=>n":"\u21CF","=>":"\u21D2","~n":"\u2241","~~n":"\u2249","~~~":"\u224B","~~-":"\u224A","~~":"\u2248","~-n":"\u2244","~-":"\u2243","~=n":"\u2247","~=":"\u2245",homotopy:xo,hom:yo,hori:Ro,hookleftarrow:Ao,hookrightarrow:So,hryvnia:Go,heta:Oo,heartsuit:Eo,hbar:To,":~":"\u223B",":=":"\u2254","::-":"\u223A","::":"\u2237","-~":"\u2242","-|":"\u22A3","-1":"\u207B\xB9","^-1":"\u207B\xB9","-2":"\u207B\xB2","-3":"\u207B\xB3","-:":"\u2239","->n":"\u219B","->":"\u2192","-->":"\u27F6","---":"\u2500","--=":"\u2550","--_":"\u2501","--.":"\u254C","-o":"\u22B8",".=.":"\u2251",".=":"\u2250",".+":"\u2214",".-":"\u2238","...":"\u22EF","(=":"\u2258","(b":"\u27C5","and=":"\u2259",and:Uo,an:Po,angle:Lo,rightangle:Bo,angstrom:jo,all:zo,allf:Do,"all^f":"\u2200\u1DA0",allm:No,"all^m":"\u2200\u1D50",alpha:Ho,aleph:$o,aleph0:Ko,asterisk:Vo,ast:Fo,asymp:Zo,apl:Xo,approxeq:Wo,approx:Jo,aa:Yo,ae:Qo,austral:ts,afghani:ns,amalg:os,average:ss,"-int":"\u2A0D","or=":"\u225A",ordfeminine:cs,ordmasculine:es,or:rs,oplus:is,od:as,orderdual:ls,addopposite:bs,aop:fs,mulopposite:us,mop:ps,opposite:Ms,op:gs,"o+":"\u2295","o--":"\u2296","o-":"\u229D",ox:ds,"o/":"\u2298","o.":"\u2299",oo:hs,"o*":"\u2218*","o=":"\u229C",oe:ms,octagonal:qs,ohm:vs,ounce:ws,omega:Cs,omicron:_s,ominus:Is,odot:ks,oint:xs,oiint:ys,oslash:Rs,otimes:As,tensorproduct:Ss,pitensorproduct:Gs,tensorpower:Os,pd:Es,"*=":"\u225B","t=":"\u225C",tint:Ts,transport:Us,trans:Ps,triangledown:Ls,trianglelefteq:Bs,triangleleft:js,triangleq:zs,trianglerighteq:Ds,triangleright:Ns,triangle:Hs,tr:$s,tb:Ks,twoheadleftarrow:Vs,twoheadrightarrow:Fs,tw:Zs,tie:Xs,times:Ws,theta:Js,therefore:Ys,thickapprox:Qs,thicksim:tc,telephone:nc,tenge:oc,textmusicalnote:sc,textmu:cc,textfractionsolidus:ec,textbaht:rc,textdied:ic,textdiscount:ac,textcolonmonetary:lc,textcircledP:bc,textwon:fc,textnaira:uc,textnumero:pc,textpeso:Mc,textpertenthousand:gc,textlira:dc,textlquill:hc,textrecipe:mc,textreferencemark:qc,textrquill:vc,textinterrobang:wc,textestimated:Cc,textopenbullet:_c,tugrik:Ic,tau:kc,top:xc,to:yc,to0:Rc,r0:Ac,to_0:Sc,r_0:Gc,finsupp:Oc,to1:Ec,r1:Tc,to_1:Uc,r_1:Pc,l1:Lc,to1s:Bc,r1s:jc,to_1s:zc,r_1s:Dc,l1simplefunc:Nc,toa:Hc,ra:$c,to_a:Kc,r_a:Vc,alghom:Fc,tob:Zc,rb:Xc,"to^b":"\u2192\u1D47","r^b":"\u2192\u1D47",boundedcontinuousfunction:Wc,tol:Jc,rl:Yc,to_l:Qc,r_l:te,linearmap:ne,tom:oe,rm:se,to_m:ce,r_m:ee,aeeqfun:re,rp:ie,to_p:ae,r_p:le,dfinsupp:be,tos:fe,rs:ue,to_s:pe,r_s:Me,simplefunc:ge,heyting:de,himp:he,hnot:me,covers:qe,covby:ve,wcovby:we,wcovers:Ce,"def=":"\u225D",defs:_e,degree:Ie,dei:ke,delta:xe,doteqdot:ye,doteq:Re,dotplus:Ae,dotsquare:Se,dot:Ge,dong:Oe,downarrow:Ee,downdownarrows:Te,downleftharpoon:Ue,downrightharpoon:Pe,"dr-":"\u2198","dr=":"\u21D8",drachma:Le,dr:Be,"dl-":"\u2199","dl=":"\u21D9",dl:je,"d-2":"\u21CA","d-u-":"\u21F5","d-|":"\u21A7","d-":"\u2193","d==":"\u27F1","d=":"\u21D3","dd-":"\u21A1",ddagger:ze,ddag:De,ddots:Ne,dz:He,dib:$e,diw:Ke,"di.":"\u25C8",die:Ve,division:Fe,divideontimes:Ze,div:Xe,diameter:We,diamondsuit:Je,diamond:Ye,digamma:Qe,di:tr,dagger:nr,dag:or,daleth:sr,dashv:cr,dh:er,dvd:rr,"m=":"\u225E",meet:ir,member:ar,mem:lr,measuredangle:br,mapsto:fr,male:ur,maltese:pr,manat:Mr,"mathscr{I}":"\u2110",minus:gr,mill:dr,micro:hr,mid:mr,multiplication:qr,multimap:vr,mho:wr,models:Cr,mp:_r,"?=":"\u225F","??":"\u2047","?!":"\u203D",prohibited:Ir,prod:kr,propto:xr,precapprox:yr,preceq:Rr,precnapprox:Ar,precnsim:Sr,precsim:Gr,prec:Or,preim:Er,preimage:Tr,prime:Ur,pr:Pr,powerset:Lr,pounds:Br,pound:jr,pab:zr,paw:Dr,partnership:Nr,partial:Hr,paragraph:$r,parallel:Kr,pa:Vr,pm:Fr,perp:Zr,"^perp":"\u15EE",permil:Xr,per:Wr,peso:Jr,peseta:Yr,pilcrow:Qr,pitchfork:ti,psi:ni,phi:oi,"8<":"\u2702",leqn:si,leqq:ci,leqslant:ei,leq:ri,len:ii,leadsto:ai,leftarrowtail:li,leftarrow:bi,leftharpoondown:fi,leftharpoonup:ui,leftleftarrows:pi,leftrightarrows:Mi,leftrightarrow:gi,leftrightharpoons:di,leftrightsquigarrow:hi,leftthreetimes:mi,lessapprox:qi,lessdot:vi,lesseqgtr:wi,lesseqqgtr:Ci,lessgtr:_i,lesssim:Ii,le:ki,lub:xi,"lr--":"\u27F7","lr-n":"\u21AE","lr-":"\u2194","lr=n":"\u21CE","lr=":"\u21D4","lr~":"\u21AD",lrcorner:yi,lr:Ri,"l-2":"\u21C7","l-r-":"\u21C6","l--":"\u27F5","l-n":"\u219A","l-|":"\u21A4","l->":"\u21A2","l-":"\u2190","l==":"\u21DA","l=n":"\u21CD","l=":"\u21D0","l~":"\u219C","ll-":"\u219E",llcorner:Ai,llbracket:Si,ll:Gi,lbag:Oi,lambda:Ei,lamda:Ti,lam:Ui,lari:Pi,langle:Li,lira:Bi,lceil:ji,ldots:zi,ldq:Di,ldata:Ni,lfloor:Hi,lf:$i,"<|":"\u29CF",lhd:Ki,lnapprox:Vi,lneqq:Fi,lneq:Zi,lnsim:Xi,lnot:Wi,longleftarrow:Ji,longleftrightarrow:Yi,longrightarrow:Qi,looparrowleft:ta,looparrowright:na,lozenge:oa,lq:sa,ltimes:ca,lvertneqq:ea,geqn:ra,geqq:ia,geqslant:aa,geq:la,gen:ba,gets:fa,ge:ua,glb:pa,glqq:Ma,glq:ga,guarani:da,gangia:ha,gamma:ma,ggg:qa,gg:va,gimel:wa,gnapprox:Ca,gneqq:_a,gneq:Ia,gnsim:ka,gtrapprox:xa,gtrdot:ya,gtreqless:Ra,gtreqqless:Aa,gtrless:Sa,gtrsim:Ga,gvertneqq:Oa,grqq:Ea,grq:Ta,"<=n":"\u2270","<=>n":"\u21CE","<=>":"\u21D4","<=":"\u2264","":"\u22D7","<->n":"\u21AE","<->":"\u2194","<-->":"\u27F7","<--":"\u27F5","<-n":"\u219A","<-":"\u2190","<<":"\u27EA",">=n":"\u2271",">=":"\u2265",">n":"\u226F",">~nn":"\u2275",">~n":"\u22E7",">~":"\u2273",">>":"\u27EB",root:Ua,ssubn:Pa,ssub:La,ssupn:Ba,ssup:ja,ssqub:za,ssqup:Da,ss:Na,subn:Ha,subseteqq:$a,subseteq:Ka,subsetneqq:Va,subsetneq:Fa,subset:Za,ssubset:Xa,sub:Wa,supn:Ja,supseteqq:Ya,supseteq:Qa,supsetneqq:tl,supsetneq:nl,supset:ol,ssupset:sl,sUnion:cl,sInter:el,sup:rl,supr:il,surd3:al,surd4:ll,surd:bl,succapprox:fl,succcurlyeq:ul,succeq:pl,succnapprox:Ml,succnsim:gl,succsim:dl,succ:hl,sum:ml,specializes:ql,"~>":"\u2933",squbn:vl,squb:wl,squpn:Cl,squp:_l,square:Il,squigarrowright:kl,sqb:xl,sqw:yl,"sq.":"\u25A3",sqo:Rl,sqcap:Al,sqcup:Sl,sqrt:Gl,sqsubseteq:Ol,sqsubset:El,sqsupseteq:Tl,sqsupset:Ul,sq:Pl,sy:Ll,symmdiff:Bl,st4:jl,st6:zl,st8:Dl,st12:Nl,stigma:Hl,star:$l,straightphi:Kl,st:Vl,spesmilo:Fl,span:Zl,spadesuit:Xl,sphericalangle:Wl,section:Jl,searrow:Yl,setminus:Ql,san:tb,sampi:nb,shortmid:ob,sho:sb,shima:cb,shei:eb,sharp:rb,sigma:ib,simeq:ab,sim:lb,sbs:bb,smallamalg:fb,smallsetminus:ub,smallsmile:pb,smile:Mb,smul:gb,swarrow:db,Tr:hb,Tb:mb,Tw:qb,Tau:vb,Theta:wb,TH:Cb,union:_b,undertie:Ib,uncertainty:kb,un:xb,"u+":"\u228E","u.":"\u228D","ud-|":"\u21A8","ud-":"\u2195","ud=":"\u21D5",ud:yb,"ul-":"\u2196","ul=":"\u21D6",ulcorner:Rb,ul:Ab,"ur-":"\u2197","ur=":"\u21D7",urcorner:Sb,ur:Gb,"u-2":"\u21C8","u-d-":"\u21C5","u-|":"\u21A5","u-":"\u2191","u==":"\u27F0","u=":"\u21D1","uu-":"\u219F",upsilon:Ob,uparrow:Eb,updownarrow:Tb,upleftharpoon:Ub,uplus:Pb,uprightharpoon:Lb,upuparrows:Bb,And:jb,AA:zb,AE:Db,Alpha:Nb,Or:Hb,"O+":"\u2A01",directsum:$b,Ox:Kb,"O.":"\u2A00","O*":"\u235F",OE:Vb,Omega:Fb,Omicron:Zb,Int:Xb,Inter:Wb,bInter:Jb,Iota:Yb,Im:Qb,Un:tf,Union:nf,bUnion:of,"U+":"\u2A04","U.":"\u2A03",Upsilon:sf,Uparrow:cf,Updownarrow:ef,"Gl-":"\u019B",Gl:rf,Gangia:af,Gamma:lf,Glb:bf,Ga:ff,GA:uf,Gb:pf,GB:Mf,Gg:gf,GG:df,Gd:hf,GD:mf,Ge:qf,GE:vf,Gz:wf,GZ:Cf,Gth:_f,Gt:If,GTH:kf,GT:xf,Gi:yf,GI:Rf,Gk:Af,GK:Sf,GL:Gf,Gm:Of,GM:Ef,Gn:Tf,GN:Uf,Gx:Pf,GX:Lf,Gr:Bf,GR:jf,Gs:zf,GS:Df,Gu:Nf,GU:Hf,Gf:$f,GF:Kf,Gc:Vf,GC:Ff,Gp:Zf,GP:Xf,Go:Wf,GO:Jf,Inf:Yf,Join:Qf,Lub:tu,Lambda:nu,Lamda:ou,Leftarrow:su,Leftrightarrow:cu,Letter:eu,Lleftarrow:ru,Ll:iu,Longleftarrow:au,Longleftrightarrow:lu,Longrightarrow:bu,Meet:fu,Sup:uu,Sqcap:pu,Sqcup:Mu,Lsh:gu,"|-n":"\u22AC","|-":"\u22A2","|=n":"\u22AD","|=":"\u22A8","|->":"\u21A6","|=>":"\u21F0","||-n":"\u22AE","||-":"\u22A9","||=n":"\u22AF","||=":"\u22AB","|||-":"\u22AA","||":"\u2016",fuzzy:du,"|n":"\u2224",Com:hu,Chi:mu,Cap:qu,Cup:vu,cul:wu,cuL:Cu,currency:_u,curlyeqprec:Iu,curlyeqsucc:ku,curlypreceq:xu,curlyvee:yu,curlywedge:Ru,curvearrowleft:Au,curvearrowright:Su,cur:Gu,cuR:Ou,cup:Eu,cu:Tu,cll:Uu,clL:Pu,clr:Lu,clR:Bu,clubsuit:ju,cl:zu,construction:Du,cong:Nu,con:Hu,compl:$u,complement:Ku,complementprefix:Vu,Complement:Fu,comp:Zu,com:Xu,coloneq:Wu,colon:Ju,copyright:Yu,cdots:Qu,cdot:tp,cib:np,ciw:op,"ci..":"\u25CC","ci.":"\u25CE",ciO:sp,circeq:cp,circlearrowleft:ep,circlearrowright:rp,circledR:ip,circledS:ap,circledast:lp,circledcirc:bp,circleddash:fp,circ:up,ci:pp,centerdot:Mp,cent:gp,cedi:dp,celsius:hp,ce:mp,checkmark:qp,chi:vp,cruzeiro:wp,caution:Cp,cap:_p,qed:Ip,quad:kp,quot:xp,bigsolidus:yp,"/":"\u29F8","+ ":"\u22B9","b+":"\u229E","b-":"\u229F",bx:Rp,"b.":"\u22A1",bn:Ap,bz:Sp,bq:Gp,brokenbar:Op,br:Ep,bc:Tp,bp:Up,bb:Pp,bsum:Lp,b0:Bp,b1:jp,b2:zp,b3:Dp,b4:Np,b5:Hp,b6:$p,b7:Kp,b8:Vp,b9:Fp,sb0:Zp,sb1:Xp,sb2:Wp,sb3:Jp,sb4:Yp,sb5:Qp,sb6:tM,sb7:nM,sb8:oM,sb9:sM,bub:cM,buw:eM,but:rM,bumpeq:iM,bu:aM,biohazard:lM,bihimp:bM,bigcap:fM,bigcirc:uM,bigcoprod:pM,bigcup:MM,bigglb:gM,biginf:dM,bigjoin:hM,biglub:mM,bigmeet:qM,bigsqcap:vM,bigsqcup:wM,bigstar:CM,bigsup:_M,bigtriangledown:IM,bigtriangleup:kM,bigvee:xM,bigwedge:yM,beta:RM,beth:AM,between:SM,because:GM,backcong:OM,backepsilon:EM,backprime:TM,backsimeq:UM,backsim:PM,barwedge:LM,blacklozenge:BM,blacksquare:jM,blacksmiley:zM,blacktriangledown:DM,blacktriangleleft:NM,blacktriangleright:HM,blacktriangle:$M,bot:KM,"^bot":"\u15EE",bowtie:VM,boxminus:FM,boxmid:ZM,hcomp:XM,boxplus:WM,boxtimes:JM,join:YM,"r-2":"\u21C9","r-3":"\u21F6","r-l-":"\u21C4","r--":"\u27F6","r-n":"\u219B","r-|":"\u21A6","r->":"\u21A3","r-o":"\u22B8","r-":"\u2192","r==":"\u21DB","r=n":"\u21CF","r=":"\u21D2","r~":"\u219D","rr-":"\u21A0",reb:QM,rew:tg,real:ng,registered:og,re:sg,rbag:cg,rat:eg,radioactive:rg,rrbracket:ig,rangle:ag,rq:lg,rial:bg,rightarrowtail:fg,rightarrow:ug,rightharpoondown:pg,rightharpoonup:Mg,rightleftarrows:gg,rightleftharpoons:dg,rightrightarrows:hg,rightthreetimes:mg,risingdotseq:qg,ruble:vg,rupee:wg,rho:Cg,rhd:_g,rceil:Ig,rfloor:kg,rtimes:xg,rdq:yg,rdata:Rg,functor:Ag,fun:Sg,"f<<":"\xAB","f>>":"\xBB","f<":"\u2039","f>":"\u203A",finprod:Gg,finsum:Og,frac12:Eg,frac13:Tg,frac14:Ug,frac15:Pg,frac16:Lg,frac18:Bg,frac1:jg,frac23:zg,frac25:Dg,frac34:Ng,frac35:Hg,frac38:$g,frac45:Kg,frac56:Vg,frac58:Fg,frac78:Zg,frac:Xg,frown:Wg,frqq:Jg,frq:Yg,female:Qg,fei:td,facsimile:nd,fallingdotseq:od,flat:sd,flqq:cd,flq:ed,forall:rd,")b":"\u27C6","[[":"\u27E6","]]":"\u27E7","{{":"\u2983","}}":"\u2984","([":"\u27EE","])":"\u27EF",Xi:id,Nat:ad,Nu:ld,Zeta:bd,Rat:fd,Real:ud,Re:pd,Rho:Md,Rightarrow:gd,Rrightarrow:dd,Rsh:hd,Fei:md,Frowny:qd,Hori:vd,Heta:wd,Khei:Cd,Koppa:_d,Kappa:Id,"^a":"\u1D43","^b":"\u1D47","^c":"\u1D9C","^d":"\u1D48","^e":"\u1D49","^f":"\u1DA0","^g":"\u1D4D","^h":"\u02B0","^i":"\u2071","^j":"\u02B2","^k":"\u1D4F","^l":"\u02E1","^m":"\u1D50","^n":"\u207F","^o":"\u1D52","^p":"\u1D56","^r":"\u02B3","^s":"\u02E2","^t":"\u1D57","^u":"\u1D58","^v":"\u1D5B","^w":"\u02B7","^x":"\u02E3","^y":"\u02B8","^z":"\u1DBB","^A":"\u1D2C","^B":"\u1D2E","^D":"\u1D30","^E":"\u1D31","^G":"\u1D33","^H":"\u1D34","^I":"\u1D35","^J":"\u1D36","^K":"\u1D37","^L":"\u1D38","^M":"\u1D39","^N":"\u1D3A","^O":"\u1D3C","^P":"\u1D3E","^R":"\u1D3F","^T":"\u1D40","^U":"\u1D41","^V":"\u2C7D","^W":"\u1D42","^0":"\u2070","^1":"\xB9","^2":"\xB2","^3":"\xB3","^4":"\u2074","^5":"\u2075","^6":"\u2076","^7":"\u2077","^8":"\u2078","^9":"\u2079","^)":"\u207E","^(":"\u207D","^=":"\u207C","^+":"\u207A","^o_":"\xBA","^-":"\u207B","^a_":"\xAA","^uhook":"\uAB5F","^ubar":"\u1DB6","^upsilon":"\u1DB7","^ltilde":"\uAB5E","^ls":"\uAB5D","^lhook":"\u1DAA","^lretroflexhook":"\u1DA9","^oe":"\uA7F9","^heng":"\uAB5C","^hhook":"\u02B1","^hwithhook":"\u02B1","^Hstroke":"\uA7F8","^theta":"\u1DBF","^turnedv":"\u1DBA","^turnedmleg":"\u1DAD","^turnedm":"\u1D5A","^turnedh":"\u1DA3","^turnedalpha":"\u1D9B","^turnedae":"\u1D46","^turneda":"\u1D44","^turnedi":"\u1D4E","^turnede":"\u1D4C","^turnedrhook":"\u02B5","^turnedrwithhook":"\u02B5","^turnedr":"\u02B4","^twithpalatalhook":"\u1DB5","^otop":"\u1D54","^ezh":"\u1DBE","^esh":"\u1DB4","^eth":"\u1D9E","^eng":"\u1D51","^zcurl":"\u1DBD","^zretroflexhook":"\u1DBC","^vhook":"\u1DB9","^Ismall":"\u1DA6","^Lsmall":"\u1DAB","^Nsmall":"\u1DB0","^Usmall":"\u1DB8","^Istroke":"\u1DA7","^Rinverted":"\u02B6","^ccurl":"\u1D9D","^chi":"\u1D61","^shook":"\u1DB3","^gscript":"\u1DA2","^schwa":"\u1D4A","^usideways":"\u1D59","^phi":"\u1DB2","^obarred":"\u1DB1","^beta":"\u1D5D","^obottom":"\u1D55","^nretroflexhook":"\u1DAF","^nlefthook":"\u1DAE","^mhook":"\u1DAC","^jtail":"\u1DA8","^iota":"\u1DA5","^istroke":"\u1DA4","^ereversedopen":"\u1D9F","^stop":"\u02E4","^varphi":"\u1D60","^vargamma":"\u1D5E","^gamma":"\u02E0","^ain":"\u1D5C","^alpha":"\u1D45","^oopen":"\u1D53","^eopen":"\u1D4B","^Ou":"\u1D3D","^Nreversed":"\u1D3B","^Ereversed":"\u1D32","^Bbarred":"\u1D2F","^Ae":"\u1D2D","^SM":"\u2120","^TEL":"\u2121","^TM":"\u2122",_a:kd,_e:xd,_h:yd,_i:Rd,_j:Ad,_k:Sd,_l:Gd,_m:Od,_n:Ed,_o:Td,_p:Ud,_r:Pd,_s:Ld,_t:Bd,_u:jd,_v:zd,_x:Dd,_0:Nd,_1:Hd,_2:$d,_3:Kd,_4:Vd,_5:Fd,_6:Zd,_7:Xd,_8:Wd,_9:Jd,"_)":"\u208E","_(":"\u208D","_=":"\u208C","_+":"\u208A","_--":"\u0332","_-":"\u208B","!!":"\u203C","!?":"\u2049",San:Yd,Sampi:Qd,Sho:th,Shima:nh,Shei:oh,Stigma:sh,Sigma:ch,Subset:eh,Supset:rh,Smiley:ih,Psi:ah,Phi:lh,Pi:bh,Pi0:fh,P0:uh,Pi_0:ph,P_0:Mh,bfA:gh,bfB:dh,bfC:hh,bfD:mh,bfE:qh,bfF:vh,bfG:wh,bfH:Ch,bfI:_h,bfJ:Ih,bfK:kh,bfL:xh,bfM:yh,bfN:Rh,bfO:Ah,bfP:Sh,bfQ:Gh,bfR:Oh,bfS:Eh,bfT:Th,bfU:Uh,bfV:Ph,bfW:Lh,bfX:Bh,bfY:jh,bfZ:zh,bfa:Dh,bfb:Nh,bfc:Hh,bfd:$h,bfe:Kh,bff:Vh,bfg:Fh,bfh:Zh,bfi:Xh,bfj:Wh,bfk:Jh,bfl:Yh,bfm:Qh,bfn:tm,bfo:nm,bfp:om,bfq:sm,bfr:cm,bfs:em,bft:rm,bfu:im,bfv:am,bfw:lm,bfx:bm,bfy:fm,bfz:um,MiA:pm,MiB:Mm,MiC:gm,MiD:dm,MiE:hm,MiF:mm,MiG:qm,MiH:vm,MiI:wm,MiJ:Cm,MiK:_m,MiL:Im,MiM:km,MiN:xm,MiO:ym,MiP:Rm,MiQ:Am,MiR:Sm,MiS:Gm,MiT:Om,MiU:Em,MiV:Tm,MiW:Um,MiX:Pm,MiY:Lm,MiZ:Bm,Mia:jm,Mib:zm,Mic:Dm,Mid:Nm,Mie:Hm,Mif:$m,Mig:Km,Mii:Vm,Mij:Fm,Mik:Zm,Mil:Xm,Mim:Wm,Min:Jm,Mio:Ym,Mip:Qm,Miq:tq,Mir:nq,Mis:oq,Mit:sq,Miu:cq,Miv:eq,Miw:rq,Mix:iq,Miy:aq,Miz:lq,MIA:bq,MIB:fq,MIC:uq,MID:pq,MIE:Mq,MIF:gq,MIG:dq,MIH:hq,MII:mq,MIJ:qq,MIK:vq,MIL:wq,MIM:Cq,MIN:_q,MIO:Iq,MIP:kq,MIQ:xq,MIR:yq,MIS:Rq,MIT:Aq,MIU:Sq,MIV:Gq,MIW:Oq,MIX:Eq,MIY:Tq,MIZ:Uq,MIa:Pq,MIb:Lq,MIc:Bq,MId:jq,MIe:zq,MIf:Dq,MIg:Nq,MIh:Hq,MIi:$q,MIj:Kq,MIk:Vq,MIl:Fq,MIm:Zq,MIn:Xq,MIo:Wq,MIp:Jq,MIq:Yq,MIr:Qq,MIs:tv,MIt:nv,MIu:ov,MIv:sv,MIw:cv,MIx:ev,MIy:rv,MIz:iv,McA:av,McB:lv,McC:bv,McD:fv,McE:uv,McF:pv,McG:Mv,McH:gv,McI:dv,McJ:hv,McK:mv,McL:qv,McM:vv,McN:wv,McO:Cv,McP:_v,McQ:Iv,McR:kv,McS:xv,McT:yv,McU:Rv,McV:Av,McW:Sv,McX:Gv,McY:Ov,McZ:Ev,Mca:Tv,Mcb:Uv,Mcc:Pv,Mcd:Lv,Mce:Bv,Mcf:jv,Mcg:zv,Mch:Dv,Mci:Nv,Mcj:Hv,Mck:$v,Mcl:Kv,Mcm:Vv,Mcn:Fv,Mco:Zv,Mcp:Xv,Mcq:Wv,Mcr:Jv,Mcs:Yv,Mct:Qv,Mcu:tw,Mcv:nw,Mcw:ow,Mcx:sw,Mcy:cw,Mcz:ew,MCA:rw,MCB:iw,MCC:aw,MCD:lw,MCE:bw,MCF:fw,MCG:uw,MCH:pw,MCI:Mw,MCJ:gw,MCK:dw,MCL:hw,MCM:mw,MCN:qw,MCO:vw,MCP:ww,MCQ:Cw,MCR:_w,MCS:Iw,MCT:kw,MCU:xw,MCV:yw,MCW:Rw,MCX:Aw,MCY:Sw,MCZ:Gw,MCa:Ow,MCb:Ew,MCc:Tw,MCd:Uw,MCe:Pw,MCf:Lw,MCg:Bw,MCh:jw,MCi:zw,MCj:Dw,MCk:Nw,MCl:Hw,MCm:$w,MCn:Kw,MCo:Vw,MCp:Fw,MCq:Zw,MCr:Xw,MCs:Ww,MCt:Jw,MCu:Yw,MCv:Qw,MCw:tC,MCx:nC,MCy:oC,MCz:sC,MfA:cC,MfB:eC,MfC:rC,MfD:iC,MfE:aC,MfF:lC,MfG:bC,MfH:fC,MfI:uC,MfJ:pC,MfK:MC,MfL:gC,MfM:dC,MfN:hC,MfO:mC,MfP:qC,MfQ:vC,MfR:wC,MfS:CC,MfT:_C,MfU:IC,MfV:kC,MfW:xC,MfX:yC,MfY:RC,MfZ:AC,Mfa:SC,Mfb:GC,Mfc:OC,Mfd:EC,Mfe:TC,Mff:UC,Mfg:PC,Mfh:LC,Mfi:BC,Mfj:jC,Mfk:zC,Mfl:DC,Mfm:NC,Mfn:HC,Mfo:$C,Mfp:KC,Mfq:VC,Mfr:FC,Mfs:ZC,Mft:XC,Mfu:WC,Mfv:JC,Mfw:YC,Mfx:QC,Mfy:t_,Mfz:n_,yen:o_,varrho:s_,varkappa:c_,varkai:e_,varnothing:r_,varpi:i_,varphi:a_,varprime:l_,varpropto:b_,vartheta:f_,vartriangleleft:u_,vartriangleright:p_,varbeta:M_,varsigma:g_,veebar:d_,vee:h_,ve:m_,vE:q_,vdash:v_,vdots:w_,vd:C_,vDash:__,vD:I_,vc:k_,vC:x_,koppa:y_,kip:R_,ki:A_,kI:S_,kelvin:G_,kappa:O_,khei:E_,warning:T_,won:U_,wedge:P_,wp:L_,wr:B_,Dei:j_,Delta:z_,Digamma:D_,Diamond:N_,Downarrow:H_,DH:$_,zeta:K_,Eta:V_,Epsilon:F_,Beta:Z_,Box:X_,Bumpeq:W_,bbA:J_,bbB:Y_,bbC:Q_,bbD:tI,bbE:nI,bbF:oI,bbG:sI,bbH:cI,bbI:eI,bbJ:rI,bbK:iI,bbL:aI,bbM:lI,bbN:bI,bbO:fI,bbP:uI,bbQ:pI,bbR:MI,bbS:gI,bbT:dI,bbU:hI,bbV:mI,bbW:qI,bbX:vI,bbY:wI,bbZ:CI,bba:_I,bbb:II,bbc:kI,bbd:xI,bbe:yI,bbf:RI,bbg:AI,bbh:SI,bbi:GI,bbj:OI,bbk:EI,bbl:TI,bbm:UI,bbn:PI,bbo:LI,bbp:BI,bbq:jI,bbr:zI,bbs:DI,bbt:NI,bbu:HI,bbv:$I,bbw:KI,bbx:VI,bby:FI,bbz:ZI,Rge0:XI,"R>=0":"\u211D\u22650",nnreal:WI,ennreal:JI,enat:YI,Zsqrt:QI,zsqrtd:tk,liel:nk,bracketl:ok,lier:sk,"[-":"\u2045","-]":"\u2046",bracketr:ck,nhds:ek,nbhds:rk,X:ik,vectorproduct:ak,crossproduct:lk,coprod:bk,sigmaobj:fk,xf:uk,exf:pk,"c[":"\u2983","c]":"\u2984",Yot:Mk,goal:gk,Vdash:dk,Vert:hk,Vvdash:mk},vk=d(function(a,e){var r=g&&g.__importDefault||function(o){return o&&o.__esModule?o:{default:o}};Object.defineProperty(e,"__esModule",{value:!0}),e.AbbreviationProvider=void 0;const p=r(qk);class t{constructor(n){l(this,"config");l(this,"replacementTextCache",{});l(this,"symbolsByAbbreviation",{});this.config=n,this.symbolsByAbbreviation={...p.default,...this.config.customTranslations}}getSymbolsByAbbreviation(){return this.symbolsByAbbreviation}collectAllAbbreviations(n){return Object.entries(this.symbolsByAbbreviation).filter(([s,c])=>c===n).map(([s])=>s)}findAutoClosingAbbreviations(n){return Object.entries(this.symbolsByAbbreviation).filter(([s,c])=>c.startsWith(`${n}$CURSOR`)).map(([s,c])=>[s,c.replace(`${n}$CURSOR`,"")])}findSymbolsIn(n){const s=new Set;for(const[c,f]of Object.entries(this.symbolsByAbbreviation))n.startsWith(f)&&s.add(f);return[...s.values()]}getReplacementText(n){if(n in this.replacementTextCache)return this.replacementTextCache[n];const s=this.findReplacementText(n);return this.replacementTextCache[n]=s,s}findReplacementText(n){if(n.length===0)return;const s=this.findSymbolsByAbbreviationPrefix(n)[0];if(s)return s;const c=this.getReplacementText(n.slice(0,n.length-1));return c?c+n.slice(n.length-1):void 0}getSymbolForAbbreviation(n){return this.symbolsByAbbreviation[n]}findSymbolsByAbbreviationPrefix(n){const s=Object.keys(this.symbolsByAbbreviation).filter(c=>c.startsWith(n));return s.sort((c,f)=>c.length-f.length),s.map(c=>this.symbolsByAbbreviation[c])}}e.AbbreviationProvider=t}),M=d(function(a,e){Object.defineProperty(e,"__esModule",{value:!0}),e.Range=void 0;class r{constructor(t,o){l(this,"offset");l(this,"length");if(this.offset=t,this.length=o,o<0)throw new Error}contains(t){return this.offset<=t&&t<=this.offsetEnd}get offsetEnd(){return this.offset+this.length-1}get isEmpty(){return this.length===0}toString(){return`[${this.offset}, +${this.length})`}move(t){return new r(this.offset+t,this.length)}moveKeepEnd(t){if(t>this.length)throw new Error;const o=new r(this.offset+t,this.length-t);return o}moveEnd(t){return new r(this.offset,this.length+t)}withLength(t){return new r(this.offset,t)}containsRange(t){return this.offset<=t.offset&&t.offsetEnd<=this.offsetEnd}isAfter(t){return t.offsetEndthis.offsetEnd}equals(t){return this.offset===t.offset&&this.length===t.length}}e.Range=r}),q=d(function(a,e){Object.defineProperty(e,"__esModule",{value:!0}),e.TrackedAbbreviation=void 0;class r{constructor(t,o,n){l(this,"_text");l(this,"abbreviationProvider");l(this,"_abbreviationRange");l(this,"_finished",!1);this._text=o,this.abbreviationProvider=n,this._abbreviationRange=t}get abbreviationRange(){return this._abbreviationRange}get range(){return this.abbreviationRange.moveKeepEnd(-1)}get abbreviation(){return this._text}get matchingSymbol(){return this.abbreviationProvider.getReplacementText(this.abbreviation)}get isAbbreviationUniqueAndComplete(){return this.abbreviationProvider.findSymbolsByAbbreviationPrefix(this.abbreviation).length===1&&!!this.abbreviationProvider.getSymbolForAbbreviation(this.abbreviation)}get finished(){return this._finished}processChange(t,o){if(this.abbreviationRange.containsRange(t)){if(this._finished=!1,this.abbreviationRange.isBefore(t)&&this.abbreviationProvider.findSymbolsByAbbreviationPrefix(this.abbreviation+o).length===0)return this._finished=!0,{shouldStopTracking:!1,isAffected:!1};this._abbreviationRange=this.abbreviationRange.moveEnd(o.length-t.length);const n=this.abbreviation.substr(0,t.offset-this.abbreviationRange.offset),s=this.abbreviation.substr(t.offsetEnd+1-this.abbreviationRange.offset);return this._text=n+o+s,{shouldStopTracking:!1,isAffected:!0}}else return t.isBefore(this.range)?(this._abbreviationRange=this._abbreviationRange.move(o.length-t.length),{shouldStopTracking:!1,isAffected:!1}):t.isAfter(this.range)?{shouldStopTracking:!1,isAffected:!1}:{shouldStopTracking:!0,isAffected:!1}}}e.TrackedAbbreviation=r}),wk=d(function(a,e){Object.defineProperty(e,"__esModule",{value:!0}),e.AbbreviationRewriter=void 0;class r{constructor(t,o,n){l(this,"config");l(this,"abbreviationProvider");l(this,"textSource");l(this,"trackedAbbreviations",new Set);l(this,"doNotTrackNewAbbr",!1);this.config=t,this.abbreviationProvider=o,this.textSource=n}changeInput(t){t.sort((o,n)=>n.range.offset-o.range.offset);for(const o of t)this.processChange(o)}async triggerAbbreviationReplacement(){await this.forceReplace([...this.trackedAbbreviations].filter(t=>t.finished||this.config.eagerReplacementEnabled&&t.isAbbreviationUniqueAndComplete))}async changeSelections(t){await this.forceReplace([...this.trackedAbbreviations].filter(o=>!t.some(n=>o.range.containsRange(n.withLength(0)))))}async replaceAllTrackedAbbreviations(){await this.forceReplace([...this.trackedAbbreviations])}getTrackedAbbreviations(){return this.trackedAbbreviations}resetTrackedAbbreviations(){this.trackedAbbreviations.clear()}async forceReplace(t){if(t.length===0)return;for(const c of t)this.trackedAbbreviations.delete(c);const o=r.computeReplacements(t);o.sort((c,f)=>c.change.range.offset-f.change.range.offset);const n=this.textSource.collectSelections();this.doNotTrackNewAbbr=!0;const s=await this.textSource.replaceAbbreviations(o.map(c=>c.change));if(this.doNotTrackNewAbbr=!1,s)this.moveSelections(n,o);else for(const c of t)this.trackedAbbreviations.add(c)}moveSelections(t,o){const n=this.textSource.selectionMoveMode();if(!(n.kind==="MoveAllSelections"||n.kind==="OnlyMoveCursorSelections"&&(o.some(i=>i.cursorOffset)||n.updateUnchangedSelections)))return;o.sort((i,b)=>i.change.range.offset-b.change.range.offset);const s=new Array;let c=0;for(const i of o){const b=i.change.newText,u=i.change.range,v=new M.Range(u.offset+c,b.length);s.push({rangeBeforeEdit:u,rangeAfterEdit:v,cursorOffset:i.cursorOffset}),c+=b.length-u.length}let f;switch(n.kind){case"OnlyMoveCursorSelections":f=this.textSource.collectSelections();break;case"MoveAllSelections":f=t.map(i=>{if(s.length===0)return i;if(i.offsetb.rangeBeforeEdit.offsetEnd)return new M.Range(b.rangeAfterEdit.offsetEnd+(i.offset-b.rangeBeforeEdit.offsetEnd),0);for(const u of s){if(i.offset>=u.rangeBeforeEdit.offset&&i.offset<=u.rangeBeforeEdit.offsetEnd)return new M.Range(u.rangeAfterEdit.offsetEnd+1,0);if(i.offset{for(const b of s){if(b.cursorOffset===void 0)continue;const u=i.offset===b.rangeAfterEdit.offsetEnd+1;if(u)return new M.Range(b.rangeAfterEdit.offset+b.cursorOffset,i.length)}return i});this.textSource.setSelections(m)}static computeReplacements(t){const o="$CURSOR",n=new Array;for(const s of t){const c=s.matchingSymbol;if(c){const f=c.replace(o,"");let m=c.indexOf(o);m===-1&&(m=void 0),n.push({change:{range:s.range,newText:f},cursorOffset:m})}}return n}processChange(t){let o=!1;for(const n of[...this.trackedAbbreviations]){const{isAffected:s,shouldStopTracking:c}=n.processChange(t.range,t.newText);s&&(o=!0),c&&this.trackedAbbreviations.delete(n)}if(t.newText===this.config.abbreviationCharacter&&!o&&!this.doNotTrackNewAbbr){const n=new q.TrackedAbbreviation(new M.Range(t.range.offset+1,0),"",this.abbreviationProvider);this.trackedAbbreviations.add(n)}}}e.AbbreviationRewriter=r}),h=d(function(a,e){var r=g&&g.__createBinding||(Object.create?function(t,o,n,s){s===void 0&&(s=n);var c=Object.getOwnPropertyDescriptor(o,n);(!c||("get"in c?!o.__esModule:c.writable||c.configurable))&&(c={enumerable:!0,get:function(){return o[n]}}),Object.defineProperty(t,s,c)}:function(t,o,n,s){s===void 0&&(s=n),t[s]=o[n]}),p=g&&g.__exportStar||function(t,o){for(var n in t)n!=="default"&&!Object.prototype.hasOwnProperty.call(o,n)&&r(o,t,n)};Object.defineProperty(e,"__esModule",{value:!0}),p(I,e),p(vk,e),p(wk,e),p(M,e),p(q,e)}),Ck=C(h),_k=h.AbbreviationProvider,Ik=h.AbbreviationRewriter,kk=h.Range,xk=h.TrackedAbbreviation;export default Ck;export{_k as AbbreviationProvider,Ik as AbbreviationRewriter,kk as Range,xk as TrackedAbbreviation,h as __moduleExports}; From 4afb127ac89a7044780967657a41d01399610e96 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 21 Jul 2025 14:18:42 +0200 Subject: [PATCH 02/15] chore: copyright headers --- src/verso-search/VersoSearch/DomainSearch.lean | 6 ++++++ src/verso-util/VersoUtil.lean | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/src/verso-search/VersoSearch/DomainSearch.lean b/src/verso-search/VersoSearch/DomainSearch.lean index dbcdcf565..e84371fac 100644 --- a/src/verso-search/VersoSearch/DomainSearch.lean +++ b/src/verso-search/VersoSearch/DomainSearch.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + import Std.Data.HashMap import VersoUtil.BinFiles diff --git a/src/verso-util/VersoUtil.lean b/src/verso-util/VersoUtil.lean index 9fd583fd0..8a019e945 100644 --- a/src/verso-util/VersoUtil.lean +++ b/src/verso-util/VersoUtil.lean @@ -1 +1,7 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + import VersoUtil.BinFiles From 23a3d99b63f602567df7ab1d38dd7fa5e703fe3d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 21 Jul 2025 14:23:58 +0200 Subject: [PATCH 03/15] chore: search component license info --- src/verso-manual/VersoManual.lean | 2 +- src/verso-manual/VersoManual/License.lean | 48 +++++++++++++++++++++++ 2 files changed, 49 insertions(+), 1 deletion(-) diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index 49a7e8726..7e05e1845 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -708,7 +708,7 @@ def Config.addSearch (config : Config) : Config := { config with extraJsFiles := config.extraJsFiles.push {filename := "elasticlunr.min.js", contents := elasticlunr.js}, - licenseInfo := Licenses.elasticlunr.js :: config.licenseInfo + licenseInfo := [Licenses.fuzzysort, Licenses.w3Combobox, Licenses.elasticlunr.js] ++ config.licenseInfo } diff --git a/src/verso-manual/VersoManual/License.lean b/src/verso-manual/VersoManual/License.lean index 98e15048e..10d18dedd 100644 --- a/src/verso-manual/VersoManual/License.lean +++ b/src/verso-manual/VersoManual/License.lean @@ -141,6 +141,54 @@ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. "# +def fuzzysort : LicenseInfo where + identifier := "MIT" + dependency := "fuzzysort v3.1.0" + howUsed := "The fuzzysort library is used in the search box to quickly filter results." + link := "https://github.com/farzher/fuzzysort" + text := #[(some "The MIT License", text)] +where + text := r#" +Copyright (c) 2018 Stephen Kamenar + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. +"# + +def w3Combobox : LicenseInfo where + identifier := "W3C-20150513" + dependency := "Editable Combobox With Both List and Inline Autocomplete Example, from the W3C's ARIA Authoring Practices Guide (APG)" + howUsed := "The search box component includes code derived from the example code in the linked article from the W3C's ARIA Authoring Practices Guide (APG)." + link := "https://www.w3.org/WAI/ARIA/apg/patterns/combobox/examples/combobox-autocomplete-both/" + text := #[(some "Software and Document License - 2023 Version", text)] +where + text := r#"Permission to copy, modify, and distribute this work, with or without +modification, for any purpose and without fee or royalty is hereby granted, +provided that you include the following on ALL copies of the work or portions +thereof, including modifications: + + * The full text of this NOTICE in a location viewable to users of the redistributed or derivative work. + + * Any pre-existing intellectual property disclaimers, notices, or terms and conditions. If none exist, the W3C software and document short notice should be included. + + * Notice of any changes or modifications, through a copyright statement on the new code or document such as "This software or document includes material copied from or derived from "Editable Combobox With Both List and Inline Autocomplete Example" at https://www.w3.org/WAI/ARIA/apg/patterns/combobox/examples/combobox-autocomplete-both/. Copyright © 2024 World Wide Web Consortium. https://www.w3.org/copyright/software-license-2023/" + +"# end Licenses From 050f8b8a0ff8cec61abf56f6295a65ce6c59021c Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 21 Jul 2025 15:55:36 +0200 Subject: [PATCH 04/15] chore: move CSS customizations to the domain mappers This gives better extensibility --- doc/UsersGuide/Basic.lean | 3 + doc/UsersGuide/Markup.lean | 33 ++++++++ lakefile.lean | 2 +- src/verso-manual/VersoManual.lean | 1 + src/verso-manual/VersoManual/Basic.lean | 92 ++++++++++++++++++++- src/verso-manual/VersoManual/Docstring.lean | 15 ++-- src/verso-manual/VersoManual/Glossary.lean | 13 ++- src/verso-manual/VersoManual/Html.lean | 1 + src/verso-search/VersoSearch.lean | 8 ++ static-web/search/search-box.css | 31 +------ 10 files changed, 155 insertions(+), 44 deletions(-) diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index a45f572ed..d31c8da0e 100644 --- a/doc/UsersGuide/Basic.lean +++ b/doc/UsersGuide/Basic.lean @@ -59,6 +59,7 @@ results in ## More Docstring Examples %%% +tag := "more-docstring-examples" shortTitle := "More Docstrings" %%% @@ -113,6 +114,7 @@ References to technical terms are valid both before and after their definition s # Index %%% +tag := "index" number := false %%% @@ -121,6 +123,7 @@ number := false # Dependencies %%% +tag := "dependencies" number := false %%% diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean index 149d530e5..ec5cbdcfe 100644 --- a/doc/UsersGuide/Markup.lean +++ b/doc/UsersGuide/Markup.lean @@ -57,6 +57,9 @@ tag := "lean-markup" Lean's documentation markup language is a close relative of Markdown, but it's not identical to it. # Design Principles +%%% +tag := "markup-design-principles" +%%% 1. Syntax errors - fail fast rather than producing unexpected output or having complicated rules 2. Reduce lookahead - parsing should succeed or fail as locally as possible @@ -66,6 +69,9 @@ Lean's documentation markup language is a close relative of Markdown, but it's n 6. Pandoc and Djot compatibility - when Markdown doesn't have a syntax for a feature, attempt to be compatible with Pandoc Markdown or Djot # Syntax +%%% +tag := "markup-syntax" +%%% Like Markdown, Lean's markup has three primary syntactic categories: @@ -82,8 +88,14 @@ Like Markdown, Lean's markup has three primary syntactic categories: Headers, footnote definitions, and named links give greater structure to a document. They may not be nested inside of blocks. ## Description +%%% +tag := "markup-syntax-description" +%%% ### Inline Syntax +%%% +tag := "inline-syntax" +%%% Emphasis is written with underscores: ```markupPreview @@ -118,14 +130,26 @@ The definition of `main` TeX math can be included using a single or double dollar sign followed by code. Two dollar signs results in display-mode math, so `` $`\sum_{i=0}^{10} i` `` results in $`\sum_{i=0}^{10} i` while `` $$`\sum_{i=0}^{10} i` `` results in: $$`\sum_{i=0}^{10} i` ### Block Syntax +%%% +tag := "block-syntax" +%%% ### Document Structure +%%% +tag := "document-structure" +%%% ## Differences from Markdown +%%% +tag := "differences-from-markdown" +%%% This is a quick "cheat sheet" for those who are used to Markdown, documenting the differences. ### Syntax Errors +%%% +tag := "syntax-errors" +%%% While Markdown includes a set of precedence rules to govern the meaning of mismatched delimiters (such as in `what _is *bold_ or emph*?`), these are syntax errors in Lean's markup. Similarly, Markdown specifies that unmatched delimiters (such as `*` or `_`) should be included as characters, while Lean's markup requires explicit escaping of delimiters. @@ -133,17 +157,26 @@ Similarly, Markdown specifies that unmatched delimiters (such as `*` or `_`) sho This is based on the principle that, for long-form technical writing, it's better to catch typos while writing than while reviewing the text later. ### Reduced Lookahead +%%% +tag := "reduced-lookahead" +%%% In Markdown, whether `[this][here]` is a link depends on whether `here` is defined as a link reference target somewhere in the document. In Lean's markup, it is always a link, and it is an error if `here` is not defined as a link target. ### Header Nesting +%%% +tag := "header-nesting" +%%% In Lean's markup, every document already has a title, so there's no need to use the highest level header (`#`) to specify one. Additionally, all documents are required to use `#` for their top-level header, `##` for the next level, and so forth, because a single file may represent a section, a chapter, or even a whole book. Authors should not need to maintain a global mapping from header levels to document structures, so Lean's markup automatically assigns these based on the structure of the document. ### Genre-Specific Extensions +%%% +tag := "genre-specific-extensions" +%%% Markdown has no standard way for specific tools or styles of writing to express domain- or {ref "genres"}[genre]-specific concepts. Lean's markup provides standard syntaxes to use for this purpose, enabling compositional extensions. diff --git a/lakefile.lean b/lakefile.lean index 7ea1af13c..19c92d544 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,7 +12,6 @@ lean_lib VersoUtil where srcDir := "src/verso-util" roots := #[`VersoUtil] - @[default_target] lean_lib Verso where srcDir := "src/verso" @@ -57,6 +56,7 @@ lean_exe «verso-demo» where lean_lib UsersGuide where srcDir := "doc" + leanOptions := #[⟨`weak.linter.verso.manual.headerTags, true⟩] @[default_target] lean_exe usersguide where diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index 7e05e1845..4cbc8a8ff 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -475,6 +475,7 @@ def emitSearchBox (dir : System.FilePath) (domains : DomainMappers) : IO Unit := for (file, contents) in searchBoxCode do IO.FS.writeBinFile (dir / file) contents IO.FS.writeFile (dir / "domain-mappers.js") (domains.toJs.pretty (width := 70)) + IO.FS.writeFile (dir / "domain-display.css") domains.quickJumpCss end diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean index dbd9bfc83..0e7dc1ced 100644 --- a/src/verso-manual/VersoManual/Basic.lean +++ b/src/verso-manual/VersoManual/Basic.lean @@ -37,6 +37,91 @@ inductive Output where html (depth : Nat) deriving DecidableEq, BEq, Hashable +/-- +The font families used when rendering documents. + +These font families are specified using CSS variables, so they can be overridden. +-/ +inductive FontFamily where + | /-- + The font used for ordinary text, customized with the `--verso-text-font-family` CSS variable. + -/ + text + | /-- + The font used for “structural” text, such as headers. Customized with the `--verso-structure-font-family` CSS variable. + -/ + structure + | /-- + The font used for monospace code, customized with the `--verso-code-font-family` CSS variable. + -/ + code +deriving DecidableEq, Repr, Hashable + +namespace FontFamily +/-- +The CSS variable that is used to style this font. +-/ +def toCssVar : FontFamily → String + | .text => "--verso-text-font-family" + | .structure => "--verso-structure-font-family" + | .code => "--verso-code-font-family" + +/-- +Returns CSS code that styles text using the font family. +-/ +def toCss (family : FontFamily) : String := s!"font-family: var({family.toCssVar});" + +end FontFamily + +inductive FontStyle where + | normal + | italic +deriving DecidableEq, Repr, Hashable + +def FontStyle.toCss (s : FontStyle) : String := + "font-style: " ++ + match s with + | .normal => "normal;" + | .italic => "italic;" + +inductive FontWeight where + | lighter + | light + | normal + | bold + | bolder + | numeric (weight : Nat) (ok : weight > 0 ∧ weight < 1000 := by omega) +deriving DecidableEq, Repr, Hashable + +def FontWeight.toCss (w : FontWeight) : String := + "font-weight: " ++ + match w with + | .lighter => "lighter;" + | .light => "light;" + | .normal => "normal;" + | .bold => "bold;" + | .bolder => "bolder;" + | .numeric n _ => s!"{n};" + +/-- A specification of a font. -/ +structure Font where + family : FontFamily := .text + style : FontStyle := .normal + weight : FontWeight := .normal +deriving DecidableEq, Repr, Hashable + +/-- CSS code for a font. -/ +def Font.toCss (font : Font) : String := + " " ++ font.family.toCss ++ "\n" ++ + " " ++ font.style.toCss ++ "\n" ++ + " " ++ font.weight.toCss ++ "\n" + +open Verso.Search in +defmethod DomainMapper.setFont (mapper : DomainMapper) (font : Font) : DomainMapper := + { mapper with + quickJumpCss := + s!"#search-wrapper .{mapper.className} " ++ "{\n" ++ font.toCss ++ "}\n" + } /-- Tags are used to refer to parts through tables of contents, cross-references, and the like. @@ -771,9 +856,9 @@ def sectionString (ctxt : TraverseContext) : Option String := def sectionDomain := `Verso.Genre.Manual.section open Verso.Search in -def sectionDomainMapper : DomainMapper where - displayName := "Section" - className := "section-domain" +def sectionDomainMapper : DomainMapper := { + displayName := "Section", + className := "section-domain", dataToSearchables := "(domainData) => Object.entries(domainData.contents).map(([key, value]) => ({ @@ -782,6 +867,7 @@ def sectionDomainMapper : DomainMapper where domainId: 'Verso.Genre.Manual.section', ref: value, }))" + : DomainMapper }.setFont { family := .structure, weight := .bold } instance : TraversePart Manual where inPart p := (·.inPart p) diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 2cd965447..2effe3c97 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -774,7 +774,8 @@ def Signature.toHtml : Signature → HighlightHtmlM Html return {{
    {{← wide.toHtml}}
    {{← narrow.toHtml}}
    }} open Verso.Search in -def docDomainMapper : DomainMapper := .withDefaultJs docstringDomain "Documentation" "doc-domain" +def docDomainMapper : DomainMapper := + DomainMapper.withDefaultJs docstringDomain "Documentation" "doc-domain" |>.setFont { family := .code } open Verso.Genre.Manual.Markdown in @[block_extension Block.docstring] @@ -1583,7 +1584,7 @@ def optionDocs : BlockRoleExpander open Verso.Search in def optionDomainMapper : DomainMapper := - .withDefaultJs optionDomain "Compiler Option" "doc-option-domain" + DomainMapper.withDefaultJs optionDomain "Compiler Option" "doc-option-domain" |>.setFont { family := .code } open Verso.Genre.Manual.Markdown in @[block_extension optionDocs] @@ -1705,7 +1706,7 @@ def Inline.tactic : Inline where open Verso.Search in -def tacticDomainMapper : DomainMapper where +def tacticDomainMapper : DomainMapper := { className := "tactic-domain" displayName := "Tactic" dataToSearchables := @@ -1716,6 +1717,7 @@ def tacticDomainMapper : DomainMapper where domainId: 'Verso.Genre.Manual.doc.tactic', ref: value, }))" + : DomainMapper }.setFont { family := .code, weight := .bold} open Verso.Genre.Manual.Markdown in open Lean Elab Term Parser Tactic Doc in @@ -1853,9 +1855,9 @@ def conv : DirectiveExpander pure #[← ``(Verso.Doc.Block.other (Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?)) #[$(contents ++ userContents),*])] open Verso.Search in -def convDomainMapper : DomainMapper where - className := "conv-tactic-domain" - displayName := "Conv Tactic" +def convDomainMapper : DomainMapper := { + className := "conv-tactic-domain", + displayName := "Conv Tactic", dataToSearchables := "(domainData) => Object.entries(domainData.contents).map(([key, value]) => ({ @@ -1864,6 +1866,7 @@ def convDomainMapper : DomainMapper where domainId: 'Verso.Genre.Manual.doc.tactic.conv', ref: value, }))" + : DomainMapper }.setFont { family := .code, weight := .bold } open Verso.Genre.Manual.Markdown in open Lean Elab Term Parser Tactic Doc in diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean index 7bddf5fc9..7a28d0151 100644 --- a/src/verso-manual/VersoManual/Glossary.lean +++ b/src/verso-manual/VersoManual/Glossary.lean @@ -96,9 +96,9 @@ def Glossary.addEntry [Monad m] [MonadState TraverseState m] [MonadLiftT IO m] [ modify (TraverseState.set · glossaryState <| v.setObjVal! key (ToJson.toJson id)) open Verso.Search in -def technicalTermDomainMapper : DomainMapper where - displayName := "Terminology" - className := "tech-term-domain" +def technicalTermDomainMapper : DomainMapper := { + displayName := "Terminology", + className := "tech-term-domain", dataToSearchables := "(domainData) => Object.entries(domainData.contents).map(([key, value]) => ({ @@ -107,6 +107,7 @@ def technicalTermDomainMapper : DomainMapper where domainId: 'Verso.Genre.Manual.doc.tech', ref: value, }))" + : DomainMapper }.setFont { family := .text } @[inline_extension deftech] def deftech.descr : InlineDescr where @@ -230,6 +231,10 @@ a.technical-term { a.technical-term:hover { text-decoration: currentcolor underline solid; } - +/* Highlight the clicked term */ +.def-technical-term:target { + background-color: var(--verso-selected-color); + outline: auto; +} "# ] diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index 7017a653f..c58d8f758 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -541,6 +541,7 @@ def page + {{extraJsFiles.map fun f => ({{}})}} {{extraStylesheets.map (fun url => {{ }})}} {{extraCss.toArray.map ({{}})}} diff --git a/src/verso-search/VersoSearch.lean b/src/verso-search/VersoSearch.lean index 06e59ee43..68325f093 100644 --- a/src/verso-search/VersoSearch.lean +++ b/src/verso-search/VersoSearch.lean @@ -127,6 +127,14 @@ def addDoc (self : DocumentStore) (ref : String) (doc : Doc) : DocumentStore := length := if self.hasDoc ref then self.length else self.length + 1, docs := self.docs.insert ref <| if self.save then doc else {} } +/-- +Removes the documents from the store, setting `save` to `false`. +-/ +def extractDocs (self : DocumentStore) : DocumentStore × TreeMap String Doc := + let docs := self.docs + let noDocs := docs.map (fun _ _ => {}) + ({ self with docs := noDocs, save := false }, docs) + /-- Gets a document if it is present in the store. -/ diff --git a/static-web/search/search-box.css b/static-web/search/search-box.css index 1a66ab3f0..0c4d20478 100644 --- a/static-web/search/search-box.css +++ b/static-web/search/search-box.css @@ -1,5 +1,5 @@ /** - * Copyright (c) 2024 Lean FRO LLC. All rights reserved. + * Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. * Released under Apache 2.0 license as described in the file LICENSE. * Author: Jakob Ambeck Vase */ @@ -111,20 +111,6 @@ } } -#search-wrapper .search-result.doc-domain, -#search-wrapper .search-result.option-domain, -#search-wrapper .search-result.syntax-domain, -#search-wrapper .search-result.lake-option-domain, -#search-wrapper .search-result.lake-toml-table-domain, -#search-wrapper .search-result.lake-toml-field-domain, -#search-wrapper .search-result.elan-option-domain, -#search-wrapper .search-result.env-var-domain, -#search-wrapper .search-result.lake-command-domain, -#search-wrapper .search-result.error-explanation-domain, -#search-wrapper .search-result.elan-command-domain { - font-family: var(--verso-code-font-family); -} - #search-wrapper .search-result.full-text { font-family: var(--verso-text-font-family); } @@ -138,21 +124,6 @@ font-weight: bold; } -#search-wrapper .search-result.tactic-domain, -#search-wrapper .search-result.conv-tactic-domain { - font-family: var(--verso-code-font-family); - font-weight: bold; -} - -#search-wrapper .search-result.tech-term-domain { - font-family: var(--verso-text-font-family); -} - -#search-wrapper .search-result.section-domain { - font-family: var(--verso-structure-font-family); - font-weight: bold; -} - #search-wrapper [role="listbox"].focus li[aria-selected="true"], #search-wrapper .search-result:hover { background-color: var(--selected-color); From 449711dd47ec3aca04d265426e0076c491e48432 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 22 Jul 2025 09:19:38 +0200 Subject: [PATCH 05/15] feat: split document store into lazily-loaded buckets This is to make it so the search will work without downloading a 20MB blob on the language reference. --- lakefile.lean | 5 ++ src/verso-manual/VersoManual.lean | 61 ++++++++++---- src/verso-manual/VersoManual/Html.lean | 2 + src/verso-search/VersoSearch.lean | 15 +++- static-web/search/search-box.js | 109 ++++++++++++++++++++----- 5 files changed, 155 insertions(+), 37 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 19c92d544..5a45b574b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -22,9 +22,14 @@ lean_lib MultiVerso where srcDir := "src/multi-verso" roots := #[`MultiVerso] +input_dir searchJs where + path := "static-web/search" + @[default_target] lean_lib VersoSearch where srcDir := "src/verso-search" + -- Rebuild search when JS on disk changes + needs := #[searchJs] @[default_target] lean_lib VersoBlog where diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index 4cbc8a8ff..33004d541 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -41,6 +41,8 @@ import VersoManual.Table open Lean (Name NameMap Json ToJson FromJson quote) +open Std (HashMap) + open Verso.FS open Verso.Doc Elab @@ -441,7 +443,7 @@ def emitXrefs (toc : List Html.Toc) (dir : System.FilePath) (state : TraverseSta section open Search -def addSearchIndex (state : TraverseState) (ctx : TraverseContext) (logError : String → IO Unit) (doc : Part Manual) : IO TraverseState := do +def emitSearchIndex (dir : System.FilePath) (state : TraverseState) (ctx : TraverseContext) (logError : String → IO Unit) (doc : Part Manual) : IO Unit := do have : Indexable Manual := { partHeader p := do let ctxt ← IndexM.traverseContext @@ -463,12 +465,39 @@ def addSearchIndex (state : TraverseState) (ctx : TraverseContext) (logError : S } match Verso.Search.mkIndex doc ctx with - | .error e => logError e; return state + | .error e => logError e; return () | .ok index => + -- Split the index into roughly 150k chunks for faster loading + let (index, docs) := index.extractDocs + let size := docs.foldl (init := 0) (fun s _ v => s + v.size) + let mut docBuckets : HashMap UInt8 (HashMap String Doc) := {} + for (ref, content) in docs do + let h := bucket ref + docBuckets := docBuckets.alter h fun v => + v.getD {} |>.insert ref content + + for (bucket, docs) in docBuckets do + let docJson := docs.fold (init := Json.mkObj []) fun json k v => json.setObjVal! k (v.foldr (init := Json.mkObj []) fun k v js => js.setObjVal! k (Json.str v)) + IO.FS.writeFile (dir / s!"searchIndex_{bucket}.js") s!"window.docContents[{bucket}].resolve({docJson.compress});" + let indexJs := "const __verso_searchIndexData = " ++ index.toJson.compress ++ ";\n\n" let indexJs := indexJs ++ "const __versoSearchIndex = elasticlunr ? elasticlunr.Index.load(__verso_searchIndexData) : null;\n" + let indexJs := indexJs ++ "window.docContents = {};\n" let indexJs := indexJs ++ "window.searchIndex = elasticlunr ? __versoSearchIndex : null;\n" - return { state with extraJsFiles := state.extraJsFiles.push { filename := "searchIndex.js", contents := indexJs } } + IO.FS.writeFile (dir / "searchIndex.js") indexJs + + IO.FS.writeFile (dir / "elasticlunr.min.js") Verso.Output.Html.elasticlunr.js + +where + -- Not using a proper hash because this needs to be implemented identically in JS + bucket (s : String) : UInt8 := Id.run do + let mut hash := 0 + let mut n := 0 + while h : n < s.utf8ByteSize do + hash := hash + s.getUtf8Byte n h + n := n + 1 + return hash + def emitSearchBox (dir : System.FilePath) (domains : DomainMappers) : IO Unit := do ensureDir dir @@ -494,14 +523,14 @@ def emitHtmlSingle (text : Part Manual) : ReaderT ExtensionImpls IO (Part Manual × TraverseState) := do let dir := config.destination.join "html-single" ensureDir dir - let (traverseOut, st) ← emitContent dir .empty - IO.FS.writeFile (dir.join "-verso-docs.json") (toString st.dedup.docJson) - emitSearchBox (dir / "-verso-search") traverseOut.2.quickJump - pure traverseOut + let ((text, state), htmlState) ← emitContent dir .empty + IO.FS.writeFile (dir.join "-verso-docs.json") (toString htmlState.dedup.docJson) + emitSearchBox (dir / "-verso-search") state.quickJump + emitSearchIndex (dir / "-verso-search") state {logError, draft := config.draft} logError text + pure (text, state) where emitContent (dir : System.FilePath) : StateT (State Html) (ReaderT ExtensionImpls IO) (Part Manual × TraverseState) := do let (text, state) ← traverse logError text {config with htmlDepth := 0} - let state ← addSearchIndex state {logError, draft := config.draft} logError text let authors := text.metadata.map (·.authors) |>.getD [] let authorshipNote := text.metadata.bind (·.authorshipNote) let _date := text.metadata.bind (·.date) |>.getD "" -- TODO @@ -572,10 +601,11 @@ def emitHtmlMulti (logError : String → IO Unit) (config : Config) (text : Part Manual) : ReaderT ExtensionImpls IO (Part Manual × TraverseState) := do let root := config.destination.join "html-multi" ensureDir root - let (traverseOut, st) ← emitContent root {} - IO.FS.writeFile (root.join "-verso-docs.json") (toString st.dedup.docJson) - emitSearchBox (root / "-verso-search") traverseOut.2.quickJump - pure traverseOut + let ((text, state), htmlState) ← emitContent root {} + IO.FS.writeFile (root.join "-verso-docs.json") (toString htmlState.dedup.docJson) + emitSearchBox (root / "-verso-search") state.quickJump + emitSearchIndex (root / "-verso-search") state {logError, draft := config.draft} logError text + pure (text, state) where /-- Emits the data used by all pages in the site, such as JS and CSS, and then emits the root page @@ -583,7 +613,6 @@ where -/ emitContent (root : System.FilePath) : StateT (State Html) (ReaderT ExtensionImpls IO) (Part Manual × TraverseState) := do let (text, state) ← traverse logError text config - let state ← addSearchIndex state {logError, draft := config.draft} logError text let authors := text.metadata.map (·.authors) |>.getD [] let authorshipNote := text.metadata >>= (·.authorshipNote) let _date := text.metadata.bind (·.date) |>.getD "" -- TODO @@ -701,14 +730,12 @@ def Config.addKaTeX (config : Config) : Config := licenseInfo := Licenses.KaTeX :: config.licenseInfo } -open Verso.Output.Html in + /-- -Adds a bundled version of elasticlunr.js to the config. +Adds search dependencies to the configuration -/ def Config.addSearch (config : Config) : Config := { config with - extraJsFiles := - config.extraJsFiles.push {filename := "elasticlunr.min.js", contents := elasticlunr.js}, licenseInfo := [Licenses.fuzzysort, Licenses.w3Combobox, Licenses.elasticlunr.js] ++ config.licenseInfo } diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index c58d8f758..42198652e 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -537,7 +537,9 @@ def page + + diff --git a/src/verso-search/VersoSearch.lean b/src/verso-search/VersoSearch.lean index 68325f093..d3d8e54a7 100644 --- a/src/verso-search/VersoSearch.lean +++ b/src/verso-search/VersoSearch.lean @@ -87,6 +87,12 @@ structure Options where /-- A document is a map from field names to field values. -/ abbrev Doc := TreeMap String String +/-- +The number of characters in the document. +-/ +def Doc.size (doc : Doc) : Nat := + doc.foldl (init := 0) fun s k v => s + k.length + v.length + /-- A collection of indexed documents, represented so as to be compatible with elasticlunr.js. -/ @@ -582,6 +588,13 @@ def addDoc (self : Index) (ref : String) (data : Array String) : Index := Id.run } { self with documentStore := self.documentStore.addDoc ref doc } +/-- +Removes the documents from the index's store, setting `save` to `false`. +-/ +def extractDocs (self : Index) : Index × TreeMap String Doc := + let (store, docs) := self.documentStore.extractDocs + ({ self with documentStore := store }, docs) + /-- Converts the context of an index into JSON. -/ @@ -772,7 +785,7 @@ code to construct the index. Primarily useful for testing. -/ def mkIndexDocs (p : Part g) (ctx : g.TraverseContext) : Except String (Array IndexDoc) := do if p.metadata.bind idx.partId |>.isNone then - throw "No ID for root part" + throw "mkIndexDocs: No ID for root part" else match partText p (#[], ctx) {} with | .error e _ => throw e diff --git a/static-web/search/search-box.js b/static-web/search/search-box.js index 59cdd9c4c..a8b470f65 100644 --- a/static-web/search/search-box.js +++ b/static-web/search/search-box.js @@ -22,6 +22,14 @@ const searchIndex = /** @type {{searchIndex: TextSearchIndex}} */ ( /** @type {unknown} */ (window) ).searchIndex; +/** + * @typedef {{id: string, header: string, context: string, contents: string}} DocContent + * @typedef {Promise> & {resolve?: (data : any) => void}} DocContentPromise + */ +/** + * @type {Record} + */ +const docContents = ((/** @type {any} */ (window)).docContents) || ((/** @type {any} */ (window)).docContents = {}); /** Whether to search word prefixes or whole words in full-text searches. Should match the setting in search-highlight.js. * @type {boolean} @@ -37,7 +45,7 @@ const expandMatches = true; * @typedef {(searchable: Searchable, matchedParts: MatchedPart[], document: Document) => HTMLElement} CustomResultRender * @typedef {{dataToSearchables: DomainDataToSearchables, customRender?: CustomResultRender, displayName: string, className: string}} DomainMapper * @typedef {Record} DomainMappers - * @typedef {{ref: string, score: number, doc: {id: string, header: string, context: string, contents: string}}} TextMatch + * @typedef {{ref: string, score: number, doc: DocContent}} TextMatch * @typedef {{item: Searchable, fuzzysortResult: Fuzzysort.Result, htmlItem: HTMLLIElement}|{terms: string, textItem: TextMatch, htmlItem: HTMLLIElement}} SearchResult * @typedef {{run: (tokens: string[]) => string[]}} ElasticLunrPipeline * @typedef {{bool?: "AND"|"OR", fields?:Record, expand?: boolean}} SearchConfig @@ -283,18 +291,71 @@ const searchableToHtml = ( return li; }; +/** + * Gets the sort bucket for a given document ID. + * @param {string} ref + * @return {number} + */ +const docBucket = ref => { + const utf8 = new TextEncoder().encode(ref); + let hash = 0; + for (let i = 0; i < utf8.length; i++) { + hash = (hash + utf8[i]) % 256; + } + return hash; +}; + +/** + * Loads the needed document bucket as a promise. + * @param {string} ref + * @return {Promise>} + */ +const loadBucket = async (ref) => { + const bucket = docBucket(ref); + let bucketDocs = docContents[bucket]; + if (bucketDocs) { + return bucketDocs; + } + + /** @type {(data : any) => void} */ + let resolveFun; + const promise = new Promise((resolve) => { + resolveFun = resolve; + }); + (/** @type {any} */ (promise)).resolve = resolveFun; + docContents[bucket] = promise; + const script = document.createElement('script'); + script.src = `-verso-search/searchIndex_${bucket}.js` + document.head.appendChild(script); + + return await docContents[bucket]; +} + +/** + * @param {string} ref The identifier of the document to fetch from the store + * @return {Promise} + */ +const getDocContents = async (ref) => { + const resultBucket = await Promise.resolve(loadBucket(ref)); + + /** @type {DocContent} */ + return resultBucket[ref]; +} + /** * Maps from a data item to a HTML LI element * @param {string} term * @param {TextMatch} match * @param {Document} document - * @return {HTMLLIElement|null} + * @return {Promise} */ -const textResultToHtml = ( +const textResultToHtml = async ( term, match, document ) => { + const doc = await getDocContents(match.ref); + const li = document.createElement("li"); li.role = "option"; li.className = `search-result full-text`; @@ -304,15 +365,15 @@ const textResultToHtml = ( const searchTerm = document.createElement("p"); let inHeader = true; - let headerHl = highlightTextResult(match.doc.header, term, {contextLength: 30}); // Only abbreviate huge headers + let headerHl = highlightTextResult(doc.header, term, {contextLength: 30}); // Only abbreviate huge headers if (!headerHl) { inHeader = false; headerHl = document.createElement("span"); - headerHl.append(document.createTextNode(match.doc.header)); + headerHl.append(document.createTextNode(doc.header)); } headerHl.className = "header"; searchTerm.append(headerHl); - let contentHl = highlightTextResult(match.doc.contents, term, {contextLength: 10}); + let contentHl = highlightTextResult(doc.contents, term, {contextLength: 10}); if (!contentHl) { if (!inHeader) { // Exclude this result. It'd be cleaner to do this elsewhere, but duplicating the string @@ -334,11 +395,11 @@ const textResultToHtml = ( const domainName = document.createElement("p"); li.appendChild(domainName); domainName.className = "domain"; - if (match.doc.context.trim() == "") { + if (doc.context.trim() == "") { domainName.textContent = "Full-text search"; } else { // This is a slight abuse of "domain", but it seems to work well - let context = match.doc.context.replaceAll("\t", " » "); + let context = doc.context.replaceAll("\t", " » "); domainName.append(document.createTextNode(context)); domainName.classList.add('text-context'); } @@ -636,7 +697,7 @@ class SearchBox { // ComboboxAutocomplete Events - filterOptions() { + async filterOptions() { const currentOptionText = opt(this.currentOption, resultToText); const filter = this.filter; @@ -742,7 +803,7 @@ class SearchBox { } } } else { - const option = textResultToHtml(filter, result, document); + const option = await textResultToHtml(filter, result, document); if (option) { /** @type {SearchResult} */ const searchResult = { @@ -880,7 +941,7 @@ class SearchBox { * @param {KeyboardEvent} event * @returns void */ - onComboboxKeyDown(event) { + async onComboboxKeyDown(event) { let eventHandled = false; const altKey = event.altKey; @@ -896,7 +957,12 @@ class SearchBox { if("fuzzysortResult" in this.currentOption) { this.confirmResult(this.currentOption.item.address); } else { - this.confirmResult(this.currentOption.textItem.doc.id, this.currentOption.terms); + const resultBucket = await Promise.resolve(loadBucket(this.currentOption.textItem.ref)); + + /** @type {DocContent} */ + const doc = resultBucket[this.currentOption.textItem.ref]; + + this.confirmResult(doc.id, this.currentOption.terms); } } } @@ -955,7 +1021,7 @@ class SearchBox { if (this.isOpen()) { this.close(true); this.filter = this.comboboxNode.textContent; - this.filterOptions(); + await this.filterOptions(); this.setVisualFocusCombobox(); } else { this.setValue(""); @@ -993,7 +1059,7 @@ class SearchBox { * @param {KeyboardEvent} event * @returns void */ - onComboboxKeyUp(event) { + async onComboboxKeyUp(event) { let eventHandled = false; if (event.key === "Escape" || event.key === "Esc") { @@ -1018,7 +1084,7 @@ class SearchBox { this.setVisualFocusCombobox(); this.setCurrentOptionStyle(null); eventHandled = true; - const option = this.filterOptions(); + const option = await this.filterOptions(); if (option) { if (this.isClosed() && this.comboboxNode.textContent.length) { this.open(); @@ -1049,9 +1115,9 @@ class SearchBox { } } - onComboboxFocus() { + async onComboboxFocus() { this.filter = this.comboboxNode.textContent; - this.filterOptions(); + await this.filterOptions(); this.setVisualFocusCombobox(); this.setCurrentOptionStyle(null); } @@ -1114,12 +1180,17 @@ class SearchBox { /** * @returns void */ - return () => { + return async () => { this.comboboxNode.textContent = resultToText(result); if ("fuzzysortResult" in result) { this.confirmResult(result.item.address); } else { - this.confirmResult(result.textItem.doc.id, resultToText(result)); + const resultBucket = await Promise.resolve(loadBucket(result.textItem.ref)); + + /** @type {DocContent} */ + const doc = resultBucket[result.textItem.ref]; + + this.confirmResult(doc.id, resultToText(result)); } this.close(true); }; From 1be07be4cf8d83d86b52bc0c29a5592afee0f0c8 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 22 Jul 2025 16:01:12 +0200 Subject: [PATCH 06/15] fix: make example definitions work correctly in quickjump This is needed to make the search not be broken for FPiL --- src/verso-manual/VersoManual/Basic.lean | 5 +- .../VersoManual/ExternalLean.lean | 123 +++++++++++++++++- src/verso/Verso/Code/External.lean | 24 ++-- src/verso/Verso/Code/Highlighted.lean | 21 +-- 4 files changed, 148 insertions(+), 25 deletions(-) diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean index 0e7dc1ced..6e3b69538 100644 --- a/src/verso-manual/VersoManual/Basic.lean +++ b/src/verso-manual/VersoManual/Basic.lean @@ -783,6 +783,8 @@ def doc.syntaxKind : Domain := {} def doc.option : Domain := {} def doc.tactic.conv : Domain := {} + +/-- Names defined as examples -/ -- Protected to avoid taking up good namespace protected def «example» : Domain := {} @@ -813,7 +815,8 @@ def TraverseState.linksFromDomain def TraverseState.localTargets (state : TraverseState) : Code.LinkTargets where const := fun x => state.linksFromDomain docstringDomain x.toString "doc" s!"Documentation for {x}" ++ - state.linksFromDomain exampleDomain x.toString "def" s!"Definition of example {x}" + -- There's no `x` in the tooltip on the next line to avoid revealing suppressed namespaces + state.linksFromDomain exampleDomain x.toString "def" s!"Definition of example" option := fun x => state.linksFromDomain optionDomain x.toString "doc" s!"Documentation for option {x}" keyword := fun k => diff --git a/src/verso-manual/VersoManual/ExternalLean.lean b/src/verso-manual/VersoManual/ExternalLean.lean index 0f7cf79ad..70a6217cb 100644 --- a/src/verso-manual/VersoManual/ExternalLean.lean +++ b/src/verso-manual/VersoManual/ExternalLean.lean @@ -27,11 +27,93 @@ namespace Verso.Genre.Manual private def hlJsDeps : List JsFile := [{filename := "popper.js", contents := popper}, {filename := "tippy.js", contents := tippy}] +open Verso.Search in +/-- +Quick jump configuration for definitions in examples +-/ +def exampleDomainMapper : DomainMapper := { + displayName := "Example Definition", + className := "example-def", + -- This is a bit of a hack. Examples with repeated names should really get differing canonical + -- names, but it's unclear what to use for them. Perhaps it should be the concatenated tags of the + -- containing sections, with a sequence number in case of further duplication? For now, this + -- fairly complicated mapper does the job. It'd also be good to have a way to show metadata in the + -- quick-jump box, with different styling. + dataToSearchables := + "(domainData) => { + const byName = Object.entries(domainData.contents).flatMap(([key, value]) => + value.map(v => ({ + context: v.data[`${v.address}#${v.id}`].context, + name: v.data[`${v.address}#${v.id}`].display, + address: `${v.address}#${v.id}` + }))).reduce((acc, obj) => { + const key = obj.name; + acc[key] = acc[key] || []; + acc[key].push(obj); + return acc; + }, {}) + return Object.entries(byName).flatMap(([key, value]) => { + if (value.length === 0) { return []; } + const firstCtxt = value[0].context; + let prefixLength = 0; + for (let i = 0; i < firstCtxt.length; i++) { + if (value.every(v => i < v.context.length && v.context[i] === firstCtxt[i])) { + prefixLength++; + } else break; + } + return value.map((v) => ({ + searchKey: v.context.slice(prefixLength).concat(v.name).join(' › '), + address: v.address, + domainId: 'Verso.Genre.Manual.example', + ref: value + })); + }); +}" + : DomainMapper} + +/-- +Extracts all names that are marked as definition sites, with both their occurrence in the source and +the underlying name. +-/ +private partial def definedNames : Highlighted → Array (Name × String) + | .token ⟨.const n _ _ true, s⟩ => #[(n, s)] + | .token _ => #[] + | .span _ hl | .tactics _ _ _ hl => definedNames hl + | .seq hls => hls.map definedNames |>.foldl (· ++ ·) #[] + | .text .. | .point .. | .unparsed .. => #[] + block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) where + init st := + st.addQuickJumpMapper exampleDomain exampleDomainMapper data := - let defined := hls.definedNames.toArray + let defined := definedNames hls Json.arr #[ToJson.toJson cfg, ToJson.toJson hls, ToJson.toJson defined] - traverse _ _ _ := pure none + traverse id data _ := do + let .arr #[cfgJson, _hlJson, definesJson] := data + | logError s!"Expected array for Lean block, got {data.compress}"; return none + match FromJson.fromJson? cfgJson with + | .error err => + logError <| "Failed to deserialize code config during traversal:" ++ err + return none + | .ok (cfg : CodeConfig) => + if cfg.defSite.isEqSome false then return none + match FromJson.fromJson? definesJson with + | .error err => + logError <| "Failed to deserialize code config during traversal:" ++ err + return none + | .ok (defines : Array (Name × String)) => + for (d, s) in defines do + if d.isAnonymous then continue + let d := d.toString + let path ← (·.path) <$> read + let _ ← externalTag id path d + let context := (← read).headers.map (·.titleString) + modify (·.saveDomainObject exampleDomain d id) + if let some link := (← get).externalTags[id]? then + modify (·.modifyDomainObjectData exampleDomain d fun v => + let v := if let .obj _ := v then v else .obj {} + v.setObjVal! link.link (json%{"context": $context, "display": $s})) + pure none toTeX := none extraCss := [highlightingStyle] extraJs := [highlightingJs] @@ -40,7 +122,7 @@ block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) where toHtml := open Verso.Output.Html in some <| fun _ _ _ data _ => do - let .arr #[cfgJson, hlJson, _] := data + let .arr #[cfgJson, hlJson, _definesJson] := data | HtmlT.logError "Expected four-element JSON for Lean code" pure .empty match FromJson.fromJson? hlJson with @@ -55,14 +137,39 @@ block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) where | .ok (cfg : CodeConfig) => let i := hl.indentation let hl := hl.deIndent i - withReader (fun ρ => { ρ with codeOptions.inlineProofStates := cfg.showProofStates }) <| + withReader ({ · with codeOptions.inlineProofStates := cfg.showProofStates, codeOptions.definitionsAsTargets := cfg.defSite.getD true }) <| hl.blockHtml "examples" inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) where data := - let defined := hls.definedNames.toArray + let defined := definedNames hls Json.arr #[ToJson.toJson cfg, ToJson.toJson hls, ToJson.toJson defined] - traverse _ _ _ := pure none + traverse id data _ := do + let .arr #[cfgJson, _hlJson, definesJson] := data + | logError s!"Expected array for Lean block, got {data.compress}"; return none + match FromJson.fromJson? cfgJson with + | .error err => + logError <| "Failed to deserialize code config during traversal:" ++ err + return none + | .ok (cfg : CodeConfig) => + unless cfg.defSite.isEqSome true do return none + match FromJson.fromJson? definesJson with + | .error err => + logError <| "Failed to deserialize code config during traversal:" ++ err + return none + | .ok (defines : Array (Name × String)) => + for (d, s) in defines do + if d.isAnonymous then continue + let d := d.toString + let path ← (·.path) <$> read + let _ ← externalTag id path d + let context := (← read).headers.map (·.titleString) + modify (·.saveDomainObject exampleDomain d id) + if let some link := (← get).externalTags[id]? then + modify (·.modifyDomainObjectData exampleDomain d fun v => + let v := if let .obj _ := v then v else .obj {} + v.setObjVal! link.link (json%{"context": $context, "display": $s})) + pure none toTeX := none extraCss := [highlightingStyle] extraJs := [highlightingJs] @@ -86,7 +193,9 @@ inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) where | .ok (cfg : CodeConfig) => let i := hl.indentation let hl := hl.deIndent i - withReader (fun ρ => { ρ with codeOptions.inlineProofStates := cfg.showProofStates }) <| + withReader + ({ · with + codeOptions.inlineProofStates := cfg.showProofStates, codeOptions.definitionsAsTargets := cfg.defSite.getD false }) <| hl.inlineHtml "examples" block_extension Block.leanOutput (severity : MessageSeverity) (message : String) (summarize : Bool := false) where diff --git a/src/verso/Verso/Code/External.lean b/src/verso/Verso/Code/External.lean index 00e46e166..27d6f80bc 100644 --- a/src/verso/Verso/Code/External.lean +++ b/src/verso/Verso/Code/External.lean @@ -37,6 +37,12 @@ register_option verso.examples.suggest : Bool := { structure CodeConfig where /-- Whether to render proof states -/ showProofStates : Bool := true + /-- + Whether to treat names defined in the code as link targets. + + If unspecified, the block or inline element in question may fall back to a default value. + -/ + defSite : Option Bool := none deriving DecidableEq, Ord, Repr, Quote, ToExpr, ToJson, FromJson /-- @@ -118,8 +124,8 @@ structure CodeModuleContext extends CodeConfig where module : Ident instance : FromArgs CodeModuleContext m where - fromArgs := ((·, ·) <$> moduleOrDefault <*> .namedD `showProofStates .bool true) <&> fun (m, s) => - ({module := m, showProofStates := s}) + fromArgs := ((·, ·, ·) <$> moduleOrDefault <*> .namedD `showProofStates .bool true <*> .named `defSite .bool true) <&> fun (m, s, d) => + ({module := m, showProofStates := s, defSite := d}) /-- A specification of which module to look in to find example code, potentially made more specific with @@ -354,7 +360,7 @@ Requires that the genre have an `ExternalCode` instance. @[code_block_expander module] def module : CodeBlockExpander | args, code => withTraceNode `Elab.Verso (fun _ => pure m!"module") <| do - let cfg@{ module := moduleName, anchor?, showProofStates := _ } ← parseThe CodeContext args + let cfg@{ module := moduleName, anchor?, showProofStates := _, defSite := _ } ← parseThe CodeContext args withAnchored moduleName anchor? fun hl => do logInfos hl let hlString := hl.toString @@ -388,7 +394,7 @@ Requires that the genre have an `ExternalCode` instance. @[role_expander module] def moduleInline : RoleExpander | args, inls => withTraceNode `Elab.Verso (fun _ => pure m!"moduleInline") <| do - let cfg@{module := moduleName, anchor?, showProofStates := _} ← parseThe CodeContext args + let cfg@{module := moduleName, anchor?, showProofStates := _, defSite := _} ← parseThe CodeContext args let code? ← oneCodeStr? inls withAnchored moduleName anchor? fun hl => do @@ -437,7 +443,7 @@ Requires that the genre have an `ExternalCode` instance. @[role_expander moduleName] def moduleName : RoleExpander | args, inls => withTraceNode `Elab.Verso (fun _ => pure m!"moduleName") <| do - let cfg@{module := moduleName, anchor?, show?, showProofStates := _} ← parseThe NameContext args + let cfg@{module := moduleName, anchor?, show?, showProofStates := _, defSite := _} ← parseThe NameContext args let name ← oneCodeStr inls let nameStr := name.getString @@ -493,7 +499,7 @@ Requires that the genre have an `ExternalCode` instance. @[role_expander moduleTerm] def moduleTerm : RoleExpander | args, inls => withTraceNode `Elab.Verso (fun _ => pure m!"moduleTerm") <| do - let cfg@{module := moduleName, anchor?, showProofStates := _} ← parseThe CodeContext args + let cfg@{module := moduleName, anchor?, showProofStates := _, defSite := _} ← parseThe CodeContext args let term ← oneCodeStr inls withAnchored moduleName anchor? fun hl => do @@ -526,7 +532,7 @@ macro_rules @[code_block_expander moduleTerm, inherit_doc moduleTerm] def moduleTermBlock : CodeBlockExpander | args, term => withTraceNode `Elab.Verso (fun _ => pure m!"moduleTerm") <| do - let cfg@{module := moduleName, anchor?, showProofStates := _} ← parseThe CodeContext args + let cfg@{module := moduleName, anchor?, showProofStates := _, defSite := _} ← parseThe CodeContext args withAnchored moduleName anchor? fun hl => do let str := term.getString.trim @@ -579,7 +585,7 @@ Requires that the genre have an `ExternalCode` instance. @[code_block_expander moduleOut] def moduleOut : CodeBlockExpander | args, str => withTraceNode `Elab.Verso (fun _ => pure m!"moduleOut") <| do - let {module := moduleName, anchor?, severity, showProofStates := _} ← parseThe MessageContext args + let {module := moduleName, anchor?, severity, showProofStates := _, defSite := _} ← parseThe MessageContext args withAnchored moduleName anchor? fun hl => do let infos : Array _ := allInfo hl @@ -635,7 +641,7 @@ def moduleOutRole : RoleExpander | args, inls => withTraceNode `Elab.Verso (fun _ => pure m!"moduleOutRole") <| do let str? ← oneCodeStr? inls - let {module := moduleName, anchor?, severity, showProofStates := _} ← parseThe MessageContext args + let {module := moduleName, anchor?, severity, showProofStates := _, defSite := _} ← parseThe MessageContext args withAnchored moduleName anchor? fun hl => do let infos := allInfo hl diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean index bc35c026b..23a2a3f4b 100644 --- a/src/verso/Verso/Code/Highlighted.lean +++ b/src/verso/Verso/Code/Highlighted.lean @@ -112,6 +112,7 @@ structure CodeLink where description : String /-- The actual link destination -/ href : String +deriving Repr, DecidableEq, Ord instance : ToJson CodeLink where toJson l := json%{"short": $l.shortDescription, "long": $l.description, "href": $l.href} @@ -181,6 +182,7 @@ structure HighlightHtmlM.Options where inlineProofStates : Bool := true visibleProofStates : VisibleProofStates := .none collapseGoals : CollapseGoals := .subsequent + definitionsAsTargets : Bool := true structure HighlightHtmlM.Context where linkTargets : LinkTargets @@ -383,9 +385,10 @@ defmethod Token.Kind.data : Token.Kind → String defmethod Token.Kind.idAttr : Token.Kind → HighlightHtmlM (Array (String × String)) | .const n _ _ true => do - if let some id := (← read).definitionIds.find? n then - pure #[("id", id)] - else pure #[] + if (← read).options.definitionsAsTargets then + if let some id := (← read).definitionIds.find? n then + return #[("id", id)] + pure #[] | _ => pure #[] defmethod Token.toHtml (tok : Token) : HighlightHtmlM Html := do @@ -513,16 +516,18 @@ partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM Html | .point s info => pure {{{{info}}}} | .seq hls => hls.mapM toHtml -defmethod Highlighted.blockHtml (contextName : String) (code : Highlighted) (trim : Bool := true) : HighlightHtmlM Html := do +defmethod Highlighted.blockHtml (contextName : String) (code : Highlighted) (trim : Bool := true) (htmlId : Option String := none) : HighlightHtmlM Html := do let code := if trim then code.trim else code - pure {{ {{ ← code.toHtml }} }} + let idAttr := htmlId.map (fun x => #[("id", x)]) |>.getD #[] + pure {{ {{ ← code.toHtml }} }} -defmethod Highlighted.inlineHtml (contextName : Option String) (code : Highlighted) (trim : Bool := true) : HighlightHtmlM Html := do +defmethod Highlighted.inlineHtml (contextName : Option String) (code : Highlighted) (trim : Bool := true) (htmlId : Option String := none) : HighlightHtmlM Html := do let code := if trim then code.trim else code + let idAttr := htmlId.map (fun x => #[("id", x)]) |>.getD #[] if let some ctx := contextName then - pure {{ {{ ← code.toHtml }} }} + pure {{ {{ ← code.toHtml }} }} else - pure {{ {{ ← code.toHtml }} }} + pure {{ {{ ← code.toHtml }} }} -- TODO CSS variables, and document them def highlightingStyle : String := " From a166afab19b8a8015257092339edbcd83b66656b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 22 Jul 2025 16:03:33 +0200 Subject: [PATCH 07/15] chore: bump SubVerso --- examples/anchor-examples/lake-manifest.json | 2 +- examples/documented-package/lake-manifest.json | 2 +- examples/website-examples/lake-manifest.json | 2 +- examples/website-literate/lake-manifest.json | 2 +- lake-manifest.json | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/examples/anchor-examples/lake-manifest.json b/examples/anchor-examples/lake-manifest.json index 59203533a..887895ee9 100644 --- a/examples/anchor-examples/lake-manifest.json +++ b/examples/anchor-examples/lake-manifest.json @@ -6,7 +6,7 @@ "url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, - "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d", + "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/documented-package/lake-manifest.json b/examples/documented-package/lake-manifest.json index ed12671b8..5483172d7 100644 --- a/examples/documented-package/lake-manifest.json +++ b/examples/documented-package/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d", + "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/website-examples/lake-manifest.json b/examples/website-examples/lake-manifest.json index 59203533a..887895ee9 100644 --- a/examples/website-examples/lake-manifest.json +++ b/examples/website-examples/lake-manifest.json @@ -6,7 +6,7 @@ "url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, - "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d", + "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/website-literate/lake-manifest.json b/examples/website-literate/lake-manifest.json index 039ec8178..09e0de0f9 100644 --- a/examples/website-literate/lake-manifest.json +++ b/examples/website-literate/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d", + "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lake-manifest.json b/lake-manifest.json index d8dd6dfdd..53f802d58 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d", + "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", From 37dbb5d27a5533372ea1af1b0f7f6b1aa7cc59d4 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 22 Jul 2025 23:03:49 +0200 Subject: [PATCH 08/15] feat: useful helpers --- src/verso-manual/VersoManual/ExternalLean.lean | 2 +- src/verso/Verso/Code/Highlighted.lean | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/verso-manual/VersoManual/ExternalLean.lean b/src/verso-manual/VersoManual/ExternalLean.lean index 70a6217cb..cba05fd16 100644 --- a/src/verso-manual/VersoManual/ExternalLean.lean +++ b/src/verso-manual/VersoManual/ExternalLean.lean @@ -75,7 +75,7 @@ def exampleDomainMapper : DomainMapper := { Extracts all names that are marked as definition sites, with both their occurrence in the source and the underlying name. -/ -private partial def definedNames : Highlighted → Array (Name × String) +partial def definedNames : Highlighted → Array (Name × String) | .token ⟨.const n _ _ true, s⟩ => #[(n, s)] | .token _ => #[] | .span _ hl | .tactics _ _ _ hl => definedNames hl diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean index 23a2a3f4b..cffedf7a0 100644 --- a/src/verso/Verso/Code/Highlighted.lean +++ b/src/verso/Verso/Code/Highlighted.lean @@ -213,6 +213,9 @@ def withCollapsedSubgoals (policy : HighlightHtmlM.CollapseGoals) (act : Highlig def withVisibleProofStates (policy : HighlightHtmlM.VisibleProofStates) (act : HighlightHtmlM α) : HighlightHtmlM α := withReader (fun ctx => {ctx with options := {ctx.options with visibleProofStates := policy} }) act +def withDefinitionsAsTargets (saveIds : Bool) (act : HighlightHtmlM α) : HighlightHtmlM α := + withReader (fun ctx => {ctx with options := {ctx.options with definitionsAsTargets := saveIds} }) act + def linkTargets : HighlightHtmlM LinkTargets := do return (← readThe HighlightHtmlM.Context).linkTargets From 0c5278b94beda187b0e6610efdd5fdfb587462ce Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 23 Jul 2025 16:57:36 +0200 Subject: [PATCH 09/15] fix: properly assign IDs to example definitions Before, there were ID conflicts when a name was reused. --- examples/custom-genre/SimplePage.lean | 3 +- examples/website/DemoSiteMain.lean | 6 +- src/verso-blog/VersoBlog.lean | 2 +- src/verso-blog/VersoBlog/Generate.lean | 5 +- src/verso-blog/VersoBlog/Template.lean | 6 +- src/verso-blog/VersoBlog/Traverse.lean | 4 + src/verso-manual/VersoManual.lean | 8 +- src/verso-manual/VersoManual/Basic.lean | 202 ++++++++++++++++-- src/verso-manual/VersoManual/Docstring.lean | 28 +-- .../VersoManual/ExternalLean.lean | 83 +------ src/verso-manual/VersoManual/InlineLean.lean | 15 +- .../VersoManual/InlineLean/Block.lean | 21 +- .../VersoManual/InlineLean/Option.lean | 2 +- .../VersoManual/InlineLean/Signature.lean | 2 +- src/verso/Verso/Code/Highlighted.lean | 107 +++++----- src/verso/Verso/Doc.lean | 48 +++-- src/verso/Verso/Doc/Elab/Monad.lean | 7 + src/verso/Verso/Doc/Html.lean | 27 +-- 18 files changed, 350 insertions(+), 226 deletions(-) diff --git a/examples/custom-genre/SimplePage.lean b/examples/custom-genre/SimplePage.lean index 883b258ab..f7495a314 100644 --- a/examples/custom-genre/SimplePage.lean +++ b/examples/custom-genre/SimplePage.lean @@ -156,6 +156,8 @@ implement traversal for the provided part metadata, block extensions, and inline instance : TraversePart SimplePage := {} +instance : TraverseBlock SimplePage := {} + instance : Traverse SimplePage TraverseM where part _ := pure none block _ := pure () @@ -220,7 +222,6 @@ instance : GenreHtml SimplePage IO where | .inr ⟨dest, some t⟩, contents => do pure {{ {{← contents.mapM recur}} }} - /-- The main function to be called to produce HTML output -/ diff --git a/examples/website/DemoSiteMain.lean b/examples/website/DemoSiteMain.lean index b78e456fb..edbc44e81 100644 --- a/examples/website/DemoSiteMain.lean +++ b/examples/website/DemoSiteMain.lean @@ -79,8 +79,8 @@ def demoSite : Site := site DemoSite.Front / DemoSite.Blog.FirstPost -def linkTargets : Code.LinkTargets where - const n := #[{shortDescription := "doc", description := s!"Documentation for {n}", href := s!"http://site.example/constlink/{n}"}] - definition d := #[{shortDescription := "def", description := "Definition", href := s!"http://site.example/deflink/{d}"}] +def linkTargets : Code.LinkTargets TraverseContext where + const n _ := #[{shortDescription := "doc", description := s!"Documentation for {n}", href := s!"http://site.example/constlink/{n}"}] + definition d _ := #[{shortDescription := "def", description := "Definition", href := s!"http://site.example/deflink/{d}"}] def main := blogMain theme demoSite (linkTargets := linkTargets) diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index 7c635b9d1..31af60388 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -799,7 +799,7 @@ private def filterString (p : Char → Bool) (str : String) : String := Id.run < pure out open Template in -def blogMain (theme : Theme) (site : Site) (relativizeUrls := true) (linkTargets : Code.LinkTargets := {}) +def blogMain (theme : Theme) (site : Site) (relativizeUrls := true) (linkTargets : Code.LinkTargets TraverseContext := {}) (options : List String) (components : Components := by exact %registered_components) : IO UInt32 := do let hasError ← IO.mkRef false diff --git a/src/verso-blog/VersoBlog/Generate.lean b/src/verso-blog/VersoBlog/Generate.lean index ede6dcf06..c077e0d59 100644 --- a/src/verso-blog/VersoBlog/Generate.lean +++ b/src/verso-blog/VersoBlog/Generate.lean @@ -27,7 +27,7 @@ structure Generate.Context where site : Site ctxt : TraverseContext xref : TraverseState - linkTargets : LinkTargets + linkTargets : LinkTargets TraverseContext /-- The root directory in which to generate the static site -/ dir : System.FilePath config : Config @@ -77,7 +77,7 @@ def GenerateM.toHtml (g : Genre) (bg.context_eq ▸ ctxt) (bg.state_eq ▸ state) {} - linkTargets + (bg.context_eq ▸ linkTargets) {} x (← get) @@ -92,6 +92,7 @@ namespace Params def forPart [BlogGenre g] [GenreHtml g ComponentM] [ToHtml g ComponentM (Part g)] + [ToHtml g ComponentM (Block g)] (txt : Part g) : GenerateM Params := do let titleHtml : Html ← txt.title.mapM (GenerateM.toHtml g) let preamble ← txt.content.mapM (GenerateM.toHtml g) diff --git a/src/verso-blog/VersoBlog/Template.lean b/src/verso-blog/VersoBlog/Template.lean index 140ce1329..41a168610 100644 --- a/src/verso-blog/VersoBlog/Template.lean +++ b/src/verso-blog/VersoBlog/Template.lean @@ -147,7 +147,7 @@ def blockHtml (g : Genre) pure {{ 
     {{ content.toHtml }}
    }} | .highlightedCode { contextName, showProofStates } hls, _contents => withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <| - hls.blockHtml (toString contextName) + hls.blockHtml (toString contextName) (g := g) | .htmlDetails classes summary, contents => do pure {{
    {{summary}} {{← contents.mapM goB}}
    }} | .htmlWrapper name attrs, contents => do @@ -176,11 +176,11 @@ def inlineHtml (g : Genre) [bg : BlogGenre g] Blog.InlineExt → Array (Inline g) → HtmlM g Html | .highlightedCode { contextName, showProofStates } hls, _contents => withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <| - hls.inlineHtml (some <| toString contextName) + hls.inlineHtml (some <| toString contextName) (g := g) | .lexedText content, _contents => do pure {{ {{ content.toHtml }} }} | .customHighlight hls, _contents => do - hls.inlineHtml none + hls.inlineHtml none (g := g) | .label x, contents => do let contentHtml ← contents.mapM go let st ← bg.state_eq ▸ state diff --git a/src/verso-blog/VersoBlog/Traverse.lean b/src/verso-blog/VersoBlog/Traverse.lean index c234e2283..0d939dbc2 100644 --- a/src/verso-blog/VersoBlog/Traverse.lean +++ b/src/verso-blog/VersoBlog/Traverse.lean @@ -109,10 +109,14 @@ def traverser (g : Genre) [bg : BlogGenre g] : Traverse g Blog.TraverseM where instance : TraversePart Page := {} +instance : TraverseBlock Page := {} + instance : Traverse Page Blog.TraverseM := traverser Page instance : TraversePart Post := {} +instance : TraverseBlock Post := {} + instance : Traverse Post Blog.TraverseM := traverser Post end Traverse diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index 33004d541..27875985e 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -214,7 +214,7 @@ structure Config where /-- How to insert links in rendered code -/ - linkTargets : TraverseState → LinkTargets := TraverseState.localTargets + linkTargets : TraverseState → LinkTargets Manual.TraverseContext := TraverseState.localTargets def ensureDir (dir : System.FilePath) : IO Unit := do @@ -341,7 +341,7 @@ partial def toc (depth : Nat) (opts : Html.Options IO) (ctxt : TraverseContext) (state : TraverseState) (definitionIds : NameMap String) - (linkTargets : LinkTargets) : + (linkTargets : LinkTargets Manual.TraverseContext) : Part Manual → StateT (State Html) (ReaderT ExtensionImpls IO) Html.Toc | .mk title sTitle «meta» _ sub => do let titleHtml ← Html.seq <$> title.mapM (Manual.toHtml (m := ReaderT ExtensionImpls IO) opts.lift ctxt state definitionIds linkTargets {} ·) @@ -536,7 +536,7 @@ where let _date := text.metadata.bind (·.date) |>.getD "" -- TODO let opts : Html.Options IO := {logError := fun msg => logError msg} let ctxt := {logError} - let definitionIds := state.definitionIds + let definitionIds := state.definitionIds ctxt let linkTargets := config.linkTargets state let titleHtml ← Html.seq <$> text.title.mapM (Manual.toHtml opts.lift ctxt state definitionIds linkTargets {}) let introHtml ← Html.seq <$> text.content.mapM (Manual.toHtml opts.lift ctxt state definitionIds linkTargets {}) @@ -618,7 +618,7 @@ where let _date := text.metadata.bind (·.date) |>.getD "" -- TODO let opts : Html.Options IO := {logError := fun msg => logError msg} let ctxt := {logError} - let definitionIds := state.definitionIds + let definitionIds := state.definitionIds ctxt let linkTargets := config.linkTargets state let toc ← text.subParts.toList.mapM fun p => toc config.htmlDepth opts (ctxt.inPart p) state definitionIds linkTargets p diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean index 6e3b69538..85317d7b5 100644 --- a/src/verso-manual/VersoManual/Basic.lean +++ b/src/verso-manual/VersoManual/Basic.lean @@ -357,7 +357,33 @@ structure Block where name : Name := by exact decl_name% id : Option InternalId := none data : Json := Json.null -deriving BEq, Hashable, ToJson, FromJson + /-- + A registry for properties that can be used to create ad-hoc protocols for coordination between + block elements in extensions. + -/ + properties : Lean.NameMap String := {} +deriving ToJson, FromJson + +section +local instance : Repr Json := ⟨fun v _ => s!"json%" ++ v.render ⟩ +deriving instance Repr for Block +end + + +instance : BEq Block where + beq + | ⟨n1, i1, d1, p1⟩, ⟨n2, i2, d2, p2⟩ => + n1 == n2 && + i1 == i2 && + ptrEqThen' d1 d2 (· == ·) && + ptrEqThen' p1 p2 fun x y => + x.size == y.size && x.all (fun k v => y.find? k |>.isEqSome v) + +instance : Hashable Block where + hash + | ⟨n, i, d, p⟩ => + have : Ord (Name × String) := Ord.lex ⟨Name.quickCmp⟩ inferInstance + mixHash (hash n) <| mixHash (hash i) <| mixHash (hash d) (hash p.toArray.qsortOrd) structure Inline where name : Name := by exact decl_name% @@ -403,11 +429,24 @@ structure PartHeader where metadata : Option PartMetadata deriving Repr +inductive BlockContext where + | para + | code + | ul + | ol (start : Int) + | dl + | blockquote + | concat + | other (container : Manual.Block) +deriving Repr + structure TraverseContext where /-- The current URL path - will be [] for non-HTML output or in the root -/ path : Path := #[] /-- The path from the root to the current header -/ headers : Array PartHeader := #[] + /-- The path from the current header to the current block -/ + blockContext : Array BlockContext := #[] /-- Whether the current build is a draft (used for hiding TODOs, etc from public builds) -/ draft : Bool := false logError : String → IO Unit @@ -476,12 +515,26 @@ instance : FromJson (Genre.Inline Manual) := inferInstanceAs (FromJson Manual.In namespace Manual +def BlockContext.ofBlock (block : Doc.Block Manual) : BlockContext := + match block with + | .para .. => .para + | .code .. => .code + | .ul .. => .ul + | .ol start .. => .ol start + | .dl .. => .dl + | .blockquote .. => .blockquote + | .concat .. => .concat + | .other container .. => .other container + def PartHeader.ofPart (part : Part Manual) : PartHeader := {titleString := part.titleString, metadata := part.metadata} def TraverseContext.inPart (self : TraverseContext) (part : Part Manual) : TraverseContext := {self with headers := self.headers.push <| .ofPart part} +def TraverseContext.inBlock (self : TraverseContext) (block : Doc.Block Manual) : TraverseContext := + { self with blockContext := self.blockContext.push (.ofBlock block) } + def TraverseContext.sectionNumber (self : TraverseContext) : Array (Option Numbering) := self.headers.map (·.metadata |>.getD {} |>.assignedNumber) @@ -796,15 +849,121 @@ def optionDomain := ``Verso.Genre.Manual.doc.option def convDomain := ``Verso.Genre.Manual.doc.tactic.conv def exampleDomain := ``Verso.Genre.Manual.example -def TraverseState.definitionIds (state : TraverseState) : NameMap String := Id.run do +def TraverseState.definitionIds (state : TraverseState) (ctxt : TraverseContext) : NameMap String := Id.run do + let exampleBlock := ctxt.blockContext.findSomeRev? fun + | .other x => x.properties.find? `Verso.Genre.Manual.exampleDefContext + | _ => none + let exampleDeco := exampleBlock.map (s!" (in {·})") if let some examples := state.domains.find? exampleDomain then let mut idMap := {} for (x, _) in examples.objects do - if let .ok { htmlId := slug, .. } := state.resolveDomainObject exampleDomain x then - idMap := idMap.insert x.toName slug.toString + let afterSpace := x.dropWhile (· != ' ') + if exampleDeco.isEqSome afterSpace then + if let .ok { htmlId := slug, .. } := state.resolveDomainObject exampleDomain x then + idMap := idMap.insert (x.takeWhile (· != ' ') |>.toName) slug.toString + else if afterSpace.isEmpty then + if let .ok { htmlId := slug, .. } := state.resolveDomainObject exampleDomain x then + idMap := idMap.insert x.toName slug.toString return idMap else return {} +open Verso.Search in +/-- +Quick jump configuration for definitions in examples +-/ +def exampleDomainMapper : DomainMapper := { + displayName := "Example Definition", + className := "example-def", + -- This is a bit of a hack. Examples with repeated names should really get differing canonical + -- names, but it's unclear what to use for them. Perhaps it should be the concatenated tags of the + -- containing sections, with a sequence number in case of further duplication? For now, this + -- fairly complicated mapper does the job. It'd also be good to have a way to show metadata in the + -- quick-jump box, with different styling. + dataToSearchables := + "(domainData) => { + const byName = Object.entries(domainData.contents).flatMap(([key, value]) => + value.map(v => ({ + context: v.data[`${v.address}#${v.id}`].context, + name: v.data[`${v.address}#${v.id}`].display, + address: `${v.address}#${v.id}` + }))).reduce((acc, obj) => { + const key = obj.name; + if (!acc.hasOwnProperty(key)) acc[key] = []; + acc[key].push(obj); + return acc; + }, {}) + return Object.entries(byName).flatMap(([key, value]) => { + if (value.length === 0) { return []; } + const firstCtxt = value[0].context; + let prefixLength = 0; + for (let i = 0; i < firstCtxt.length; i++) { + if (value.every(v => i < v.context.length && v.context[i] === firstCtxt[i])) { + prefixLength++; + } else break; + } + return value.map((v) => ({ + searchKey: v.context.slice(prefixLength).concat(v.name).join(' › '), + address: v.address, + domainId: 'Verso.Genre.Manual.example', + ref: value + })); + }); +}" + : DomainMapper }.setFont { family := .code } + +section + +open SubVerso.Highlighting + +/-- +Extracts all names that are marked as definition sites, with both their occurrence in the source and +the underlying name. +-/ +partial def definedNames : Highlighted → Array (Name × String) + | .token ⟨.const n _ _ true, s⟩ => #[(n, s)] + | .token _ => #[] + | .span _ hl | .tactics _ _ _ hl => definedNames hl + | .seq hls => hls.map definedNames |>.foldl (· ++ ·) #[] + | .text .. | .point .. | .unparsed .. => #[] + +variable [Monad m] [MonadReader TraverseContext m] [MonadStateOf TraverseState m] + +/-- +Saves a set of example definitions to the xref database with the expected metadata. +-/ +def saveExampleDefs (id : InternalId) (definedNames : Array (Name × String)) : m Unit := do + let key := (ToJson.toJson id).compress + let assignedIds : Option (Except String Json) := (← get).get? `Verso.Genre.Manual.saveExampleDefs + let assignedIds := assignedIds.bind (·.toOption) |>.getD (Json.mkObj []) + let mut theseIds := if let .ok v@(.obj _) := assignedIds.getObjVal? key then v else Json.mkObj [] + + let exampleBlock := (← read).blockContext.findSomeRev? fun + | .other x => x.properties.find? `Verso.Genre.Manual.exampleDefContext + | _ => none + let context := (← read).headers.map (·.titleString) + let context := exampleBlock.map context.push |>.getD context + for (d, s) in definedNames do + if d.isAnonymous then continue + let thisId := theseIds.getObjValAs? InternalId d.toString |>.toOption + let thisId ← + if let some i := thisId then pure i + else + let i ← freshId + theseIds := theseIds.setObjValAs! d.toString i + pure i + let d := + if let some ex := exampleBlock then s!"{d} (in {ex})" else d.toString + let path ← (·.path) <$> read + let _ ← externalTag thisId path d + modify (·.saveDomainObject exampleDomain d thisId) + if let some link := (← get).externalTags[thisId]? then + modify (·.modifyDomainObjectData exampleDomain d fun v => + let v := if let .obj _ := v then v else .obj {} + v.setObjVal! link.link (json%{"context": $context, "display": $s})) + let assignedIds := assignedIds.setObjVal! key theseIds + modify (·.set `Verso.Genre.Manual.saveExampleDefs assignedIds) +end + def TraverseState.linksFromDomain (domain : Name) (canonicalName : String) (shortDescription description : String) @@ -812,24 +971,30 @@ def TraverseState.linksFromDomain state.resolveDomainObject domain canonicalName |>.toOption |>.toArray |>.map fun l => { shortDescription, description, href := l.link } -def TraverseState.localTargets (state : TraverseState) : Code.LinkTargets where - const := fun x => +def TraverseState.exampleLinks (name : String) (state : TraverseState) (ctxt? : Option TraverseContext) : Array Code.CodeLink := Id.run do + let exampleBlock := ctxt?.bind (·.blockContext.findSomeRev? fun + | .other x => x.properties.find? `Verso.Genre.Manual.exampleDefContext + | _ => none) + let name := exampleBlock.map (s!"{name} (in {·})") |>.getD name + -- There's no `x` in the tooltip on the next line to avoid revealing suppressed namespaces + state.linksFromDomain exampleDomain name "def" s!"Definition of example" + +def TraverseState.localTargets (state : TraverseState) : Code.LinkTargets Manual.TraverseContext where + const := fun x ctxt? => state.linksFromDomain docstringDomain x.toString "doc" s!"Documentation for {x}" ++ - -- There's no `x` in the tooltip on the next line to avoid revealing suppressed namespaces - state.linksFromDomain exampleDomain x.toString "def" s!"Definition of example" - option := fun x => + state.exampleLinks x.toString ctxt? + option := fun x _ctxt? => state.linksFromDomain optionDomain x.toString "doc" s!"Documentation for option {x}" - keyword := fun k => + keyword := fun k _ctxt? => state.linksFromDomain tacticDomain k.toString "doc" "Documentation for tactic" ++ state.linksFromDomain syntaxKindDomain k.toString "doc" "Documentation for syntax" - -def TraverseState.remoteTargets (state : TraverseState) : Code.LinkTargets where - const := fun x => +def TraverseState.remoteTargets (state : TraverseState) : Code.LinkTargets Manual.TraverseContext where + const := fun x _ctxt? => fromRemoteDomain docstringDomain x.toString (s!"doc ({·})") (s!"Documentation for {x} in {·}") - option := fun x => + option := fun x _ctxt? => fromRemoteDomain optionDomain x.toString (s!"doc ({·})") (s!"Documentation for option {x} in {·}") - keyword := fun k => + keyword := fun k _ctxt? => fromRemoteDomain tacticDomain k.toString (s!"doc ({·})") (s!"Documentation for tactic in {·}") ++ fromRemoteDomain syntaxKindDomain k.toString (s!"doc ({·})") (s!"Documentation for syntax in {·}") where @@ -875,6 +1040,9 @@ def sectionDomainMapper : DomainMapper := { instance : TraversePart Manual where inPart p := (·.inPart p) +instance : TraverseBlock Manual where + inBlock b := (·.inBlock b) + instance : Traverse Manual TraverseM where part p := if p.metadata.isNone then pure (some {}) else pure none @@ -967,7 +1135,7 @@ instance : Traverse Manual TraverseM where else pure (part |>.withMetadata «meta» |>.withSubparts subs) genreBlock - | ⟨name, id?, data⟩, content => do + | ⟨name, id?, data, props⟩, content => do if let some id := id? then if let some impl := (← readThe ExtensionImpls).getBlock? name then for js in impl.extraJs do @@ -990,7 +1158,7 @@ instance : Traverse Manual TraverseM where else -- Assign a fresh ID if there is none. It can then be used on the next traversal pass. let id ← freshId - pure <| some <| Block.other ⟨name, some id, data⟩ content + pure <| some <| Block.other ⟨name, some id, data, props⟩ content genreInline | ⟨name, id?, data⟩, content => do if let some id := id? then diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 2effe3c97..3a1abdf67 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -673,9 +673,9 @@ def internalSignature.descr : BlockDescr where return {{ 
    -            {{← name.toHtml}}
+            {{← name.toHtml (g := Manual)}}
             {{← if let some s := signature then do
-                  pure {{" : " {{← s.toHtml}} }}
+                  pure {{" : " {{← s.toHtml (g := Manual)}} }}
                 else pure .empty}}
    @@ -704,7 +704,7 @@ def inheritance.descr : BlockDescr where pure {{
  • - +
    • }} }} @@ -730,7 +730,7 @@ def fieldSignature.descr : BlockDescr where return {{ 
    -            {{visibility}}{{← name.toHtml}} " : " {{ ← signature.toHtml}}
+            {{visibility}}{{← name.toHtml (g := Manual)}} " : " {{ ← signature.toHtml (g := Manual)}}
    {{← if inheritedFrom.isSome then do pure {{ @@ -738,7 +738,7 @@ def fieldSignature.descr : BlockDescr where "Inherited from "
      {{ ← parents.mapM fun p => do - pure {{
    1. {{ ← p.toHtml }}
      2. }} + pure {{
    2. {{ ← p.toHtml (g := Manual) }}
      3. }} }}
    }} @@ -761,7 +761,7 @@ def constructorSignature.descr : BlockDescr where return {{
    - 
    {{← signature.toHtml}}
    + 
    {{← signature.toHtml (g := Manual)}}
    {{← contents.mapM goB}}
    @@ -769,7 +769,7 @@ def constructorSignature.descr : BlockDescr where }} open Verso.Output Html in -def Signature.toHtml : Signature → HighlightHtmlM Html +def Signature.toHtml : Signature → HighlightHtmlM Manual Html | {wide, narrow} => do return {{
    {{← wide.toHtml}}
    {{← narrow.toHtml}}
    }} @@ -907,7 +907,7 @@ def leanFromMarkdown.inlinedescr : InlineDescr := withHighlighting { HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err pure .empty | .ok (hl : Highlighted) => - hl.inlineHtml "docstring-examples" + hl.inlineHtml (g := Manual) "docstring-examples" } @[block_extension leanFromMarkdown] @@ -926,7 +926,7 @@ def leanFromMarkdown.blockdescr : BlockDescr := withHighlighting { HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err pure .empty | .ok (hl : Highlighted) => - hl.blockHtml "docstring-examples" + hl.blockHtml (g := Manual) "docstring-examples" } open Lean Elab Term in @@ -1622,7 +1622,7 @@ def optionDocs.descr : BlockDescr where "option" 
    {{x}}
    -

    "Default value: " {{← defaultValue.toHtml}}

    +

    "Default value: " {{← defaultValue.toHtml (g := Manual)}}

    {{← contents.mapM goB}}
    @@ -1755,7 +1755,7 @@ def tactic.descr : BlockDescr := withHighlighting {
    {{permalink id xref false}} "tactic" - 
    {{← x.toHtml}}
    + 
    {{← x.toHtml (g := Manual)}}
    {{← contents.mapM goB}}
    @@ -1813,7 +1813,7 @@ def tacticInline.descr : InlineDescr := withHighlighting { HtmlT.logError <| "Couldn't deserialize Lean tactic code while rendering HTML: " ++ err pure .empty | .ok (hl : Highlighted) => - hl.inlineHtml "examples" + hl.inlineHtml (g := Manual) "examples" } -- TODO implement a system upstream like the one for normal tactics @@ -1861,7 +1861,7 @@ def convDomainMapper : DomainMapper := { dataToSearchables := "(domainData) => Object.entries(domainData.contents).map(([key, value]) => ({ - searchKey: key, + searchKey: value[0].data.userName, address: `${value[0].address}#${value[0].id}`, domainId: 'Verso.Genre.Manual.doc.tactic.conv', ref: value, @@ -1902,7 +1902,7 @@ def conv.descr : BlockDescr := withHighlighting {
    {{permalink id xref false}} "conv tactic" - 
    {{← x.toHtml}}
    + 
    {{← x.toHtml (g := Manual)}}
    {{← contents.mapM goB}}
    diff --git a/src/verso-manual/VersoManual/ExternalLean.lean b/src/verso-manual/VersoManual/ExternalLean.lean index cba05fd16..4656a4441 100644 --- a/src/verso-manual/VersoManual/ExternalLean.lean +++ b/src/verso-manual/VersoManual/ExternalLean.lean @@ -27,61 +27,6 @@ namespace Verso.Genre.Manual private def hlJsDeps : List JsFile := [{filename := "popper.js", contents := popper}, {filename := "tippy.js", contents := tippy}] -open Verso.Search in -/-- -Quick jump configuration for definitions in examples --/ -def exampleDomainMapper : DomainMapper := { - displayName := "Example Definition", - className := "example-def", - -- This is a bit of a hack. Examples with repeated names should really get differing canonical - -- names, but it's unclear what to use for them. Perhaps it should be the concatenated tags of the - -- containing sections, with a sequence number in case of further duplication? For now, this - -- fairly complicated mapper does the job. It'd also be good to have a way to show metadata in the - -- quick-jump box, with different styling. - dataToSearchables := - "(domainData) => { - const byName = Object.entries(domainData.contents).flatMap(([key, value]) => - value.map(v => ({ - context: v.data[`${v.address}#${v.id}`].context, - name: v.data[`${v.address}#${v.id}`].display, - address: `${v.address}#${v.id}` - }))).reduce((acc, obj) => { - const key = obj.name; - acc[key] = acc[key] || []; - acc[key].push(obj); - return acc; - }, {}) - return Object.entries(byName).flatMap(([key, value]) => { - if (value.length === 0) { return []; } - const firstCtxt = value[0].context; - let prefixLength = 0; - for (let i = 0; i < firstCtxt.length; i++) { - if (value.every(v => i < v.context.length && v.context[i] === firstCtxt[i])) { - prefixLength++; - } else break; - } - return value.map((v) => ({ - searchKey: v.context.slice(prefixLength).concat(v.name).join(' › '), - address: v.address, - domainId: 'Verso.Genre.Manual.example', - ref: value - })); - }); -}" - : DomainMapper} - -/-- -Extracts all names that are marked as definition sites, with both their occurrence in the source and -the underlying name. --/ -partial def definedNames : Highlighted → Array (Name × String) - | .token ⟨.const n _ _ true, s⟩ => #[(n, s)] - | .token _ => #[] - | .span _ hl | .tactics _ _ _ hl => definedNames hl - | .seq hls => hls.map definedNames |>.foldl (· ++ ·) #[] - | .text .. | .point .. | .unparsed .. => #[] - block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) where init st := st.addQuickJumpMapper exampleDomain exampleDomainMapper @@ -102,17 +47,7 @@ block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) where logError <| "Failed to deserialize code config during traversal:" ++ err return none | .ok (defines : Array (Name × String)) => - for (d, s) in defines do - if d.isAnonymous then continue - let d := d.toString - let path ← (·.path) <$> read - let _ ← externalTag id path d - let context := (← read).headers.map (·.titleString) - modify (·.saveDomainObject exampleDomain d id) - if let some link := (← get).externalTags[id]? then - modify (·.modifyDomainObjectData exampleDomain d fun v => - let v := if let .obj _ := v then v else .obj {} - v.setObjVal! link.link (json%{"context": $context, "display": $s})) + saveExampleDefs id defines pure none toTeX := none extraCss := [highlightingStyle] @@ -138,7 +73,7 @@ block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) where let i := hl.indentation let hl := hl.deIndent i withReader ({ · with codeOptions.inlineProofStates := cfg.showProofStates, codeOptions.definitionsAsTargets := cfg.defSite.getD true }) <| - hl.blockHtml "examples" + hl.blockHtml (g := Manual) "examples" inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) where data := @@ -158,17 +93,7 @@ inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) where logError <| "Failed to deserialize code config during traversal:" ++ err return none | .ok (defines : Array (Name × String)) => - for (d, s) in defines do - if d.isAnonymous then continue - let d := d.toString - let path ← (·.path) <$> read - let _ ← externalTag id path d - let context := (← read).headers.map (·.titleString) - modify (·.saveDomainObject exampleDomain d id) - if let some link := (← get).externalTags[id]? then - modify (·.modifyDomainObjectData exampleDomain d fun v => - let v := if let .obj _ := v then v else .obj {} - v.setObjVal! link.link (json%{"context": $context, "display": $s})) + saveExampleDefs id defines pure none toTeX := none extraCss := [highlightingStyle] @@ -196,7 +121,7 @@ inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) where withReader ({ · with codeOptions.inlineProofStates := cfg.showProofStates, codeOptions.definitionsAsTargets := cfg.defSite.getD false }) <| - hl.inlineHtml "examples" + hl.inlineHtml (g := Manual) "examples" block_extension Block.leanOutput (severity : MessageSeverity) (message : String) (summarize : Bool := false) where data := ToJson.toJson (severity, message, summarize) diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean index 4592bd958..d55d95e34 100644 --- a/src/verso-manual/VersoManual/InlineLean.lean +++ b/src/verso-manual/VersoManual/InlineLean.lean @@ -25,7 +25,7 @@ import VersoManual.InlineLean.SyntaxError open Lean Elab open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets ExpectString -open SubVerso.Highlighting Highlighted +open SubVerso.Highlighting open Verso.SyntaxUtils (parserInputString runParserCategory' SyntaxError) @@ -38,7 +38,7 @@ private def hlJsDeps : List JsFile := inline_extension Inline.lean (hls : Highlighted) where data := - let defined := hls.definedNames.toArray + let defined := definedNames hls Json.arr #[ToJson.toJson hls, ToJson.toJson defined] traverse id data _ := do @@ -48,11 +48,8 @@ inline_extension Inline.lean (hls : Highlighted) where | .error err => logError <| "Couldn't deserialize Lean code while traversing inline example: " ++ err pure none - | .ok (defs : Array Name) => - let path ← (·.path) <$> read - for n in defs do - let _ ← externalTag id path n.toString - modify (·.saveDomainObject exampleDomain n.toString id) + | .ok (defs : Array (Name × String)) => + saveExampleDefs id defs pure none toTeX := some <| fun go _ _ content => do @@ -72,7 +69,7 @@ inline_extension Inline.lean (hls : Highlighted) where HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err pure .empty | .ok (hl : Highlighted) => - hl.inlineHtml "examples" + hl.inlineHtml (g := Manual) "examples" section Config @@ -743,7 +740,7 @@ inline_extension Inline.name where HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err pure .empty | .ok (hl : Highlighted) => - hl.inlineHtml "examples" + hl.inlineHtml (g := Manual) "examples" structure NameConfig where full : Option Name diff --git a/src/verso-manual/VersoManual/InlineLean/Block.lean b/src/verso-manual/VersoManual/InlineLean/Block.lean index d7dc872de..00582fcd5 100644 --- a/src/verso-manual/VersoManual/InlineLean/Block.lean +++ b/src/verso-manual/VersoManual/InlineLean/Block.lean @@ -19,9 +19,11 @@ open SubVerso.Highlighting namespace Verso.Genre.Manual.InlineLean block_extension Block.lean (hls : Highlighted) (file : Option System.FilePath := none) (range : Option Lsp.Range := none) where + init s := s.addQuickJumpMapper exampleDomain exampleDomainMapper data := - let defined := hls.definedNames.toArray + let defined := definedNames hls Json.arr #[ToJson.toJson hls, ToJson.toJson defined, ToJson.toJson file, ToJson.toJson range] + traverse id data _ := do let .arr #[_, defined, _, _] := data | logError "Expected two-element JSON for Lean code" *> pure none @@ -29,11 +31,8 @@ block_extension Block.lean (hls : Highlighted) (file : Option System.FilePath := | .error err => logError <| "Couldn't deserialize Lean code while traversing block example: " ++ err pure none - | .ok (defs : Array Name) => - let path ← (·.path) <$> read - for n in defs do - let _ ← externalTag id path n.toString - modify (·.saveDomainObject exampleDomain n.toString id) + | .ok (defs : Array (Name × String)) => + saveExampleDefs id defs pure none toTeX := some <| fun _ go _ _ content => do @@ -46,11 +45,17 @@ block_extension Block.lean (hls : Highlighted) (file : Option System.FilePath := toHtml := open Verso.Output.Html in some <| fun _ _ _ data _ => do - let .arr #[hlJson, _, _, _] := data + let .arr #[hlJson, ds, _, _] := data | HtmlT.logError "Expected four-element JSON for Lean code" *> pure .empty match FromJson.fromJson? hlJson with | .error err => HtmlT.logError <| "Couldn't deserialize Lean code block while rendering HTML: " ++ err pure .empty | .ok (hl : Highlighted) => - hl.blockHtml "examples" + --if hl.toString.startsWith "namespace A" then + -- dbg_trace hl.toString + -- dbg_trace ds + -- have : Ord (Name × String) := Ord.lex ⟨fun x y => compare x.toString y.toString⟩ inferInstance + -- for (x, y) in (← HtmlT.definitionIds).toArray.qsortOrd do + -- dbg_trace "{x}\t=>\t{y}" + hl.blockHtml (g := Manual) "examples" diff --git a/src/verso-manual/VersoManual/InlineLean/Option.lean b/src/verso-manual/VersoManual/InlineLean/Option.lean index 35fd5e44b..8b932c786 100644 --- a/src/verso-manual/VersoManual/InlineLean/Option.lean +++ b/src/verso-manual/VersoManual/InlineLean/Option.lean @@ -54,4 +54,4 @@ def option.descr : InlineDescr where HtmlT.logError <| "Couldn't deserialize Lean option code while rendering HTML: " ++ err pure .empty | .ok (hl : Highlighted) => - hl.inlineHtml "examples" + hl.inlineHtml (g := Manual) "examples" diff --git a/src/verso-manual/VersoManual/InlineLean/Signature.lean b/src/verso-manual/VersoManual/InlineLean/Signature.lean index 59ad4f93c..acb4f1ef5 100644 --- a/src/verso-manual/VersoManual/InlineLean/Signature.lean +++ b/src/verso-manual/VersoManual/InlineLean/Signature.lean @@ -38,7 +38,7 @@ block_extension Block.signature where HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML signature: " ++ err ++ "\n" ++ toString data pure .empty | .ok (hl : Highlighted) => - hl.blockHtml "examples" + hl.blockHtml (g := Manual) "examples" declare_syntax_cat signature_spec diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean index cffedf7a0..f928d2712 100644 --- a/src/verso/Verso/Code/Highlighted.lean +++ b/src/verso/Verso/Code/Highlighted.lean @@ -7,6 +7,7 @@ import Lean.Data.OpenDecl import Lean.Data.Json import Std.Data.HashMap import SubVerso.Highlighting +import Verso.Doc import Verso.Method import Verso.Output.Html @@ -138,23 +139,23 @@ Instructions for computing link targets for various code elements. Each kind of link may have multiple destinations. The first is the default link, while the remainder are considered alternates. -/ -structure LinkTargets where - var : FVarId → Array CodeLink := fun _ => #[] - sort : Level → Array CodeLink := fun _ => #[] - const : Name → Array CodeLink := fun _ => #[] - option : Name → Array CodeLink := fun _ => #[] - keyword : Name → Array CodeLink := fun _ => #[] - definition : Name → Array CodeLink := fun _ => #[] - -def LinkTargets.augment (tgts1 tgts2 : LinkTargets) : LinkTargets where - var fv := tgts1.var fv ++ tgts2.var fv - sort l := tgts1.sort l ++ tgts2.sort l - const n := tgts1.const n ++ tgts2.const n - option o := tgts1.option o ++ tgts2.option o - keyword kw := tgts1.keyword kw ++ tgts2.keyword kw - definition x := tgts1.definition x ++ tgts2.definition x - -instance : Append LinkTargets where +structure LinkTargets (Ctxt : Type) where + var : FVarId → Option Ctxt → Array CodeLink := fun _ _ => #[] + sort : Level → Option Ctxt → Array CodeLink := fun _ _ => #[] + const : Name → Option Ctxt → Array CodeLink := fun _ _ => #[] + option : Name → Option Ctxt → Array CodeLink := fun _ _ => #[] + keyword : Name → Option Ctxt → Array CodeLink := fun _ _ => #[] + definition : Name → Option Ctxt → Array CodeLink := fun _ _ => #[] + +def LinkTargets.augment (tgts1 tgts2 : LinkTargets g) : LinkTargets g where + var fv ctxt := tgts1.var fv ctxt ++ tgts2.var fv ctxt + sort l ctxt := tgts1.sort l ctxt ++ tgts2.sort l ctxt + const n ctxt := tgts1.const n ctxt ++ tgts2.const n ctxt + option o ctxt := tgts1.option o ctxt ++ tgts2.option o ctxt + keyword kw ctxt := tgts1.keyword kw ctxt ++ tgts2.keyword kw ctxt + definition x ctxt := tgts1.definition x ctxt ++ tgts2.definition x ctxt + +instance : Append (LinkTargets g) where append := LinkTargets.augment inductive HighlightHtmlM.CollapseGoals where @@ -184,8 +185,9 @@ structure HighlightHtmlM.Options where collapseGoals : CollapseGoals := .subsequent definitionsAsTargets : Bool := true -structure HighlightHtmlM.Context where - linkTargets : LinkTargets +structure HighlightHtmlM.Context (g : Verso.Doc.Genre) where + linkTargets : LinkTargets g.TraverseContext + traverseContext : g.TraverseContext definitionIds : Lean.NameMap String options : HighlightHtmlM.Options @@ -197,64 +199,65 @@ The monad enables the following features: 2. Conveying document-wide configurations, in particular policies for hyperlinking identifiers. 3. De-duplicating hovers, which can greatly reduce the size of generated HTML. -/ -abbrev HighlightHtmlM α := ReaderT HighlightHtmlM.Context (StateT (State Html) Id) α +abbrev HighlightHtmlM g α := ReaderT (HighlightHtmlM.Context g) (StateT (State Html) Id) α -def addHover (content : Html) : HighlightHtmlM Nat := modifyGet fun st => +def addHover (content : Html) : HighlightHtmlM g Nat := modifyGet fun st => let (hoverId, dedup) := st.dedup.insert content (hoverId, {st with dedup := dedup}) -def uniqueId (base := "--verso-unique") : HighlightHtmlM String := modifyGet fun st => +def uniqueId (base := "--verso-unique") : HighlightHtmlM g String := modifyGet fun st => let (id, idSupply) := st.idSupply.unique (base := base) (id, {st with idSupply := idSupply}) -def withCollapsedSubgoals (policy : HighlightHtmlM.CollapseGoals) (act : HighlightHtmlM α) : HighlightHtmlM α := +def withCollapsedSubgoals (policy : HighlightHtmlM.CollapseGoals) (act : HighlightHtmlM g α) : HighlightHtmlM g α := withReader (fun ctx => {ctx with options := {ctx.options with collapseGoals := policy} }) act -def withVisibleProofStates (policy : HighlightHtmlM.VisibleProofStates) (act : HighlightHtmlM α) : HighlightHtmlM α := +def withVisibleProofStates (policy : HighlightHtmlM.VisibleProofStates) (act : HighlightHtmlM g α) : HighlightHtmlM g α := withReader (fun ctx => {ctx with options := {ctx.options with visibleProofStates := policy} }) act -def withDefinitionsAsTargets (saveIds : Bool) (act : HighlightHtmlM α) : HighlightHtmlM α := +def withDefinitionsAsTargets (saveIds : Bool) (act : HighlightHtmlM g α) : HighlightHtmlM g α := withReader (fun ctx => {ctx with options := {ctx.options with definitionsAsTargets := saveIds} }) act -def linkTargets : HighlightHtmlM LinkTargets := do - return (← readThe HighlightHtmlM.Context).linkTargets +def linkTargets : HighlightHtmlM g (LinkTargets g.TraverseContext) := do + return (← readThe (HighlightHtmlM.Context g)).linkTargets -def options : HighlightHtmlM HighlightHtmlM.Options := do - return (← readThe HighlightHtmlM.Context).options +def options : HighlightHtmlM g HighlightHtmlM.Options := do + return (← readThe (HighlightHtmlM.Context g)).options open Lean in open Verso.Output.Html in -def constLink (constName : Name) (content : Html) : HighlightHtmlM Html := do - return CodeLink.manyHtml ((← linkTargets).const constName) content +def constLink (constName : Name) (content : Html) (ctxt : Option g.TraverseContext := none) : HighlightHtmlM g Html := do + return CodeLink.manyHtml ((← linkTargets).const constName ctxt) content open Lean in open Verso.Output.Html in -def optionLink (optionName : Name) (content : Html) : HighlightHtmlM Html := do - return CodeLink.manyHtml ((← linkTargets).option optionName) content +def optionLink (optionName : Name) (content : Html) (ctxt : Option g.TraverseContext := none) : HighlightHtmlM g Html := do + return CodeLink.manyHtml ((← linkTargets).option optionName ctxt) content open Lean in open Verso.Output.Html in -def varLink (varName : FVarId) (content : Html) : HighlightHtmlM Html := do - return CodeLink.manyHtml ((← linkTargets).var varName) content +def varLink (varName : FVarId) (content : Html) (ctxt : Option g.TraverseContext := none) : HighlightHtmlM g Html := do + return CodeLink.manyHtml ((← linkTargets).var varName ctxt) content open Lean in open Verso.Output.Html in -def kwLink (kind : Name) (content : Html) : HighlightHtmlM Html := do - return CodeLink.manyHtml ((← linkTargets).keyword kind) content +def kwLink (kind : Name) (content : Html) (ctxt : Option g.TraverseContext := none) : HighlightHtmlM g Html := do + return CodeLink.manyHtml ((← linkTargets).keyword kind ctxt) content open Lean in open Verso.Output.Html in -def defLink (defName : Name) (content : Html) : HighlightHtmlM Html := do - return CodeLink.manyHtml ((← linkTargets).definition defName) content +def defLink (defName : Name) (content : Html) (ctxt : Option g.TraverseContext := none) : HighlightHtmlM g Html := do + return CodeLink.manyHtml ((← linkTargets).definition defName ctxt) content -defmethod Token.Kind.addLink (tok : Token.Kind) (content : Html) : HighlightHtmlM Html := do +defmethod Token.Kind.addLink (tok : Token.Kind) (content : Html) : HighlightHtmlM g Html := do + let ctxt := (← read).traverseContext match tok with - | .const x _ _ false => constLink x content - | .const x _ _ true => defLink x content - | .option o .. => optionLink o content - | .var x .. => varLink x content - | .keyword (some k) .. => kwLink k content + | .const x _ _ false => constLink x content (some ctxt) + | .const x _ _ true => defLink x content (some ctxt) + | .option o .. => optionLink o content (some ctxt) + | .var x .. => varLink x content (some ctxt) + | .keyword (some k) .. => kwLink k content (some ctxt) | _ => pure content /-- @@ -308,7 +311,7 @@ Removes leading and trailing whitespace from highlighted code. -/ defmethod Highlighted.trim (hl : Highlighted) : Highlighted := hl.trimLeft.trimRight -defmethod Token.Kind.hover? (tok : Token.Kind) : HighlightHtmlM (Option Nat) := +defmethod Token.Kind.hover? (tok : Token.Kind) : HighlightHtmlM g (Option Nat) := match tok with | .const _n sig doc _ | .anonCtor _n sig doc => let docs := @@ -386,7 +389,7 @@ defmethod Token.Kind.data : Token.Kind → String | .levelOp op => s!"level-op-{op}" | _ => "" -defmethod Token.Kind.idAttr : Token.Kind → HighlightHtmlM (Array (String × String)) +defmethod Token.Kind.idAttr : Token.Kind → HighlightHtmlM g (Array (String × String)) | .const n _ _ true => do if (← read).options.definitionsAsTargets then if let some id := (← read).definitionIds.find? n then @@ -394,7 +397,7 @@ defmethod Token.Kind.idAttr : Token.Kind → HighlightHtmlM (Array (String × St pure #[] | _ => pure #[] -defmethod Token.toHtml (tok : Token) : HighlightHtmlM Html := do +defmethod Token.toHtml (tok : Token) : HighlightHtmlM g Html := do let hoverId ← tok.kind.hover? let idAttr ← tok.kind.idAttr let hoverAttr := hoverId.map (fun i => #[("data-verso-hover", toString i)]) |>.getD #[] @@ -402,7 +405,7 @@ defmethod Token.toHtml (tok : Token) : HighlightHtmlM Html := do {{tok.content}} }} -defmethod Highlighted.Goal.toHtml (exprHtml : expr → HighlightHtmlM Html) (index : Nat) : Highlighted.Goal expr → HighlightHtmlM Html +defmethod Highlighted.Goal.toHtml (exprHtml : expr → HighlightHtmlM g Html) (index : Nat) : Highlighted.Goal expr → HighlightHtmlM g Html | {name, goalPrefix, hypotheses, conclusion} => do let hypsHtml : Html ← if hypotheses.size = 0 then pure .empty @@ -477,7 +480,7 @@ def _root_.Array.mapIndexedM [Monad m] (arr : Array α) (f : Fin arr.size → α out := out.push (← f ⟨i, by get_elem_tactic⟩ arr[i]) pure out -partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM Html +partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM g Html | .token t => t.toHtml | .text str | .unparsed str => pure {{{{str}}}} | .span infos hl => @@ -519,12 +522,12 @@ partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM Html | .point s info => pure {{{{info}}}} | .seq hls => hls.mapM toHtml -defmethod Highlighted.blockHtml (contextName : String) (code : Highlighted) (trim : Bool := true) (htmlId : Option String := none) : HighlightHtmlM Html := do +defmethod Highlighted.blockHtml (contextName : String) (code : Highlighted) (trim : Bool := true) (htmlId : Option String := none) : HighlightHtmlM g Html := do let code := if trim then code.trim else code let idAttr := htmlId.map (fun x => #[("id", x)]) |>.getD #[] pure {{ {{ ← code.toHtml }} }} -defmethod Highlighted.inlineHtml (contextName : Option String) (code : Highlighted) (trim : Bool := true) (htmlId : Option String := none) : HighlightHtmlM Html := do +defmethod Highlighted.inlineHtml (contextName : Option String) (code : Highlighted) (trim : Bool := true) (htmlId : Option String := none) : HighlightHtmlM g Html := do let code := if trim then code.trim else code let idAttr := htmlId.map (fun x => #[("id", x)]) |>.getD #[] if let some ctx := contextName then diff --git a/src/verso/Verso/Doc.lean b/src/verso/Verso/Doc.lean index adbdb74c3..6b99a369c 100644 --- a/src/verso/Verso/Doc.lean +++ b/src/verso/Verso/Doc.lean @@ -434,15 +434,26 @@ instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] : Repr (Part g) := class TraversePart (g : Genre) where /-- - How to modify the context while traversing the contents a given part. - This is applied after `part` and `genrePart` have rewritten the text, if applicable. + How to modify the context while traversing the contents of a given part. This is applied after + `part` and `genrePart` have rewritten the text, if applicable. It is also used during HTML generation. -/ inPart : Part g → g.TraverseContext → g.TraverseContext := fun _ => id +class TraverseBlock (g : Genre) where + /-- + How to modify the context while traversing a given block. + + It is also used during HTML generation. + -/ + inBlock : Block g → g.TraverseContext → g.TraverseContext := fun _ => id + + instance : TraversePart .none := {} +instance : TraverseBlock .none := {} + /-- Genre-specific traversal. @@ -474,7 +485,7 @@ class Traverse (g : Genre) (m : outParam (Type → Type)) where partial def Genre.traverse (g : Genre) - [Traverse g m] [TraversePart g] [Monad m] + [Traverse g m] [TraversePart g] [TraverseBlock g] [Monad m] [MonadReader g.TraverseContext m] [MonadWithReader g.TraverseContext m] [MonadState g.TraverseState m] (top : Part g) : m (Part g) := @@ -498,21 +509,22 @@ where block (b : Doc.Block g) : m (Doc.Block g) := do Traverse.block b - match b with - | .para contents => .para <$> contents.mapM inline - | .ul items => .ul <$> items.mapM fun - | ListItem.mk contents => ListItem.mk <$> contents.mapM block - | .ol start items => .ol start <$> items.mapM fun - | ListItem.mk contents => ListItem.mk <$> contents.mapM block - | .dl items => .dl <$> items.mapM fun - | DescItem.mk t d => DescItem.mk <$> t.mapM inline <*> d.mapM block - | .blockquote items => .blockquote <$> items.mapM block - | .concat items => .concat <$> items.mapM block - | .other container content => - match ← Traverse.genreBlock container content with - | .none => .other container <$> content.mapM block - | .some b' => block b' - | .code .. => pure b + withReader (TraverseBlock.inBlock b) <| + match b with + | .para contents => .para <$> contents.mapM inline + | .ul items => .ul <$> items.mapM fun + | ListItem.mk contents => ListItem.mk <$> contents.mapM block + | .ol start items => .ol start <$> items.mapM fun + | ListItem.mk contents => ListItem.mk <$> contents.mapM block + | .dl items => .dl <$> items.mapM fun + | DescItem.mk t d => DescItem.mk <$> t.mapM inline <*> d.mapM block + | .blockquote items => .blockquote <$> items.mapM block + | .concat items => .concat <$> items.mapM block + | .other container content => do + match ← Traverse.genreBlock container content with + | .none => .other container <$> content.mapM block + | .some b' => block b' + | .code .. => pure b part (p : Doc.Part g) : m (Doc.Part g) := do let meta' ← Traverse.part p diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean index 6c5b75a9c..a53137468 100644 --- a/src/verso/Verso/Doc/Elab/Monad.lean +++ b/src/verso/Verso/Doc/Elab/Monad.lean @@ -75,6 +75,13 @@ def nullInline_to_string : InlineToString return String.join <| contents.toList.map (inlineToString env) | _, _ => none +@[inline_to_string Lean.Parser.Term.app] +def app_to_string : InlineToString := fun (env : Environment) => fun + | `(Verso.Doc.Inline.text $s:str) => + return s.getString + | `(Verso.Doc.Inline.concat #[$xs,*]) => + return String.join <| (xs : Array _).toList.map (inlineToString env) + | _ => none def inlinesToString (env : Environment) (inlines : Array Syntax) : String := String.intercalate " " (inlines.map (inlineToString env)).toList diff --git a/src/verso/Verso/Doc/Html.lean b/src/verso/Verso/Doc/Html.lean index 74103d3bd..f88b01348 100644 --- a/src/verso/Verso/Doc/Html.lean +++ b/src/verso/Verso/Doc/Html.lean @@ -38,7 +38,7 @@ structure HtmlT.Context (genre : Genre) (m : Type → Type) where occurrence for later cross-referencing? -/ definitionIds : Lean.NameMap String - linkTargets : Code.LinkTargets + linkTargets : Code.LinkTargets genre.TraverseContext codeOptions : Code.HighlightHtmlM.Options def HtmlT.Context.reinterpret (lift : {α : _} → m α → m' α) (ctx : HtmlT.Context g m) : HtmlT.Context g m' := @@ -48,14 +48,14 @@ def HtmlT.Context.reinterpret (lift : {α : _} → m α → m' α) (ctx : HtmlT. def HtmlT.Context.lift [MonadLiftT m m'] (ctx : HtmlT.Context g m) : HtmlT.Context g m' := ctx.reinterpret monadLift - def HtmlT.Context.cast {g1 g2 : Genre} (ctx : HtmlT.Context g1 m) (context_eq : g1.TraverseContext = g2.TraverseContext := by trivial) (state_eq : g1.TraverseState = g2.TraverseState := by trivial) : HtmlT.Context g2 m := - {ctx with + { ctx with traverseContext := context_eq ▸ ctx.traverseContext, - traverseState := state_eq ▸ ctx.traverseState } + traverseState := state_eq ▸ ctx.traverseState, + linkTargets := context_eq ▸ ctx.linkTargets } abbrev HtmlT (genre : Genre) (m : Type → Type) : Type → Type := ReaderT (HtmlT.Context genre m) (StateT (Verso.Code.Hover.State Html) m) @@ -82,17 +82,16 @@ def HtmlT.state [Monad m] : HtmlT genre m genre.TraverseState := do def HtmlT.definitionIds [Monad m] : HtmlT genre m (Lean.NameMap String) := do return (← read).definitionIds -def HtmlT.linkTargets [Monad m] : HtmlT genre m Code.LinkTargets := do +def HtmlT.linkTargets [Monad m] : HtmlT genre m (Code.LinkTargets genre.TraverseContext) := do return (← read).linkTargets def HtmlT.codeOptions [Monad m] : HtmlT genre m Code.HighlightHtmlM.Options := do return (← read).codeOptions - def HtmlT.logError [Monad m] (message : String) : HtmlT genre m Unit := do (← options).logError message -instance [Monad m] : MonadLift HighlightHtmlM (HtmlT genre m) where - monadLift act := do modifyGet (act ⟨← HtmlT.linkTargets, ← HtmlT.definitionIds, ← HtmlT.codeOptions⟩) +instance [Monad m] : MonadLift (HighlightHtmlM genre) (HtmlT genre m) where + monadLift act := do modifyGet (act ⟨← HtmlT.linkTargets, ← HtmlT.context, ← HtmlT.definitionIds, ← HtmlT.codeOptions⟩) open HtmlT @@ -152,7 +151,9 @@ instance [Monad m] [GenreHtml g m] : ToHtml g m (Inline g) where toHtml := Inline.toHtml -partial def Block.toHtml [Monad m] [GenreHtml g m] : Block g → HtmlT g m Html +partial def Block.toHtml [Monad m] [GenreHtml g m] [TraverseBlock g] (b : Block g) : HtmlT g m Html := + withReader (fun ctxt => { ctxt with traverseContext := TraverseBlock.inBlock b ctxt.traverseContext } ) do + match b with | .para xs => do pure {{

    {{← xs.mapM Inline.toHtml }}

    }} | .blockquote bs => do @@ -177,10 +178,10 @@ partial def Block.toHtml [Monad m] [GenreHtml g m] : Block g → HtmlT g m Html | .other container content => GenreHtml.block Inline.toHtml Block.toHtml container content -instance [Monad m] [GenreHtml g m] : ToHtml g m (Block g) where +instance [Monad m] [GenreHtml g m] [TraverseBlock g] : ToHtml g m (Block g) where toHtml := Block.toHtml -partial def Part.toHtml [Monad m] [GenreHtml g m] [TraversePart g] +partial def Part.toHtml [Monad m] [GenreHtml g m] [TraversePart g] [TraverseBlock g] (p : Part g) (mkHeader : Nat → Html → Html := mkPartHeader) : HtmlT g m Html := match p.metadata with | .none => do @@ -197,7 +198,7 @@ partial def Part.toHtml [Monad m] [GenreHtml g m] [TraversePart g] | some m => GenreHtml.part (fun p mkHeader => Part.toHtml p (mkHeader := mkHeader)) m p.withoutMetadata -instance [Monad m] [GenreHtml g m] [TraversePart g] : ToHtml g m (Part g) where +instance [Monad m] [GenreHtml g m] [TraversePart g] [TraverseBlock g] : ToHtml g m (Part g) where toHtml p := Part.toHtml p instance : GenreHtml .none m where @@ -208,7 +209,7 @@ instance : GenreHtml .none m where defmethod Genre.toHtml (g : Genre) [ToHtml g m α] (options : Options m) (context : g.TraverseContext) (state : g.TraverseState) (definitionIds : Lean.NameMap String) - (linkTargets : Code.LinkTargets) (codeOptions : Code.HighlightHtmlM.Options) + (linkTargets : Code.LinkTargets g.TraverseContext) (codeOptions : Code.HighlightHtmlM.Options) (x : α) : StateT (Verso.Code.Hover.State Html) m Html := ToHtml.toHtml x ⟨options, context, state, definitionIds, linkTargets, codeOptions⟩ From 2c40b5ab4c55a13e0e67ebd66011f8f318f54000 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 23 Jul 2025 17:01:50 +0200 Subject: [PATCH 10/15] chore: latest subverso --- examples/anchor-examples/lake-manifest.json | 2 +- examples/documented-package/lake-manifest.json | 2 +- examples/website-examples/lake-manifest.json | 2 +- examples/website-literate/lake-manifest.json | 2 +- lake-manifest.json | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/examples/anchor-examples/lake-manifest.json b/examples/anchor-examples/lake-manifest.json index 887895ee9..373a7b1f8 100644 --- a/examples/anchor-examples/lake-manifest.json +++ b/examples/anchor-examples/lake-manifest.json @@ -6,7 +6,7 @@ "url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, - "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", + "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/documented-package/lake-manifest.json b/examples/documented-package/lake-manifest.json index 5483172d7..316dac986 100644 --- a/examples/documented-package/lake-manifest.json +++ b/examples/documented-package/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", + "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/website-examples/lake-manifest.json b/examples/website-examples/lake-manifest.json index 887895ee9..373a7b1f8 100644 --- a/examples/website-examples/lake-manifest.json +++ b/examples/website-examples/lake-manifest.json @@ -6,7 +6,7 @@ "url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, - "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", + "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/website-literate/lake-manifest.json b/examples/website-literate/lake-manifest.json index 09e0de0f9..0e34ec32b 100644 --- a/examples/website-literate/lake-manifest.json +++ b/examples/website-literate/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", + "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lake-manifest.json b/lake-manifest.json index 53f802d58..9b23a65e6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2160afd9e8bd70ec39c31ca9e840f765a63bd79b", + "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", From f73f0e30573d673282d8e0b6375839f5945d42a1 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 23 Jul 2025 17:03:22 +0200 Subject: [PATCH 11/15] fix: warning --- src/verso-manual/VersoManual/InlineLean/Block.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/verso-manual/VersoManual/InlineLean/Block.lean b/src/verso-manual/VersoManual/InlineLean/Block.lean index 00582fcd5..a240b00aa 100644 --- a/src/verso-manual/VersoManual/InlineLean/Block.lean +++ b/src/verso-manual/VersoManual/InlineLean/Block.lean @@ -45,7 +45,7 @@ block_extension Block.lean (hls : Highlighted) (file : Option System.FilePath := toHtml := open Verso.Output.Html in some <| fun _ _ _ data _ => do - let .arr #[hlJson, ds, _, _] := data + let .arr #[hlJson, _ds, _, _] := data | HtmlT.logError "Expected four-element JSON for Lean code" *> pure .empty match FromJson.fromJson? hlJson with | .error err => From da8c34147fc23568c5bc8a1258deb87b4206b39d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 23 Jul 2025 17:15:40 +0200 Subject: [PATCH 12/15] chore: bump TL version --- .github/workflows/ci.yml | 2 +- .github/workflows/merge-main-nightly.yml | 2 +- .github/workflows/update-nightly.yml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 06f7cb0bc..7e39d3367 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -76,7 +76,7 @@ jobs: - name: Install PDF Dependencies uses: zauguin/install-texlive@v4 with: - texlive_version: 2024 + texlive_version: 2025 packages: | scheme-minimal l3packages diff --git a/.github/workflows/merge-main-nightly.yml b/.github/workflows/merge-main-nightly.yml index 38185f9b1..358c53d13 100644 --- a/.github/workflows/merge-main-nightly.yml +++ b/.github/workflows/merge-main-nightly.yml @@ -66,7 +66,7 @@ jobs: - name: Install PDF Dependencies uses: zauguin/install-texlive@v4 with: - texlive_version: 2024 + texlive_version: 2025 packages: | scheme-minimal l3packages diff --git a/.github/workflows/update-nightly.yml b/.github/workflows/update-nightly.yml index 58e1295c7..d87450e47 100644 --- a/.github/workflows/update-nightly.yml +++ b/.github/workflows/update-nightly.yml @@ -123,7 +123,7 @@ jobs: - name: Install PDF Dependencies uses: zauguin/install-texlive@v4 with: - texlive_version: 2024 + texlive_version: 2025 packages: | scheme-minimal l3packages From e11ca79169ffd3cd5481fd16ba812aac5aad4026 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 23 Jul 2025 22:04:11 +0200 Subject: [PATCH 13/15] chore: TypeScript in CI for search --- .github/workflows/ci.yml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7e39d3367..17fe97074 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -115,6 +115,17 @@ jobs: cp -r _out/html-single html-single-page zip -r html-single-page.zip html-single-page + - name: Install TypeScript + run: | + sudo apt update && sudo apt install node-typescript + + - uses: actions/checkout@v4 + + - name: Type check the search bar code + run: | + cd _out/html-multi/-verso-search + tsc --noEmit -p jsconfig.json + - name: Upload docs to artifact storage if: github.ref != 'refs/heads/main' uses: actions/upload-artifact@v4 From ea09fdca5413d8ddffc1054f229aba8d136199ee Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 23 Jul 2025 22:08:11 +0200 Subject: [PATCH 14/15] debug --- .github/workflows/ci.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 17fe97074..9629127e0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -123,6 +123,8 @@ jobs: - name: Type check the search bar code run: | + pwd + ls cd _out/html-multi/-verso-search tsc --noEmit -p jsconfig.json From 5d5be9a924b436a956ee885286f9040d88e02ebe Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 23 Jul 2025 22:12:47 +0200 Subject: [PATCH 15/15] remove checkout step --- .github/workflows/ci.yml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9629127e0..07bf39f3e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -119,12 +119,8 @@ jobs: run: | sudo apt update && sudo apt install node-typescript - - uses: actions/checkout@v4 - - name: Type check the search bar code run: | - pwd - ls cd _out/html-multi/-verso-search tsc --noEmit -p jsconfig.json