diff --git a/.github/workflows/check-search-tsc.yml b/.github/workflows/check-search-tsc.yml
new file mode 100644
index 00000000..79a9cf30
--- /dev/null
+++ b/.github/workflows/check-search-tsc.yml
@@ -0,0 +1,19 @@
+name: Check for copyright headers
+
+on: [pull_request]
+
+jobs:
+ check-lean-files:
+ runs-on: ubuntu-latest
+ steps:
+ - 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 static/search
+ tsc --noEmit -p jsconfig.json
+
diff --git a/.vale/scripts/rewrite_html.py b/.vale/scripts/rewrite_html.py
index 349ee37c..ab4c1aba 100644
--- a/.vale/scripts/rewrite_html.py
+++ b/.vale/scripts/rewrite_html.py
@@ -51,6 +51,10 @@ def process_html_file(filepath, output_filepath):
for inner in element.contents:
inner.replace_with(inner.get_text())
+ # Delete software license info
+ for element in soup.find_all("section", class_="license-info"):
+ element.decompose()
+
# Ensure the output directory exists
os.makedirs(os.path.dirname(output_filepath), exist_ok=True)
diff --git a/Main.lean b/Main.lean
index 7f1ec3aa..916e807b 100644
--- a/Main.lean
+++ b/Main.lean
@@ -9,17 +9,125 @@ import VersoManual
open Verso.Genre.Manual
+open Verso.Output.Html in
+def searchModule := {{
+
+ }}
+
+
+def KaTeXLicense : LicenseInfo where
+ identifier := "MIT"
+ dependency := "KaTeX"
+ howUsed := "KaTeX is used to render mathematical notation."
+ link := "https://katex.org/"
+ text := #[(some "The MIT License", text)]
+where
+ text := r#"
+Copyright (c) 2013-2020 Khan Academy and other contributors
+
+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 addKaTeX (config : Config) : Config :=
+ {config with
+ extraCss := "/static/katex/katex.min.css" :: config.extraCss,
+ extraJs := "/static/katex/katex.min.js" :: "/static/math.js" :: config.extraJs,
+ licenseInfo := KaTeXLicense :: config.licenseInfo
+ }
+
+
+def fuzzysortLicense : 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 w3ComboboxLicense : 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/"
+
+
+"#
def main :=
manualMain (%doc Manual) (config := config)
where
- config := {
+ config := addKaTeX {
extraFiles := [("static", "static")],
- extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
- extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],
+ extraCss := [
+ "/static/colors.css",
+ "/static/theme.css",
+ "/static/print.css",
+ "/static/search/search-box.css",
+ "/static/fonts/source-serif/source-serif-text.css",
+ "/static/fonts/source-code-pro/source-code-pro.css",
+ ],
+ extraJs := [
+ -- Search box
+ "/static/search/fuzzysort.js",
+ -- Print stylesheet improvements
+ "/static/print.js"
+ ],
+ extraHead := #[searchModule],
emitTeX := false,
emitHtmlSingle := true, -- for proofreading
logo := some "/static/lean_logo.svg",
sourceLink := some "https://github.com/leanprover/reference-manual",
issueLink := some "https://github.com/leanprover/reference-manual/issues"
+ -- Licenses for the search box
+ licenseInfo := [fuzzysortLicense, w3ComboboxLicense]
}
diff --git a/Manual/BuildTools/Lake/Config.lean b/Manual/BuildTools/Lake/Config.lean
index ce6d41b9..5d8fe427 100644
--- a/Manual/BuildTools/Lake/Config.lean
+++ b/Manual/BuildTools/Lake/Config.lean
@@ -74,7 +74,7 @@ Field names not used by Lake should not be used to store metadata to be processe
The top-level contents of `lakefile.toml` specify the options that apply to the package itself, including metadata such as the name and version, the locations of the files in the {tech}[workspace], compiler flags to be used for all {tech}[targets], and
The only mandatory field is `name`, which declares the package's name.
-::::tomlTableDocs "Package Configuration" Lake.PackageConfig skip:=backend skip:=releaseRepo? skip:=buildArchive? skip:=manifestFile skip:=moreServerArgs
+::::tomlTableDocs root "Package Configuration" Lake.PackageConfig skip:=backend skip:=releaseRepo? skip:=buildArchive? skip:=manifestFile skip:=moreServerArgs
:::tomlFieldCategory "Metadata" name version versionTags description keywords homepage license licenseFiles readmeFile reservoir
These options describe the package.
@@ -294,7 +294,7 @@ There are three kinds of sources:
* Git repositories, which may be local paths or URLs
* Local paths
-::::tomlTableDocs "Requiring Packages" Lake.Dependency skip:=src? skip := opts skip:=subdir skip:=version?
+::::tomlTableDocs "require" "Requiring Packages" Lake.Dependency skip:=src? skip := opts skip:=subdir skip:=version?
The `path` and `git` fields specify an explicit source for a dependency.
If neither are provided, then the dependency is fetched from {ref "reservoir"}[Reservoir], or an alternative registry if one has been configured.
@@ -448,7 +448,7 @@ source = {type = "git", url = "https://example.com/example.git"}
Library targets are expected in the `lean_lib` array of tables.
-::::tomlTableDocs "Library Targets" Lake.LeanLibConfig skip := backend skip:=globs skip:=nativeFacets
+::::tomlTableDocs "lean_lib" "Library Targets" Lake.LeanLibConfig skip := backend skip:=globs skip:=nativeFacets
::::
:::::example "Minimal Library Target"
@@ -522,7 +522,7 @@ If its modules are accessed at elaboration time, they will be compiled to native
## Executable Targets
-:::: tomlTableDocs "Executable Targets" Lake.LeanExeConfig skip := backend skip:=globs skip:=nativeFacets
+:::: tomlTableDocs "lean_exe" "Executable Targets" Lake.LeanExeConfig skip := backend skip:=globs skip:=nativeFacets
::::
diff --git a/Manual/IO.lean b/Manual/IO.lean
index fc2f9157..74306282 100644
--- a/Manual/IO.lean
+++ b/Manual/IO.lean
@@ -87,6 +87,9 @@ Without using one of a few clearly-marked unsafe operators, programs have no way
This ensures that the correct ordering of side effects is preserved, and it ensures that programs that have side effects are clearly marked as such.
## The `IO`, `EIO` and `BaseIO` Monads
+%%%
+tag := "io-monad"
+%%%
There are two monads that are typically used for programs that interact with the real world:
@@ -126,7 +129,10 @@ example : BaseIO = EIO Empty := rfl
{docstring IO.toEIO}
-## Errors and Error Handling
+## Errors and Error Handling in `IO`
+%%%
+tag := "io-monad-errors"
+%%%
Error handling in the {lean}`IO` monad uses the same facilities as any other {tech}[exception monad].
In particular, throwing and catching exceptions uses the methods of the {name}`MonadExceptOf` {tech}[type class].
@@ -193,6 +199,9 @@ Access granted!
::::
### Constructing IO Errors
+%%%
+tag := "io-error-construction"
+%%%
{docstring IO.Error.mkUnsupportedOperation}
@@ -248,6 +257,9 @@ Access granted!
{docstring IO.Error.mkInappropriateTypeFile}
# Control Structures
+%%%
+tag := "io-monad-control"
+%%%
Normally, programs written in {lean}`IO` use {ref "monads-and-do"}[the same control structures as those written in other monads].
There is one specific {lean}`IO` helper.
@@ -261,10 +273,16 @@ There is one specific {lean}`IO` helper.
{include 0 Manual.IO.Files}
# Environment Variables
+%%%
+tag := "io-monad-getenv"
+%%%
{docstring IO.getEnv}
# Timing
+%%%
+tag := "io-timing"
+%%%
{docstring IO.sleep}
@@ -277,6 +295,9 @@ There is one specific {lean}`IO` helper.
{docstring IO.addHeartbeats}
# Processes
+%%%
+tag := "io-processes"
+%%%
## Current Process
diff --git a/Manual/Intro.lean b/Manual/Intro.lean
index 677efea1..81345844 100644
--- a/Manual/Intro.lean
+++ b/Manual/Intro.lean
@@ -218,3 +218,11 @@ inductive Even : Nat → Prop where
{docstring Even}
::::
+
+# Open-Source Licenses
+%%%
+tag := "dependency-licenses"
+number := false
+%%%
+
+{licenseInfo}
diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
index 29a4088c..c2a87e2e 100644
--- a/Manual/Language/InductiveTypes.lean
+++ b/Manual/Language/InductiveTypes.lean
@@ -288,6 +288,13 @@ Instead of writing the constructor's name applied to its arguments, the explicit
This works in both pattern and expression contexts.
Providing arguments by name or converting all implicit parameters to explicit parameters with `@` requires using the ordinary constructor syntax.
+:::syntax term (title := "Anonymous Constructors")
+Constructors can be invoked anonymously by enclosing their explicit arguments in angle brackets, separated by commas.
+```grammar
+⟨ $_,* ⟩
+```
+:::
+
::::example "Anonymous constructors"
:::keepEnv
diff --git a/Manual/Meta/Example.lean b/Manual/Meta/Example.lean
index eeb0e58e..0bd73705 100644
--- a/Manual/Meta/Example.lean
+++ b/Manual/Meta/Example.lean
@@ -24,12 +24,12 @@ def Block.example (name : Option String) : Block where
structure ExampleConfig where
description : FileMap × Array Syntax
/-- Name for refs -/
- name : Option String := none
+ tag : Option String := none
keep : Bool := false
def ExampleConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m] : ArgParse m ExampleConfig :=
- ExampleConfig.mk <$> .positional `description .inlinesString <*> .named `name .string true <*> (.named `keep .bool true <&> (·.getD false))
+ ExampleConfig.mk <$> .positional `description .inlinesString <*> .named `tag .string true <*> (.named `keep .bool true <&> (·.getD false))
def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α → m β) (xs : Array α) : m (Array β) := do
let mut out := #[]
@@ -71,7 +71,7 @@ def «example» : DirectiveExpander
withoutModifyingEnv <| prioritizedElab (isLeanBlock ·) elabBlock contents
-- Examples are represented using the first block to hold the description. Storing it in the JSON
-- entails repeated (de)serialization.
- pure #[← ``(Block.other (Block.example $(quote cfg.name)) #[Block.para #[$description,*], $blocks,*])]
+ pure #[← ``(Block.other (Block.example $(quote cfg.tag)) #[Block.para #[$description,*], $blocks,*])]
@[block_extension «example»]
def example.descr : BlockDescr where
diff --git a/Manual/Meta/LakeToml.lean b/Manual/Meta/LakeToml.lean
index befc69e8..36d2ab31 100644
--- a/Manual/Meta/LakeToml.lean
+++ b/Manual/Meta/LakeToml.lean
@@ -20,6 +20,7 @@ import Manual.Meta.Basic
import Manual.Meta.ExpectString
import Manual.Meta.Lean.Scopes
import Manual.Meta.Lean.Block
+import Manual.Meta.LakeToml.Toml
import Lake
import Lake.Toml.Decode
@@ -122,12 +123,10 @@ def Inline.tomlField (inTable : Name) (field : Name) : Inline where
name := `Manual.Inline.tomlField
data := ToJson.toJson (inTable, field)
-def Block.tomlTable (name : String) (typeName : Name) : Block where
+def Block.tomlTable (arrayKey : Option String) (name : String) (typeName : Name) : Block where
name := `Manual.Block.tomlTable
- data := ToJson.toJson (name, typeName)
+ data := ToJson.toJson (arrayKey, name, typeName)
-def tomlFieldDomain := `Manual.lakeTomlField
-def tomlTableDomain := `Manual.lakeTomlTable
structure TomlFieldOpts where
inTable : Name
@@ -164,10 +163,14 @@ def Block.tomlField.descr : BlockDescr where
traverse id info _ := do
let .ok (_, inTable, field) := FromJson.fromJson? (α := Option Nat × Name × Toml.Field Empty) info
| do logError "Failed to deserialize field doc data"; pure none
+
+ let tableArrayKey : Option Json := (← get).getDomainObject? tomlTableDomain inTable.toString |>.bind fun t =>
+ t.data.getObjVal? "arrayKey" |>.toOption
+
modify fun s =>
let name := s!"{inTable} {field.name}"
s |>.saveDomainObject tomlFieldDomain name id
- |>.saveDomainObjectData tomlFieldDomain name inTable.toString
+ |>.saveDomainObjectData tomlFieldDomain name (json%{"table": $inTable.toString, "tableArrayKey": $(tableArrayKey.getD .null), "field": $field.name.toString})
discard <| externalTag id (← read).path s!"{inTable}-{field.name}"
pure none
toTeX := none
@@ -177,26 +180,13 @@ def Block.tomlField.descr : BlockDescr where
toHtml := some <| fun _goI goB id info contents =>
open Verso.Doc.Html in
open Verso.Output Html in do
- let .ok (_, inTable, field) := FromJson.fromJson? (α := Option Nat × Name × Toml.Field Empty) info
+ let .ok (_, _inTable, field) := FromJson.fromJson? (α := Option Nat × Name × Toml.Field Empty) info
| do Verso.Doc.Html.HtmlT.logError "Failed to deserialize field doc data"; pure .empty
let sig : Html := {{ {{field.name.toString}} }}
let xref ← HtmlT.state
let idAttr := xref.htmlId id
- let name := s!"{inTable} {field.name}"
-
- let label : Option Html := do
- let .str tableName ← xref.getDomainObject? tomlFieldDomain name <&> (·.data)
- | none
- let table ← xref.getDomainObject? tomlTableDomain tableName
- let #[id] := table.ids.toArray
- | none
- let .str name := table.data
- | none
- let (path, slug) ← xref.externalTags[id]?
- pure {{"field in "{{name}}}}
-
return {{
{{sig}}
@@ -269,11 +259,13 @@ def Block.tomlFieldCategory.descr : BlockDescr where
@[block_extension Block.tomlTable]
def Block.tomlTable.descr : BlockDescr where
traverse id info _ := do
- let .ok (humanName, typeName) := FromJson.fromJson? (α := String × Name) info
+ let .ok (arrayKey, humanName, typeName) := FromJson.fromJson? (α := Option String × String × Name) info
| do logError "Failed to deserialize FFI doc data"; pure none
+ let arrayKeyJson := arrayKey.map Json.str |>.getD Json.null
modify fun s =>
s |>.saveDomainObject tomlTableDomain typeName.toString id
- |>.saveDomainObjectData tomlTableDomain typeName.toString humanName
+ |>.saveDomainObjectData tomlTableDomain typeName.toString (json%{"description": $humanName, "type": $typeName.toString, "arrayKey": $arrayKeyJson})
+
discard <| externalTag id (← read).path typeName.toString
pure none
@@ -289,9 +281,16 @@ dl.toml-table-field-spec {
toHtml := some <| fun _goI goB id info contents =>
open Verso.Doc.Html in
open Verso.Output Html in do
- let .ok (humanName, _typeName) := FromJson.fromJson? (α := String × Name) info
- | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize FFI doc data"; pure .empty
- let sig : Html := {{ {{humanName}} }}
+ let .ok (arrayKey, humanName, typeName) := FromJson.fromJson? (α := Option String × String × Name) info
+ | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize Lake TOML table doc data"; pure .empty
+
+ let tableArrayName : Option Toml.Highlighted := arrayKey.map fun k =>
+ .tableHeader <| .tableDelim (.text "[[") ++ .tableName (some typeName.toString) (.key (some k) (.text k)) ++ .tableDelim (.text "]]")
+
+ -- Don't include links here because they'd just be self-links anyway
+ let tableArrayName : Option Html := tableArrayName.map (Toml.Highlighted.toHtml (fun _ => none) (fun _ _ => none))
+
+ let sig : Html := {{ {{humanName}} {{tableArrayName.map ({{" — " {{·}} }}) |>.getD .empty }} }}
let xref ← HtmlT.state
let idAttr := xref.htmlId id
@@ -469,22 +468,37 @@ def Field.toBlock (inTable : Name) (f : Field (Array (Block Genre.Manual))) : Bl
let (f, docs?) := f.takeDocs
.other (Block.tomlField none inTable f) (docs?.getD #[])
-def Table.toBlock (docs : Array (Block Genre.Manual)) (t : Table (Array (Block Genre.Manual))) : Array (Block Genre.Manual) :=
+def Table.toBlock (arrayKey : Option String) (docs : Array (Block Genre.Manual)) (t : Table (Array (Block Genre.Manual))) : Array (Block Genre.Manual) :=
let (fieldBlocks, notFields) := docs.partition (fun b => b matches Block.other {name:=`Manual.Block.tomlField, .. : Genre.Manual.Block} ..)
- #[.other (Block.tomlTable t.name t.typeName) <| notFields ++ (fieldBlocks ++ t.fields.map (Field.toBlock t.typeName))]
+ #[.other (Block.tomlTable arrayKey t.name t.typeName) <| notFields ++ (fieldBlocks ++ t.fields.map (Field.toBlock t.typeName))]
end
end Toml
structure TomlTableOpts where
+ /--
+ `none` to describe the root of the configuration, or a key that points at a table array to
+ describe a nested entry.
+ -/
+ arrayKey : Option String
description : String
name : Name
skip : List Name
def TomlTableOpts.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] : ArgParse m TomlTableOpts :=
- TomlTableOpts.mk <$> .positional `description .string <*> .positional `name .resolvedName <*> many (.named `skip .name false)
+ TomlTableOpts.mk <$> .positional `key arrayKey <*> .positional `description .string <*> .positional `name .resolvedName <*> many (.named `skip .name false)
+where
+ arrayKey := {
+ description := "'root' for the root table, or a string that contains a key for nested tables",
+ get
+ | .name n =>
+ if n.getId == `root then pure none
+ else throwErrorAt n "Expected 'root' or a string"
+ | .str s => pure (some s.getString)
+ | .num n => throwErrorAt n "Expected 'root' or a string"
+ }
open Markdown in
@@ -494,7 +508,7 @@ Interpret a structure type as a TOML table, and generate docs.
@[directive_expander tomlTableDocs]
def tomlTableDocs : DirectiveExpander
| args, contents => do
- let {description, name, skip} ← TomlTableOpts.parse.run args
+ let {arrayKey, description, name, skip} ← TomlTableOpts.parse.run args
let docsStx ←
match ← Lean.findDocString? (← getEnv) name with
| none => throwError m!"No docs found for '{name}'"; pure #[]
@@ -511,488 +525,8 @@ def tomlTableDocs : DirectiveExpander
let userContents ← contents.mapM elabBlock
- return #[← `(Block.concat (Toml.Table.toBlock #[$(docsStx),* , $userContents,*] $tableStx))]
-
-
-namespace Toml
-
-namespace Highlighted
-
-inductive Token where
- | string : String → Token
- | bool : Bool → Token
- | num : Nat → Token -- TODO other kinds of number?
-deriving DecidableEq, Repr, Ord, ToJson, FromJson
-
-open Lean.Syntax in
-open Token in
-instance : Quote Token where
- quote
- | .string s => mkCApp ``string #[quote s]
- | .bool b => mkCApp ``Token.bool #[quote b]
- | .num n => mkCApp ``num #[quote n]
-
-end Highlighted
-
-inductive Highlighted where
- | token : Highlighted.Token → String → Highlighted
- | key (fullPath : Option String) : Highlighted → Highlighted
- | text : String → Highlighted
- | /-- Whitespace from leading/trailing source info -/ ws : String → Highlighted
- | link (url : String) : Highlighted → Highlighted
- | concat : Array Highlighted → Highlighted
- | tableHeader : Highlighted → Highlighted
- | tableName (name : Option String) : Highlighted → Highlighted
- | tableDelim : Highlighted → Highlighted
-deriving Inhabited, Repr, BEq, ToJson, FromJson
-
-open Lean.Syntax in
-open Highlighted in
-partial instance : Quote Highlighted where
- quote := q
-where
- q
- | .token t s => mkCApp ``Highlighted.token #[quote t, quote s]
- | .key p s => mkCApp ``key #[quote p, q s]
- | .text s => mkCApp ``Highlighted.text #[quote s]
- | .ws s => mkCApp ``Highlighted.text #[quote s]
- | .link url s => mkCApp ``Highlighted.link #[quote url, q s]
- | .concat xs =>
- let _ : Quote Highlighted := ⟨q⟩
- mkCApp ``Highlighted.concat #[quote xs]
- | .tableHeader hl => mkCApp ``Highlighted.tableHeader #[q hl]
- | .tableName n hl => mkCApp ``Highlighted.tableName #[quote n, q hl]
- | .tableDelim hl => mkCApp ``Highlighted.tableDelim #[q hl]
-
-instance : Append Highlighted where
- append
- | .concat xs, .concat ys => .concat (xs ++ ys)
- | .concat xs, y => .concat (xs.push y)
- | x, .concat ys => .concat (#[x] ++ ys)
- | x, y => .concat (#[x] ++ [y])
-
-instance : Coe (Array Highlighted) Highlighted where
- coe := .concat
-
-def srcInfoHl : SourceInfo → Highlighted → Highlighted
- | .original leading _ trailing _, hl =>
- mkWs leading.toString ++ #[hl] ++ mkWs trailing.toString
- | _, hl => hl
-where
- mkWs : String → Array Highlighted
- | "" => #[]
- | w => #[.ws w]
-
-private def takeDropWhile (xs : Array α) (p : α → Bool) : Array α × Array α := Id.run do
- for h : i in [0:xs.size] do
- if !p xs[i] then
- return (xs.extract 0 i, xs.extract i xs.size)
- (xs, #[])
-
-private def takeDropWhileRev (xs : Array α) (p : α → Bool) : Array α × Array α := Id.run do
- for h : i in [0:xs.size] do
- have : i < xs.size := by get_elem_tactic
- let j := xs.size - (i + 1)
- if !p xs[j] then
- return (xs.extract 0 (j + 1), xs.extract (j + 1) xs.size)
- (#[], xs)
-
-
-/-- info: (#[], #[1, 2, 3, 4, 5]) -/
-#guard_msgs in
-#eval takeDropWhile #[1,2,3,4,5] (· > 3)
-
-/-- info: (#[1, 2], #[3, 4, 5]) -/
-#guard_msgs in
-#eval takeDropWhile #[1,2,3,4,5] (· < 3)
-
-/-- info: (#[1, 2, 3], #[4, 5]) -/
-#guard_msgs in
-#eval takeDropWhileRev #[1,2,3,4,5] (· > 3)
-
-/-- info: (#[1, 2, 3, 4, 5], #[]) -/
-#guard_msgs in
-#eval takeDropWhileRev #[1,2,3,4,5] (· < 3)
-
-/--
-Normalizes semantic info such that it doesn't have leading or trailing whitespace.
--/
-partial def Highlighted.normalize : Highlighted → Highlighted
- | .concat xs => .concat (normArray (xs.map Highlighted.normalize))
- | .ws x => .ws x
- | .text x => .text x
- | .token t x => .token t x
- | .tableDelim x =>
- let (pre, y, post) := splitWs (normArray #[x.normalize])
- pre ++ .tableDelim y ++ post
- | .tableHeader x =>
- let (pre, y, post) := splitWs (normArray #[x.normalize])
- pre ++ .tableHeader y ++ post
- | .tableName n x =>
- let (pre, y, post) := splitWs (normArray #[x.normalize])
- pre ++ .tableName n y ++ post
- | .key p x =>
- let (pre, y, post) := splitWs (normArray #[x.normalize])
- pre ++ .key p y ++ post
- | .link d x =>
- let (pre, y, post) := splitWs (normArray #[x.normalize])
- pre ++ .link d y ++ post
-
-where
- splitWs (xs : Array Highlighted) : (Array Highlighted × Array Highlighted × Array Highlighted) :=
- let (pre, rest) := takeDropWhile xs (· matches (.ws ..))
- let (mid, post) := takeDropWhileRev rest (· matches (.ws ..))
- (pre, mid, post)
- normArray (xs : Array Highlighted) :=
- xs.flatMap fun
- | .concat ys => normArray ys
- | .ws "" => #[]
- | other => #[other]
-
--- Inefficient string matching, which is fine because URLs are assumed short here
-private def hasSubstring (haystack : String) (needle : String) : Bool := Id.run do
- if needle.isEmpty then return true
- if needle.length > haystack.length then return false
- let mut iter := haystack.iter
- let fst := needle.get 0
- while h : iter.hasNext do
- if iter.curr' h == fst then
- let mut iter' := iter
- let mut iter'' := needle.iter
- while iter'.hasNext && iter''.hasNext do
- if iter'.curr == iter''.curr then
- iter' := iter'.next
- iter'' := iter''.next
- else break
- if iter''.hasNext then
- iter := iter.next
- continue
- else return true
- else
- iter := iter.next
- continue
- return false
-
-/-- info: true -/
-#guard_msgs in
-#eval hasSubstring "" ""
-
-/-- info: false -/
-#guard_msgs in
-#eval hasSubstring "" "a"
-
-/-- info: true -/
-#guard_msgs in
-#eval hasSubstring "bab" "a"
-
-/-- info: true -/
-#guard_msgs in
-#eval hasSubstring "bab" "ab"
-
-/-- info: false -/
-#guard_msgs in
-#eval hasSubstring "bab" "abb"
-
-/-- info: true -/
-#guard_msgs in
-#eval hasSubstring "abcdef" "ef"
-
-/-- info: true -/
-#guard_msgs in
-#eval hasSubstring "https://repohost.example.com/example2.git" "example.com"
-
-/-- info: false -/
-#guard_msgs in
-#eval hasSubstring "https://github.com/example2.git" "example.com"
-
-partial def highlightToml : Syntax → StateM (Option String) Highlighted := fun stx =>
- match stx with
- | .node info `null elts =>
- srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.toml elts =>
- srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.header elts =>
- srcInfoHl info <$> elts.mapM highlightToml
- | stx@(.node info ``Lake.Toml.keyval #[k, eq, v]) => do
- let keypath := (← get).map (· ++ ".") |>.getD ""
- let fullKey :=
- if let `(Lake.Toml.keyval|$k = $_) := stx then
- getKey k |>.map (keypath ++ ·)
- else none
- let hlK ← (.key fullKey) <$> highlightToml k
-
- return srcInfoHl info #[hlK, (← highlightToml eq), (← highlightToml v)]
- | .node info ``Lake.Toml.keyval elts =>
- srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.key elts =>
- (srcInfoHl info ∘ .key none) <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.simpleKey elts => srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.unquotedKey elts => srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.string elts =>
- srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.basicString #[s@(.atom _ str)] =>
- if let some str' := Lean.Syntax.decodeStrLit str then
- if (str'.take 8 == "https://" || str'.take 7 == "http://") && !hasSubstring str' "example.com" then
- (srcInfoHl info ∘ .link str') <$> highlightToml s
- else
- srcInfoHl info <$> highlightToml s
- else
- srcInfoHl info <$> highlightToml s
- | .node info ``Lake.Toml.boolean elts => srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.true #[.atom _ b] =>
- pure <| srcInfoHl info <| .token (.bool true) b
- | .node info ``Lake.Toml.false #[.atom _ b] =>
- pure <| srcInfoHl info <| .token (.bool false) b
- | .node info ``Lake.Toml.arrayTable #[open1, open2, contents, close1, close2] => do
- let n := getKey ⟨contents⟩
- set n
- return srcInfoHl info <| .tableHeader <|
- .tableDelim ((← highlightToml open1) ++ (← highlightToml open2)) ++
- (.tableName n (← highlightToml contents)) ++
- .tableDelim ((← highlightToml close1) ++ (← highlightToml close2))
- | .node info ``Lake.Toml.arrayTable elts =>
- srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.decInt #[.atom _ n] => pure <| srcInfoHl info <| .token (.num n.toNat!) n
- | .node info ``Lake.Toml.array elts => srcInfoHl info <$> elts.mapM highlightToml
- | .node info ``Lake.Toml.inlineTable elts => do
- let x ← get
- set (none : Option String)
- let out ← srcInfoHl info <$> elts.mapM highlightToml
- set x
- return out
- | .atom info str => pure <| srcInfoHl info (.text str)
- | other => panic! s!"Failed to highlight TOML (probably highlightToml in Manual.Meta.LakeToml needs another pattern case): {toString other}"
-
-where
- getKey : TSyntax `Lake.Toml.key → Option String
- | `(Lake.Toml.key| $d:unquotedKey) =>
- d.raw.isLit? ``Lake.Toml.unquotedKey
- | `(Lake.Toml.key| $d:literalString) =>
- d.raw.isLit? ``Lake.Toml.literalString
- | `(Lake.Toml.key| $d:basicString) =>
- d.raw.isLit? ``Lake.Toml.basicString
- | _ => none
-
-/--
-A mapping from paths into the nested tables of the config file to the datatypes at which the field
-documentation can be found.
--/
-def configPaths : Std.HashMap (List String) Name := Std.HashMap.ofList [
- (["require"], ``Lake.Dependency),
- (["lean_lib"], ``Lake.LeanLibConfig),
- (["lean_exe"], ``Lake.LeanExeConfig),
-]
-
-open Verso Output Html in
-partial def Highlighted.toHtml (tableLink : Name → Option String) (keyLink : Name → Name → Option String) : Highlighted -> Html
- | .token t s =>
- match t with
- | .bool _ => {{{{s}}}}
- | .string _ => {{{{s}}}}
- | .num _ => {{{{s}}}}
- | .tableHeader hl =>
- {{}}
- | .tableName n hl =>
- let tableName := n.map (·.splitOn ".") >>= (configPaths[·]?)
- if let some dest := tableName >>= tableLink then
- {{{{hl.toHtml tableLink keyLink}}}}
- else
- hl.toHtml tableLink keyLink
- | .tableDelim hl => {{{{hl.toHtml tableLink keyLink}}}}
- | .concat hls => .seq (hls.map (toHtml tableLink keyLink))
- | .link url hl => {{{{hl.toHtml tableLink keyLink}}}}
- | .text s => s
- | .ws s =>
- let comment := s.find (· == '#')
- let commentStr := s.extract comment s.endPos
- let commentHtml := if commentStr.isEmpty then .empty else {{}}
- {{ {{s.extract 0 comment}} {{commentHtml}} }}
- | .key none k => {{
-
- {{k.toHtml tableLink keyLink}}
-
- }}
- | .key (some p) k =>
- let path := p.splitOn "."
- let dest :=
- if let (table, [k]) := path.splitAt (path.length - 1) then
- if let some t := configPaths[table]? then
- keyLink t k.toName
- else none
- else none
-
- {{
- {{ if let some url := dest then {{
- {{k.toHtml tableLink keyLink}}
- }} else k.toHtml tableLink keyLink }}
-
- }}
-
-
-
-end Toml
-
-def Block.toml (highlighted : Toml.Highlighted) : Block where
- name := `Manual.Block.toml
- data := toJson highlighted
-
-def Inline.toml (highlighted : Toml.Highlighted) : Inline where
- name := `Manual.Inline.toml
- data := toJson highlighted
-
-
-open Verso.Output Html in
-def htmlLink (state : TraverseState) (id : InternalId) (html : Html) : Html :=
- if let some (path, htmlId) := state.externalTags[id]? then
- {{{{html}}}}
- else html
-
-open Verso.Output Html in
-def htmlDest (state : TraverseState) (id : InternalId) : Option String :=
- if let some (path, htmlId) := state.externalTags[id]? then
- some <| path.link htmlId.toString
- else none
-
--- TODO upstream
-/--
-Return an arbitrary ID assigned to the object (or `none` if there are none).
--/
-defmethod Object.getId (obj : Object) : Option InternalId := do
- for i in obj.ids do return i
- failure
-
-def fieldLink (xref : Genre.Manual.TraverseState) (inTable fieldName : Name) : Option String := do
- let obj ← xref.getDomainObject? tomlFieldDomain s!"{inTable} {fieldName}"
- let (path, htmlId) ← xref.externalTags[← obj.getId]?
- return path.link htmlId.toString
-
-def tableLink (xref : Genre.Manual.TraverseState) (table : Name) : Option String := do
- let obj ← xref.getDomainObject? tomlTableDomain table.toString
- let (path, htmlId) ← xref.externalTags[← obj.getId]?
- return path.link htmlId.toString
-
-open Lean.Parser in
-def tomlContent (str : StrLit) : DocElabM Toml.Highlighted := do
- let scope : Command.Scope := {header := ""}
- let inputCtx := Parser.mkInputContext (← parserInputString str) (← getFileName)
- let pmctx : Parser.ParserModuleContext :=
- { env := ← getEnv, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
- let pos := str.raw.getPos? |>.getD 0
-
- let p := andthenFn whitespace Lake.Toml.toml.fn
- let s := p.run inputCtx pmctx (getTokenTable pmctx.env) { cache := initCacheForInput inputCtx.input, pos }
- match s.errorMsg with
- | some err =>
- throwErrorAt str "Couldn't parse TOML: {err}"
- | none =>
- let #[stx] := s.stxStack.toSubarray.toArray
- | throwErrorAt str s!"Internal error parsing TOML - expected one result, got {s.stxStack.toSubarray.toArray}"
- return Toml.highlightToml stx |>.run' none |>.normalize
-
-def tomlCSS : String := r#"
-.toml {
- font-family: var(--verso-code-font-family);
-}
-
-pre.toml {
- margin: 0.5rem .75rem;
- padding: 0.1rem 0;
-}
-
-.toml .bool, .toml .table-header {
- font-weight: 600;
-}
-
-.toml .table-header .key {
- color: #3030c0;
-}
-
-.toml .bool {
- color: #107090;
-}
-
-.toml .string {
- color: #0a5020;
-}
-
-.toml a, .toml a:link {
- color: inherit;
- text-decoration: none;
- border-bottom: 1px dotted #a2a2a2;
-}
-
-.toml a:hover {
- border-bottom-style: solid;
-}
-"#
-
-open Lean.Parser in
-@[code_block_expander toml]
-def toml : CodeBlockExpander
- | args, str => do
- ArgParse.done.run args
- let hl ← tomlContent str
- pure #[← ``(Block.other (Block.toml $(quote hl)) #[Block.code $(quote str.getString)])]
-
-open Lean.Parser in
-@[role_expander toml]
-def tomlInline : RoleExpander
- | args, inlines => do
- ArgParse.done.run args
-
- let #[arg] := inlines
- | throwError "Expected exactly one argument"
- let `(inline|code( $str:str )) := arg
- | throwErrorAt arg "Expected code literal with TOML code"
-
- let hl ← tomlContent str
-
- pure #[← ``(Inline.other (Inline.toml $(quote hl)) #[Inline.code $(quote str.getString)])]
-
-
-@[block_extension Block.toml]
-def Block.toml.descr : BlockDescr where
- traverse _ _ _ := pure none
-
- toTeX := none
-
- extraCss := [tomlCSS]
-
- toHtml := some <| fun _goI _ _ info _ =>
- open Verso.Doc.Html in
- open Verso.Output Html in do
- let .ok hl := FromJson.fromJson? (α := Toml.Highlighted) info
- | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize highlighted TOML data"; pure .empty
-
- let xref := (← read).traverseState
-
- return {{
-
- {{hl.toHtml (tableLink xref) (fieldLink xref)}}
-
- }}
-
-@[inline_extension Inline.toml]
-def Inline.toml.descr : InlineDescr where
- traverse _ _ _ := pure none
-
- toTeX := none
+ return #[← `(Block.concat (Toml.Table.toBlock $(quote arrayKey) #[$(docsStx),* , $userContents,*] $tableStx))]
- extraCss := [tomlCSS]
-
- toHtml := some <| fun _ _ info _ =>
- open Verso.Doc.Html in
- open Verso.Output Html in do
- let .ok hl := FromJson.fromJson? (α := Toml.Highlighted) info
- | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize highlighted TOML data"; pure .empty
-
- let xref := (← read).traverseState
-
- return {{
-
- {{hl.toHtml (tableLink xref) (fieldLink xref)}}
-
- }}
namespace Toml
diff --git a/Manual/Meta/LakeToml/Toml.lean b/Manual/Meta/LakeToml/Toml.lean
new file mode 100644
index 00000000..ac6605f3
--- /dev/null
+++ b/Manual/Meta/LakeToml/Toml.lean
@@ -0,0 +1,509 @@
+/-
+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
+import Verso.Doc.ArgParse
+import Verso.Doc.Elab.Monad
+import VersoManual
+import Verso.Code
+
+import Manual.Meta.Basic
+
+import Lake
+import Lake.Toml.Decode
+import Lake.Load.Toml
+
+open Lean Elab
+open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
+open SubVerso.Highlighting Highlighted
+
+open Lean.Elab.Tactic.GuardMsgs
+
+namespace Manual
+
+def tomlFieldDomain := `Manual.lakeTomlField
+def tomlTableDomain := `Manual.lakeTomlTable
+
+namespace Toml
+
+namespace Highlighted
+
+inductive Token where
+ | string : String → Token
+ | bool : Bool → Token
+ | num : Nat → Token -- TODO other kinds of number?
+deriving DecidableEq, Repr, Ord, ToJson, FromJson
+
+open Lean.Syntax in
+open Token in
+instance : Quote Token where
+ quote
+ | .string s => mkCApp ``string #[quote s]
+ | .bool b => mkCApp ``Token.bool #[quote b]
+ | .num n => mkCApp ``num #[quote n]
+
+end Highlighted
+
+inductive Highlighted where
+ | token : Highlighted.Token → String → Highlighted
+ | key (fullPath : Option String) : Highlighted → Highlighted
+ | text : String → Highlighted
+ | /-- Whitespace from leading/trailing source info -/
+ ws : String → Highlighted
+ | link (url : String) : Highlighted → Highlighted
+ | concat : Array Highlighted → Highlighted
+ | tableHeader : Highlighted → Highlighted
+ | tableName (name : Option String) : Highlighted → Highlighted
+ | tableDelim : Highlighted → Highlighted
+deriving Inhabited, Repr, BEq, ToJson, FromJson
+
+open Lean.Syntax in
+open Highlighted in
+partial instance : Quote Highlighted where
+ quote := q
+where
+ q
+ | .token t s => mkCApp ``Highlighted.token #[quote t, quote s]
+ | .key p s => mkCApp ``key #[quote p, q s]
+ | .text s => mkCApp ``Highlighted.text #[quote s]
+ | .ws s => mkCApp ``Highlighted.text #[quote s]
+ | .link url s => mkCApp ``Highlighted.link #[quote url, q s]
+ | .concat xs =>
+ let _ : Quote Highlighted := ⟨q⟩
+ mkCApp ``Highlighted.concat #[quote xs]
+ | .tableHeader hl => mkCApp ``Highlighted.tableHeader #[q hl]
+ | .tableName n hl => mkCApp ``Highlighted.tableName #[quote n, q hl]
+ | .tableDelim hl => mkCApp ``Highlighted.tableDelim #[q hl]
+
+instance : Append Highlighted where
+ append
+ | .concat xs, .concat ys => .concat (xs ++ ys)
+ | .concat xs, y => .concat (xs.push y)
+ | x, .concat ys => .concat (#[x] ++ ys)
+ | x, y => .concat (#[x] ++ [y])
+
+instance : Coe (Array Highlighted) Highlighted where
+ coe := .concat
+
+def srcInfoHl : SourceInfo → Highlighted → Highlighted
+ | .original leading _ trailing _, hl =>
+ mkWs leading.toString ++ #[hl] ++ mkWs trailing.toString
+ | _, hl => hl
+where
+ mkWs : String → Array Highlighted
+ | "" => #[]
+ | w => #[.ws w]
+
+private def takeDropWhile (xs : Array α) (p : α → Bool) : Array α × Array α := Id.run do
+ for h : i in [0:xs.size] do
+ if !p xs[i] then
+ return (xs.extract 0 i, xs.extract i xs.size)
+ (xs, #[])
+
+private def takeDropWhileRev (xs : Array α) (p : α → Bool) : Array α × Array α := Id.run do
+ for h : i in [0:xs.size] do
+ have : i < xs.size := by get_elem_tactic
+ let j := xs.size - (i + 1)
+ if !p xs[j] then
+ return (xs.extract 0 (j + 1), xs.extract (j + 1) xs.size)
+ (#[], xs)
+
+
+/-- info: (#[], #[1, 2, 3, 4, 5]) -/
+#guard_msgs in
+#eval takeDropWhile #[1,2,3,4,5] (· > 3)
+
+/-- info: (#[1, 2], #[3, 4, 5]) -/
+#guard_msgs in
+#eval takeDropWhile #[1,2,3,4,5] (· < 3)
+
+/-- info: (#[1, 2, 3], #[4, 5]) -/
+#guard_msgs in
+#eval takeDropWhileRev #[1,2,3,4,5] (· > 3)
+
+/-- info: (#[1, 2, 3, 4, 5], #[]) -/
+#guard_msgs in
+#eval takeDropWhileRev #[1,2,3,4,5] (· < 3)
+
+/--
+Normalizes semantic info such that it doesn't have leading or trailing whitespace.
+-/
+partial def Highlighted.normalize : Highlighted → Highlighted
+ | .concat xs => .concat (normArray (xs.map Highlighted.normalize))
+ | .ws x => .ws x
+ | .text x => .text x
+ | .token t x => .token t x
+ | .tableDelim x =>
+ let (pre, y, post) := splitWs (normArray #[x.normalize])
+ pre ++ .tableDelim y ++ post
+ | .tableHeader x =>
+ let (pre, y, post) := splitWs (normArray #[x.normalize])
+ pre ++ .tableHeader y ++ post
+ | .tableName n x =>
+ let (pre, y, post) := splitWs (normArray #[x.normalize])
+ pre ++ .tableName n y ++ post
+ | .key p x =>
+ let (pre, y, post) := splitWs (normArray #[x.normalize])
+ pre ++ .key p y ++ post
+ | .link d x =>
+ let (pre, y, post) := splitWs (normArray #[x.normalize])
+ pre ++ .link d y ++ post
+
+where
+ splitWs (xs : Array Highlighted) : (Array Highlighted × Array Highlighted × Array Highlighted) :=
+ let (pre, rest) := takeDropWhile xs (· matches (.ws ..))
+ let (mid, post) := takeDropWhileRev rest (· matches (.ws ..))
+ (pre, mid, post)
+ normArray (xs : Array Highlighted) :=
+ xs.flatMap fun
+ | .concat ys => normArray ys
+ | .ws "" => #[]
+ | other => #[other]
+
+-- Inefficient string matching, which is fine because URLs are assumed short here
+private def hasSubstring (haystack : String) (needle : String) : Bool := Id.run do
+ if needle.isEmpty then return true
+ if needle.length > haystack.length then return false
+ let mut iter := haystack.iter
+ let fst := needle.get 0
+ while h : iter.hasNext do
+ if iter.curr' h == fst then
+ let mut iter' := iter
+ let mut iter'' := needle.iter
+ while iter'.hasNext && iter''.hasNext do
+ if iter'.curr == iter''.curr then
+ iter' := iter'.next
+ iter'' := iter''.next
+ else break
+ if iter''.hasNext then
+ iter := iter.next
+ continue
+ else return true
+ else
+ iter := iter.next
+ continue
+ return false
+
+/-- info: true -/
+#guard_msgs in
+#eval hasSubstring "" ""
+
+/-- info: false -/
+#guard_msgs in
+#eval hasSubstring "" "a"
+
+/-- info: true -/
+#guard_msgs in
+#eval hasSubstring "bab" "a"
+
+/-- info: true -/
+#guard_msgs in
+#eval hasSubstring "bab" "ab"
+
+/-- info: false -/
+#guard_msgs in
+#eval hasSubstring "bab" "abb"
+
+/-- info: true -/
+#guard_msgs in
+#eval hasSubstring "abcdef" "ef"
+
+/-- info: true -/
+#guard_msgs in
+#eval hasSubstring "https://repohost.example.com/example2.git" "example.com"
+
+/-- info: false -/
+#guard_msgs in
+#eval hasSubstring "https://github.com/example2.git" "example.com"
+
+partial def highlightToml : Syntax → StateM (Option String) Highlighted := fun stx =>
+ match stx with
+ | .node info `null elts =>
+ srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.toml elts =>
+ srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.header elts =>
+ srcInfoHl info <$> elts.mapM highlightToml
+ | stx@(.node info ``Lake.Toml.keyval #[k, eq, v]) => do
+ let keypath := (← get).map (· ++ ".") |>.getD ""
+ let fullKey :=
+ if let `(Lake.Toml.keyval|$k = $_) := stx then
+ getKey k |>.map (keypath ++ ·)
+ else none
+ let hlK ← (.key fullKey) <$> highlightToml k
+
+ return srcInfoHl info #[hlK, (← highlightToml eq), (← highlightToml v)]
+ | .node info ``Lake.Toml.keyval elts =>
+ srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.key elts =>
+ (srcInfoHl info ∘ .key none) <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.simpleKey elts => srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.unquotedKey elts => srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.string elts =>
+ srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.basicString #[s@(.atom _ str)] =>
+ if let some str' := Lean.Syntax.decodeStrLit str then
+ if (str'.take 8 == "https://" || str'.take 7 == "http://") && !hasSubstring str' "example.com" then
+ (srcInfoHl info ∘ .link str') <$> highlightToml s
+ else
+ srcInfoHl info <$> highlightToml s
+ else
+ srcInfoHl info <$> highlightToml s
+ | .node info ``Lake.Toml.boolean elts => srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.true #[.atom _ b] =>
+ pure <| srcInfoHl info <| .token (.bool true) b
+ | .node info ``Lake.Toml.false #[.atom _ b] =>
+ pure <| srcInfoHl info <| .token (.bool false) b
+ | .node info ``Lake.Toml.arrayTable #[open1, open2, contents, close1, close2] => do
+ let n := getKey ⟨contents⟩
+ set n
+ return srcInfoHl info <| .tableHeader <|
+ .tableDelim ((← highlightToml open1) ++ (← highlightToml open2)) ++
+ (.tableName n (← highlightToml contents)) ++
+ .tableDelim ((← highlightToml close1) ++ (← highlightToml close2))
+ | .node info ``Lake.Toml.arrayTable elts =>
+ srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.decInt #[.atom _ n] => pure <| srcInfoHl info <| .token (.num n.toNat!) n
+ | .node info ``Lake.Toml.array elts => srcInfoHl info <$> elts.mapM highlightToml
+ | .node info ``Lake.Toml.inlineTable elts => do
+ let x ← get
+ set (none : Option String)
+ let out ← srcInfoHl info <$> elts.mapM highlightToml
+ set x
+ return out
+ | .atom info str => pure <| srcInfoHl info (.text str)
+ | other => panic! s!"Failed to highlight TOML (probably highlightToml in Manual.Meta.LakeToml needs another pattern case): {toString other}"
+
+where
+ getKey : TSyntax `Lake.Toml.key → Option String
+ | `(Lake.Toml.key| $d:unquotedKey) =>
+ d.raw.isLit? ``Lake.Toml.unquotedKey
+ | `(Lake.Toml.key| $d:literalString) =>
+ d.raw.isLit? ``Lake.Toml.literalString
+ | `(Lake.Toml.key| $d:basicString) =>
+ d.raw.isLit? ``Lake.Toml.basicString
+ | _ => none
+
+/--
+A mapping from paths into the nested tables of the config file to the datatypes at which the field
+documentation can be found.
+-/
+def configPaths : Std.HashMap (List String) Name := Std.HashMap.ofList [
+ (["require"], ``Lake.Dependency),
+ (["lean_lib"], ``Lake.LeanLibConfig),
+ (["lean_exe"], ``Lake.LeanExeConfig),
+]
+
+open Verso Output Html in
+partial def Highlighted.toHtml (tableLink : Name → Option String) (keyLink : Name → Name → Option String) : Highlighted -> Html
+ | .token t s =>
+ match t with
+ | .bool _ => {{{{s}}}}
+ | .string _ => {{{{s}}}}
+ | .num _ => {{{{s}}}}
+ | .tableHeader hl =>
+ {{}}
+ | .tableName n hl =>
+ let tableName := n.map (·.splitOn ".") >>= (configPaths[·]?)
+ if let some dest := tableName >>= tableLink then
+ {{{{hl.toHtml tableLink keyLink}}}}
+ else
+ hl.toHtml tableLink keyLink
+ | .tableDelim hl => {{{{hl.toHtml tableLink keyLink}}}}
+ | .concat hls => .seq (hls.map (toHtml tableLink keyLink))
+ | .link url hl => {{{{hl.toHtml tableLink keyLink}}}}
+ | .text s => s
+ | .ws s =>
+ let comment := s.find (· == '#')
+ let commentStr := s.extract comment s.endPos
+ let commentHtml := if commentStr.isEmpty then .empty else {{}}
+ {{ {{s.extract 0 comment}} {{commentHtml}} }}
+ | .key none k => {{
+
+ {{k.toHtml tableLink keyLink}}
+
+ }}
+ | .key (some p) k =>
+ let path := p.splitOn "."
+ let dest :=
+ if let (table, [k]) := path.splitAt (path.length - 1) then
+ if let some t := configPaths[table]? then
+ keyLink t k.toName
+ else none
+ else none
+
+ {{
+ {{ if let some url := dest then {{
+ {{k.toHtml tableLink keyLink}}
+ }} else k.toHtml tableLink keyLink }}
+
+ }}
+
+
+
+end Toml
+
+def Block.toml (highlighted : Toml.Highlighted) : Block where
+ name := `Manual.Block.toml
+ data := toJson highlighted
+
+def Inline.toml (highlighted : Toml.Highlighted) : Inline where
+ name := `Manual.Inline.toml
+ data := toJson highlighted
+
+
+open Verso.Output Html in
+def htmlLink (state : TraverseState) (id : InternalId) (html : Html) : Html :=
+ if let some (path, htmlId) := state.externalTags[id]? then
+ {{{{html}}}}
+ else html
+
+open Verso.Output Html in
+def htmlDest (state : TraverseState) (id : InternalId) : Option String :=
+ if let some (path, htmlId) := state.externalTags[id]? then
+ some <| path.link htmlId.toString
+ else none
+
+-- TODO upstream
+/--
+Return an arbitrary ID assigned to the object (or `none` if there are none).
+-/
+defmethod Object.getId (obj : Object) : Option InternalId := do
+ for i in obj.ids do return i
+ failure
+
+def Toml.fieldLink (xref : Genre.Manual.TraverseState) (inTable fieldName : Name) : Option String := do
+ let obj ← xref.getDomainObject? tomlFieldDomain s!"{inTable} {fieldName}"
+ let (path, htmlId) ← xref.externalTags[← obj.getId]?
+ return path.link htmlId.toString
+
+def Toml.tableLink (xref : Genre.Manual.TraverseState) (table : Name) : Option String := do
+ let obj ← xref.getDomainObject? tomlTableDomain table.toString
+ let (path, htmlId) ← xref.externalTags[← obj.getId]?
+ return path.link htmlId.toString
+
+open Lean.Parser in
+def tomlContent (str : StrLit) : DocElabM Toml.Highlighted := do
+ let scope : Command.Scope := {header := ""}
+ let inputCtx := Parser.mkInputContext (← parserInputString str) (← getFileName)
+ let pmctx : Parser.ParserModuleContext :=
+ { env := ← getEnv, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
+ let pos := str.raw.getPos? |>.getD 0
+
+ let p := andthenFn whitespace Lake.Toml.toml.fn
+ let s := p.run inputCtx pmctx (getTokenTable pmctx.env) { cache := initCacheForInput inputCtx.input, pos }
+ match s.errorMsg with
+ | some err =>
+ throwErrorAt str "Couldn't parse TOML: {err}"
+ | none =>
+ let #[stx] := s.stxStack.toSubarray.toArray
+ | throwErrorAt str s!"Internal error parsing TOML - expected one result, got {s.stxStack.toSubarray.toArray}"
+ return Toml.highlightToml stx |>.run' none |>.normalize
+
+def tomlCSS : String := r#"
+.toml {
+ font-family: var(--verso-code-font-family);
+}
+
+pre.toml {
+ margin: 0.5rem .75rem;
+ padding: 0.1rem 0;
+}
+
+.toml .bool, .toml .table-header {
+ font-weight: 600;
+}
+
+.toml .table-header .key {
+ color: #3030c0;
+}
+
+.toml .bool {
+ color: #107090;
+}
+
+.toml .string {
+ color: #0a5020;
+}
+
+.toml a, .toml a:link {
+ color: inherit;
+ text-decoration: none;
+ border-bottom: 1px dotted #a2a2a2;
+}
+
+.toml a:hover {
+ border-bottom-style: solid;
+}
+"#
+
+open Lean.Parser in
+@[code_block_expander toml]
+def toml : CodeBlockExpander
+ | args, str => do
+ ArgParse.done.run args
+ let hl ← tomlContent str
+ pure #[← ``(Block.other (Block.toml $(quote hl)) #[Block.code $(quote str.getString)])]
+
+open Lean.Parser in
+@[role_expander toml]
+def tomlInline : RoleExpander
+ | args, inlines => do
+ ArgParse.done.run args
+
+ let #[arg] := inlines
+ | throwError "Expected exactly one argument"
+ let `(inline|code( $str:str )) := arg
+ | throwErrorAt arg "Expected code literal with TOML code"
+
+ let hl ← tomlContent str
+
+ pure #[← ``(Inline.other (Inline.toml $(quote hl)) #[Inline.code $(quote str.getString)])]
+
+
+@[block_extension Block.toml]
+def Block.toml.descr : BlockDescr where
+ traverse _ _ _ := pure none
+
+ toTeX := none
+
+ extraCss := [tomlCSS]
+
+ toHtml := some <| fun _goI _ _ info _ =>
+ open Verso.Doc.Html in
+ open Verso.Output Html in do
+ let .ok hl := FromJson.fromJson? (α := Toml.Highlighted) info
+ | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize highlighted TOML data"; pure .empty
+
+ let xref := (← read).traverseState
+
+ return {{
+
+ {{hl.toHtml (Toml.tableLink xref) (Toml.fieldLink xref)}}
+
+ }}
+
+@[inline_extension Inline.toml]
+def Inline.toml.descr : InlineDescr where
+ traverse _ _ _ := pure none
+
+ toTeX := none
+
+ extraCss := [tomlCSS]
+
+ toHtml := some <| fun _ _ info _ =>
+ open Verso.Doc.Html in
+ open Verso.Output Html in do
+ let .ok hl := FromJson.fromJson? (α := Toml.Highlighted) info
+ | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize highlighted TOML data"; pure .empty
+
+ let xref := (← read).traverseState
+
+ return {{
+
+ {{hl.toHtml (Toml.tableLink xref) (Toml.fieldLink xref)}}
+
+ }}
diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean
index e62ed012..c5b0abe4 100644
--- a/Manual/Meta/Syntax.lean
+++ b/Manual/Meta/Syntax.lean
@@ -26,10 +26,6 @@ namespace Manual
set_option guard_msgs.diff true
--- run_elab do
--- let xs := _
--- let stx ← `(command|universe $xs*)
--- dbg_trace stx
@[role_expander evalPrio]
def evalPrio : RoleExpander
@@ -252,7 +248,10 @@ def SyntaxConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEn
SyntaxConfig.mk <$> FreeSyntaxConfig.parse <*> (many (.named `alias .resolvedName false) <* .done)
inductive GrammarTag where
+ | lhs
+ | rhs
| keyword
+ | literalIdent
| nonterminal (name : Name) (docstring? : Option String)
| fromNonterminal (name : Name) (docstring? : Option String)
| error
@@ -265,7 +264,10 @@ open Lean.Syntax in
open GrammarTag in
instance : Quote GrammarTag where
quote
+ | .lhs => mkCApp ``GrammarTag.lhs #[]
+ | .rhs => mkCApp ``GrammarTag.rhs #[]
| .keyword => mkCApp ``GrammarTag.keyword #[]
+ | .literalIdent => mkCApp ``GrammarTag.literalIdent #[]
| nonterminal x d => mkCApp ``nonterminal #[quote x, quote d]
| fromNonterminal x d => mkCApp ``fromNonterminal #[quote x, quote d]
| GrammarTag.error => mkCApp ``GrammarTag.error #[]
@@ -438,14 +440,21 @@ partial def production (which : Nat) (stx : Syntax) : StateT (NameMap (Name × O
| .atom info str => infoWrap info <$> lift (tag GrammarTag.keyword str)
| .missing => lift <| tag GrammarTag.error ""
| .ident info _ x _ =>
- let d? ← findDocString? (← getEnv) x
- -- TODO render markdown
- let tok ←
- lift <| tag (.nonterminal x d?) <|
- match x with
- | .str x' "pseudo" => x'.toString
- | _ => x.toString
- return infoWrap info tok
+ -- If the identifier is the name of something that works like a syntax category, then treat it as a nonterminal
+ if x ∈ [`ident, `atom, `num] || (Lean.Parser.parserExtension.getState (← getEnv)).categories.contains x then
+ let d? ← findDocString? (← getEnv) x
+ -- TODO render markdown
+ let tok ←
+ lift <| tag (.nonterminal x d?) <|
+ match x with
+ | .str x' "pseudo" => x'.toString
+ | _ => x.toString
+ return infoWrap info tok
+ else
+ -- If it's not a syntax category, treat it as the literal identifier (e.g. `config` before `:=` in tactic configurations)
+ let tok ←
+ lift <| tag .literalIdent x.toString
+ return infoWrap info tok
| .node info k args => do
infoWrap info <$>
match k, antiquoteOf k, args with
@@ -493,6 +502,18 @@ partial def production (which : Nat) (stx : Syntax) : StateT (NameMap (Name × O
lift <| tag .comment contents
| _ => lift <| tag .comment "error extracting comment..."
+ | ``FreeSyntax.identItem, _, _ => do
+ let cat := stx[0]
+ if let .ident info' _ c _ := cat then
+ let d? ← findDocString? (← getEnv) c
+ -- TODO render markdown
+ let tok ←
+ lift <| tag (.nonterminal c d?) <|
+ match c with
+ | .str c' "pseudo" => c'.toString
+ | _ => c.toString
+ return infoWrap info <| infoWrap info' tok
+ return "_" ++ (← lift <| tag .bnf ":") ++ (← production which cat)
| ``FreeSyntax.namedIdentItem, _, _ => do
let name := stx[0]
let cat := stx[2]
@@ -562,7 +583,7 @@ def getBnf (config : FreeSyntaxConfig) (isFirst : Bool) (stxs : List Syntax) : D
let hd := indentIfNotOpen config.open (← renderProd config isFirst 0 p)
let tl ← ps.enum.mapM fun (i, s) => renderProd config false i s
pure <| hd :: tl
- pure <| lhs ++ Format.nest 4 (.join (prods.map (.line ++ ·)))
+ pure <| lhs ++ (← tag .rhs (Format.nest 4 (.join (prods.map (.line ++ ·)))))
return bnf.render (w := 5)
where
indentIfNotOpen (isOpen : Bool) (f : Format) : Format :=
@@ -574,7 +595,7 @@ where
let mut bnf : Format := (← tag (.nonterminal cat d?) s!"{nonTerm cat}") ++ " " ++ (← tag .bnf "::=")
if config.open || (!config.open && !isFirst) then
bnf := bnf ++ (" ..." : Format)
- return bnf
+ tag .lhs bnf
renderProd (config : FreeSyntaxConfig) (isFirst : Bool) (which : Nat) (stx : Syntax) : TagFormatT GrammarTag DocElabM Format := do
let stx := removeTrailing stx
@@ -665,6 +686,166 @@ def withOpenedNamespace (ns : Name) (act : DocElabM α) : DocElabM α :=
finally
popScope
+inductive SearchableTag where
+ | meta
+ | keyword
+ | literalIdent
+ | ws
+deriving DecidableEq, Ord, Repr
+
+open Lean.Syntax in
+instance : Quote SearchableTag where
+ quote
+ | .meta => mkCApp ``SearchableTag.meta #[]
+ | .keyword => mkCApp ``SearchableTag.keyword #[]
+ | .literalIdent => mkCApp ``SearchableTag.literalIdent #[]
+ | .ws => mkCApp ``SearchableTag.ws #[]
+
+def SearchableTag.toKey : SearchableTag → String
+ | .meta => "meta"
+ | .keyword => "keyword"
+ | .literalIdent => "literalIdent"
+ | .ws => "ws"
+
+def SearchableTag.toJson : SearchableTag → Json := Json.str ∘ SearchableTag.toKey
+
+instance : ToJson SearchableTag where
+ toJson := SearchableTag.toJson
+
+def SearchableTag.fromJson? : Json → Except String SearchableTag
+ | .str "meta" => pure .meta
+ | .str "keyword" => pure .keyword
+ | .str "literalIdent" => pure .literalIdent
+ | .str "ws" => pure .ws
+ | other =>
+ let s :=
+ match other with
+ | .str s => s.quote
+ | .arr .. => "array"
+ | .obj .. => "object"
+ | .num .. => "number"
+ | .bool b => toString b
+ | .null => "null"
+ throw s!"Expected 'meta', 'keyword', 'literalIdent', or 'ws', got {s}"
+
+instance : FromJson SearchableTag where
+ fromJson? := SearchableTag.fromJson?
+
+
+def searchableJson (ss : Array (SearchableTag × String)) : Json :=
+ .arr <| ss.map fun (tag, str) =>
+ json%{"kind": $tag.toKey, "string": $str}
+
+partial def searchable (cat : Name) (txt : TaggedText GrammarTag) : Array (SearchableTag × String) :=
+ (go txt *> get).run' #[] |> fixup
+where
+ dots : SearchableTag × String := (.meta, "…")
+ go : TaggedText GrammarTag → StateM (Array (SearchableTag × String)) String
+ | .text s => do
+ ws s
+ pure s
+ | .append xs => do
+ for ⟨x, _⟩ in xs.attach do
+ discard <| go x
+ pure ""
+ | .tag .keyword x => do
+ let x' ← go x
+ modify (·.push (.keyword, x'))
+ pure x'
+ | .tag .lhs _ => pure ""
+ | .tag (.nonterminal (.str (.str .anonymous "token") _) _) (.text txt) => do
+ let txt := txt.trim
+ modify (·.push (.keyword, txt))
+ pure txt
+ | .tag (.nonterminal ``Lean.Parser.Attr.simple ..) txt => do
+ let kw := txt.stripTags.trim
+ modify (·.push (.keyword, kw))
+ pure kw
+ | .tag (.nonterminal ..) _ => do
+ ellipsis
+ pure dots.2
+ | .tag .literalIdent (.text s) => do
+ modify (·.push (.literalIdent, s))
+ return s
+ | .tag .bnf (.text s) => do
+ let s := s.trim
+ modify fun st => Id.run do
+ match s with
+ -- Suppress leading |
+ | "|" => if st.isEmpty then return st
+ -- Don't add repetition modifiers after ... or to an empty output
+ | "*" | "?" | ",*" =>
+ if let some _ := suffixMatches #[(· == dots)] st then return st
+ if st.isEmpty then return st
+ -- Don't parenthesize just "..."
+ | ")" | ")?" | ")*" =>
+ if let some st' := suffixMatches #[(· == (.meta, "(")) , (· == dots)] st then return st'.push dots
+ | _ => pure ()
+ return st.push (.meta, s)
+ pure s
+ | .tag other txt => do
+ go txt
+ fixup (s : Array (SearchableTag × String)) : Array (SearchableTag × String) :=
+ let s := s.popWhile (·.1 == .ws) -- Remove trailing whitespace
+ match cat with
+ | `command => Id.run do
+ -- Drop leading ellipses from commands
+ for h : i in [0:s.size] do
+ if s[i] ∉ [dots, (.meta, "?"), (.ws, " ")] then return s.extract i s.size
+ return s
+ | _ => s
+ ws (s : String) : StateM (Array (SearchableTag × String)) Unit := do
+ if !s.isEmpty && s.all (·.isWhitespace) then
+ modify fun st =>
+ if st.isEmpty then st
+ else if st.back?.map (·.1 == .ws) |>.getD true then st
+ else st.push (.ws, " ")
+
+ suffixMatches (suffix : Array (SearchableTag × String → Bool)) (st : (Array (SearchableTag × String))) : Option (Array (SearchableTag × String)) := do
+ let mut suffix := suffix
+ for h : i in [0 : st.size] do
+ match suffix.back? with
+ | none => return st.extract 0 (st.size - i)
+ | some p =>
+ have : st.size > 0 := by
+ let ⟨_, h, _⟩ := h
+ simp_all +zetaDelta
+ omega
+ let curr := st[st.size - (i + 1)]
+ if curr.1 matches .ws then continue
+ if p curr then
+ suffix := suffix.pop
+ else throw ()
+ if suffix.isEmpty then some #[] else none
+
+ ellipsis : StateM (Array (SearchableTag × String)) Unit := do
+ modify fun st =>
+ -- Don't push ellipsis onto ellipsis
+ if let some _ := suffixMatches #[(· == dots)] st then st
+ -- Don't alternate ellipses
+ else if let some st' := suffixMatches #[(· == dots), (· == (.meta, "|"))] st then st'.push dots
+ else st.push dots
+
+
+/-- info: some #[] -/
+#guard_msgs in
+#eval searchable.suffixMatches #[] #[]
+
+/-- info: some #[(Manual.SearchableTag.keyword, "aaa")] -/
+#guard_msgs in
+#eval searchable.suffixMatches #[(· == (.meta, "(")), (· == searchable.dots)] #[(.keyword, "aaa"),(.meta, "("), (.ws, " "),(.meta, "…")]
+
+/-- info: some #[(Manual.SearchableTag.keyword, "aaa")] -/
+#guard_msgs in
+#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.keyword, "aaa"),(.meta, "…"), (.ws, " ")]
+
+/-- info: some #[] -/
+#guard_msgs in
+#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.meta, "…"), (.ws, " ")]
+
+/-- info: some #[] -/
+#guard_msgs in
+#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.meta, "…")]
open Manual.Meta.PPrint Grammar in
/--
@@ -712,9 +893,13 @@ where
| .ok stx =>
Doc.PointOfInterest.save stx stx.getKind.toString
let bnf ← getBnf config.toFreeSyntaxConfig isFirst [FreeSyntax.decode stx]
- Hover.addCustomHover nameStx s!"Kind: {stx.getKind}\n\n````````\n{bnf.stripTags}\n````````"
+ let searchTarget := searchable config.name bnf
+
+ Hover.addCustomHover nameStx s!"Kind: {stx.getKind}\n\n````````\n{bnf.stripTags}````````"
+
- `(Block.other {Block.grammar with data := ToJson.toJson (($(quote stx.getKind), $(quote bnf)) : Name × TaggedText GrammarTag)} #[])
+ let blockStx ← `(Block.other {Block.grammar with data := ToJson.toJson (($(quote stx.getKind), $(quote bnf), searchableJson $(quote searchTarget)) : Name × TaggedText GrammarTag × Json)} #[])
+ pure (blockStx)
| .error es =>
for (pos, msg) in es do
log (severity := .error) (mkErrorStringWithPos "" pos msg)
@@ -767,7 +952,8 @@ where
| .ok stx =>
let bnf ← getBnf config isFirst (FreeSyntax.decodeMany stx |>.map FreeSyntax.decode)
Hover.addCustomHover nameStx s!"Kind: {stx.getKind}\n\n````````\n{bnf.stripTags}\n````````"
- `(Block.other {Block.grammar with data := ToJson.toJson (($(quote stx.getKind), $(quote bnf)) : Name × TaggedText GrammarTag)} #[])
+ -- TODO: searchable instead of Json.arr #[]
+ `(Block.other {Block.grammar with data := ToJson.toJson (($(quote stx.getKind), $(quote bnf), Json.arr #[]) : Name × TaggedText GrammarTag × Json)} #[])
| .error es =>
for (pos, msg) in es do
log (severity := .error) (mkErrorStringWithPos "" pos msg)
@@ -778,9 +964,6 @@ where
def syntax.descr : BlockDescr where
traverse id data contents := do
if let .ok (title, kind, label, tag, aliases) := FromJson.fromJson? (α := Option String × Name × String × Option Tag × Array Name) data then
- modify fun st => st.saveDomainObject syntaxKindDomain kind.toString id
- for a in aliases do
- modify fun st => st.saveDomainObject syntaxKindDomain a.toString id
if tag.isSome then
pure none
else
@@ -969,14 +1152,20 @@ private def lookingAt (k : Name) : GrammarHtmlM α → GrammarHtmlM α := withRe
private def notLooking : GrammarHtmlM α → GrammarHtmlM α := withReader (·.noLook)
+def productionDomain : Name := `Manual.Syntax.production
+
open Verso.Output Html in
@[block_extension grammar]
partial def grammar.descr : BlockDescr where
traverse id info _ := do
- if let .ok (k, _) := FromJson.fromJson? (α := Name × TaggedText GrammarTag) info then
+ if let .ok (k, _, searchable) := FromJson.fromJson? (α := Name × TaggedText GrammarTag × Json) info then
let path ← (·.path) <$> read
let _ ← Verso.Genre.Manual.externalTag id path k.toString
modify fun st => st.saveDomainObject syntaxKindDomain k.toString id
+
+ let prodName := s!"{k} {searchable}"
+ modify fun st => st.saveDomainObject productionDomain prodName id
+ modify fun st => st.saveDomainObjectData productionDomain prodName (json%{"category": null, "kind": $k.toString, "forms": $searchable})
else
logError "Couldn't deserialize grammar info during traversal"
pure none
@@ -984,14 +1173,14 @@ partial def grammar.descr : BlockDescr where
toHtml :=
open Verso.Output.Html in
some <| fun _goI _goB id info _ => do
- match FromJson.fromJson? (α := Name × TaggedText GrammarTag) info with
- | .ok bnf =>
+ match FromJson.fromJson? (α := Name × TaggedText GrammarTag × Json) info with
+ | .ok (kind, bnf, _searchable) =>
let t ← match (← read).traverseState.externalTags.get? id with
| some (_, t) => pure t.toString
- | _ => Html.HtmlT.logError s!"Couldn't get HTML ID for grammar of {bnf.1}" *> pure ""
+ | _ => Html.HtmlT.logError s!"Couldn't get HTML ID for grammar of {kind}" *> pure ""
pure {{
- {{← bnfHtml bnf.2 |>.run (GrammarHtmlContext.default.skip bnf.1) }}
+ {{← bnfHtml bnf |>.run (GrammarHtmlContext.default.skip kind) }}
}}
| .error e =>
@@ -1011,9 +1200,11 @@ where
tagHtml (t : GrammarTag) (go : GrammarHtmlM Html) : GrammarHtmlM Html :=
match t with
+ | .lhs | .rhs => go
| .bnf => ({{{{·}}}}) <$> notLooking go
| .comment => ({{}}) <$> notLooking go
| .error => ({{{{·}}}}) <$> notLooking go
+ | .literalIdent => ({{{{·}}}}) <$> notLooking go
| .keyword => do
let inner ← go
if let some k := (← read).lookingAt then
diff --git a/Manual/Monads/Syntax.lean b/Manual/Monads/Syntax.lean
index bbdb68e4..0a764f3a 100644
--- a/Manual/Monads/Syntax.lean
+++ b/Manual/Monads/Syntax.lean
@@ -283,7 +283,7 @@ This syntax is also translated to a use of {name}`bind`.
This indicates a pure, rather than monadic, definition:
:::syntax Lean.Parser.Term.doSeqItem
```grammar
-let v := $e:term
+let $v := $e:term
```
:::
{lean}`do let x := e; es` is translated to {lean}`let x := e; do es`.
diff --git a/Manual/Terms.lean b/Manual/Terms.lean
index 84804b5d..6238e825 100644
--- a/Manual/Terms.lean
+++ b/Manual/Terms.lean
@@ -19,6 +19,8 @@ open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
set_option linter.constructorNameAsVariable false
set_option guard_msgs.diff true
+set_option guard_msgs.diff true
+
#doc (Manual) "Terms" =>
%%%
tag := "terms"
@@ -810,11 +812,11 @@ Repeated pipelines use parsing precedence instead of nested parentheses to nest
:::syntax term (title := "Pipelines")
Right pipe notation applies the term to the right of the pipe to the one on its left.
```grammar
-e |> e
+$e |> $e
```
Left pipe notation applies the term on the left of the pipe to the one on its right.
```grammar
-e <| e
+$e <| $e
```
:::
@@ -1055,7 +1057,7 @@ else
With the name annotation, the branches of the {keywordOf termDepIfThenElse}`if` have access to a local assumption that the proposition is respectively true or false.
```grammar
-if h : $e then
+if $h : $e then
$e
else
$e
diff --git a/lake-manifest.json b/lake-manifest.json
index 23e2225d..0ae3ccb2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,32 +1,32 @@
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
- [{"url": "https://github.com/leanprover/subverso.git",
+ [{"url": "https://github.com/leanprover/verso.git",
"type": "git",
"subDir": null,
"scope": "",
- "rev": "b4dd804a58961657d6c2f24d5eb350abb4992204",
- "name": "subverso",
+ "rev": "d9c0352c9ec4f953992a1739b4c3d25b15b78702",
+ "name": "verso",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": false,
"configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover/verso.git",
+ {"url": "https://github.com/acmepjz/md4lean",
"type": "git",
"subDir": null,
"scope": "",
- "rev": "9c0d4a38c4ed8850882a057c3073e936f5495470",
- "name": "verso",
+ "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb",
+ "name": "MD4Lean",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
- "inherited": false,
+ "inherited": true,
"configFile": "lakefile.lean"},
- {"url": "https://github.com/acmepjz/md4lean",
+ {"url": "https://github.com/leanprover/subverso.git",
"type": "git",
"subDir": null,
"scope": "",
- "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb",
- "name": "MD4Lean",
+ "rev": "b4dd804a58961657d6c2f24d5eb350abb4992204",
+ "name": "subverso",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
diff --git a/lakefile.lean b/lakefile.lean
index 4739a9c8..472da612 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -8,7 +8,6 @@ open Lake DSL
open System (FilePath)
require verso from git "https://github.com/leanprover/verso.git"@"main"
-require subverso from git "https://github.com/leanprover/subverso.git"@"main"
package "verso-manual" where
-- building the C code cost much more than the optimizations save
diff --git a/static/search/README.txt b/static/search/README.txt
new file mode 100644
index 00000000..bca379fb
--- /dev/null
+++ b/static/search/README.txt
@@ -0,0 +1,59 @@
+# Search bar for LEAN
+
+To type check: `tsc -p ./jsconfig.json`.
+
+To run: `python -m http.server 8870` and go to `localhost:8870`.
+
+## 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/tonnes 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/search/domain-mappers.js b/static/search/domain-mappers.js
new file mode 100644
index 00000000..2acdd1e2
--- /dev/null
+++ b/static/search/domain-mappers.js
@@ -0,0 +1,212 @@
+/**
+ * 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
+ */
+
+/**
+ * @import {DomainMapper} from './search-box.js'
+ */
+
+/**
+ * @type {DomainMapper}
+ */
+const docDomainMapper = {
+ dataToSearchables: (domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => ({
+ searchKey: key,
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: "Verso.Genre.Manual.doc",
+ ref: value,
+ })),
+ className: "doc-domain",
+ displayName: "Documentation",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const docOptionDomainMapper = {
+ dataToSearchables: (domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => ({
+ searchKey: key,
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: "Verso.Genre.Manual.doc.option",
+ ref: value,
+ })),
+ className: "doc-option-domain",
+ displayName: "Option",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const docTacticDomainMapper = {
+ 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,
+ })),
+ className: "tactic-domain",
+ displayName: "Tactic",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const docConvTacticDomainMapper = {
+ 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.conv",
+ ref: value,
+ })),
+ className: "conv-tactic-domain",
+ displayName: "Conv Tactic",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const sectionMapper = {
+ 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,
+ })),
+ className: "section-domain",
+ displayName: "Section",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const techTermMapper = {
+ 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,
+ })),
+ className: "tech-term-domain",
+ displayName: "Terminology",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const syntaxMapper = {
+ dataToSearchables: (domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => ({
+ // TODO find a way to not include the "meta" parts of the string
+ // in the search key here, but still display them
+ searchKey: value[0].data.forms.map(v => v.string).join(''),
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: "Manual.Syntax.production",
+ ref: value,
+ })),
+ className: "syntax-domain",
+ displayName: "Syntax",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const lakeCommandMapper = {
+ dataToSearchables: (domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => ({
+ searchKey: `lake ${key}`,
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: "Manual.lakeCommand",
+ ref: value,
+ })),
+ className: "lake-command-domain",
+ displayName: "Lake Command",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const lakeOptMapper = {
+ dataToSearchables: (domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => ({
+ searchKey: key,
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: "Manual.lakeOpt",
+ ref: value,
+ })),
+ className: "lake-option-domain",
+ displayName: "Lake Command-Line Option",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const envVarMapper = {
+ dataToSearchables: (domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => ({
+ searchKey: key,
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: "Manual.envVar",
+ ref: value,
+ })),
+ className: "env-var-domain",
+ displayName: "Environment Variable",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const lakeTomlFieldMapper = {
+ dataToSearchables: (domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => {
+ let tableArrayKey = value[0].data.tableArrayKey;
+ let arr = tableArrayKey ? `[[${tableArrayKey}]]` : "package configuration";
+ return {
+ searchKey: `${value[0].data.field} in ${arr}`,
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: "Manual.lakeTomlField",
+ ref: value,
+ }}),
+ className: "lake-toml-field-domain",
+ displayName: "Lake TOML Field",
+};
+
+/**
+ * @type {DomainMapper}
+ */
+const lakeTomlTableMapper = {
+ dataToSearchables: (domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => {
+ let arrayKey = value[0].data.arrayKey;
+ let arr = arrayKey ? `[[${arrayKey}]] — ` : "";
+ return {
+ searchKey: arr + value[0].data.description,
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: "Manual.lakeTomlTable",
+ ref: value,
+ }}),
+ className: "lake-toml-table-domain",
+ displayName: "Lake TOML Table",
+};
+
+export const domainMappers = {
+ "Verso.Genre.Manual.doc": docDomainMapper,
+ "Verso.Genre.Manual.doc.option": docOptionDomainMapper,
+ "Verso.Genre.Manual.doc.tactic": docTacticDomainMapper,
+ "Verso.Genre.Manual.doc.tactic.conv": docConvTacticDomainMapper,
+ "Verso.Genre.Manual.section": sectionMapper,
+ "Verso.Genre.Manual.doc.tech": techTermMapper,
+ "Manual.Syntax.production": syntaxMapper,
+ "Manual.lakeCommand": lakeCommandMapper,
+ "Manual.lakeOpt": lakeOptMapper,
+ "Manual.envVar": envVarMapper,
+ "Manual.lakeTomlTable" : lakeTomlTableMapper,
+ "Manual.lakeTomlField" : lakeTomlFieldMapper,
+};
diff --git a/static/search/fuzzysort.d.ts b/static/search/fuzzysort.d.ts
new file mode 100644
index 00000000..7516a89e
--- /dev/null
+++ b/static/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/search/fuzzysort.js b/static/search/fuzzysort.js
new file mode 100644
index 00000000..5f61751e
--- /dev/null
+++ b/static/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/search/jsconfig.json b/static/search/jsconfig.json
new file mode 100644
index 00000000..0ba50aca
--- /dev/null
+++ b/static/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/search/licenses.md b/static/search/licenses.md
new file mode 100644
index 00000000..76bb76b9
--- /dev/null
+++ b/static/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/search/search-box.css b/static/search/search-box.css
new file mode 100644
index 00000000..be1b1f7a
--- /dev/null
+++ b/static/search/search-box.css
@@ -0,0 +1,197 @@
+/**
+ * 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: #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: 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;
+}
+
+#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.env-var-domain,
+#search-wrapper .search-result.lake-command-domain {
+ font-family: var(--verso-code-font-family);
+}
+
+#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;
+}
+
+#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 {
+ text-align: right;
+ color: #777;
+ font-style: italic;
+ font-family: var(--verso-structure-font-family);
+ font-weight: normal;
+ font-size: .7rem;
+}
+
+#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 {
+ padding: var(--verso--content-padding-x);
+ width: fit-content;
+ position: absolute;
+ top: 0;
+ right: 0;
+ z-index: 1;
+}
+
+@media screen and (700px < width <= 1400px) {
+ #search-wrapper {
+ padding-top: 0.25rem;
+ }
+}
+
+@media screen and (width <= 700px) {
+ #search-wrapper {
+ padding-top: 0.25rem;
+ padding-right: 0.5rem;
+ }
+}
diff --git a/static/search/search-box.js b/static/search/search-box.js
new file mode 100644
index 00000000..c6afa300
--- /dev/null
+++ b/static/search/search-box.js
@@ -0,0 +1,834 @@
+/**
+ * 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;
+
+/**
+ * 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 {{item: Searchable, fuzzysortResult: Fuzzysort.Result, htmlItem: HTMLLIElement}} SearchResult
+ */
+
+/**
+ * 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;
+};
+
+/**
+ * @param {SearchResult} result
+ * @returns string
+ */
+const resultToText = (result) => result.fuzzysortResult.target;
+
+/**
+ * @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
+ );
+
+ 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.filterOptions();
+
+ // 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 {SearchResult} result
+ */
+ confirmResult(result) {
+ window.location.assign(result.item.address);
+ }
+
+ /**
+ * @param {string} value
+ */
+ setValue(value) {
+ this.filter = value;
+ this.comboboxNode.textContent = this.filter;
+ this.imeRewriter.setSelections([new Range(this.filter.length, 0)]);
+ this.filterOptions();
+ }
+
+ /**
+ * @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;
+ }
+
+ const results = fuzzysort.go(filter, this.preparedData, {
+ limit: 30,
+ threshold: 0.25,
+ });
+
+ if (results.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;
+
+ for (let i = 0; i < results.length; i++) {
+ const result = results[i];
+ 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
+ );
+ /** @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 === results.length - 1 && j === dataItems.length - 1) {
+ this.lastOption = searchResult;
+ }
+ if (currentOptionText === resultToText(searchResult)) {
+ newCurrentOption = searchResult;
+ }
+ }
+ }
+
+ const moreResults = document.createElement("li");
+ moreResults.textContent = `Showing ${results.length}/${results.total} results`;
+ moreResults.className = `more-results`;
+ this.listboxNode.appendChild(moreResults);
+
+ if (newCurrentOption) {
+ this.currentOption = newCurrentOption;
+ }
+
+ 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) {
+ this.confirmResult(this.currentOption);
+ }
+ }
+ 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);
+ this.confirmResult(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/search/search-init.js b/static/search/search-init.js
new file mode 100644
index 00000000..57ec2ea7
--- /dev/null
+++ b/static/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("main");
+ main.insertAdjacentHTML("afterbegin", searchHTML);
+ const searchWrapper = document.querySelector(".combobox-list");
+ data.then((data) => {
+ registerSearch({searchWrapper, data, domainMappers});
+ });
+});
diff --git a/static/search/unicode-input-component.min.js b/static/search/unicode-input-component.min.js
new file mode 100644
index 00000000..4124f3b1
--- /dev/null
+++ b/static/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/search/unicode-input.min.js b/static/search/unicode-input.min.js
new file mode 100644
index 00000000..397ffd95
--- /dev/null
+++ b/static/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};