From a5009dfae6f450cf0e4029616fe3e3cbb7f097b6 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 10 Jan 2025 12:42:07 +0100 Subject: [PATCH 01/37] feat: experimental search box integration --- Main.lean | 26 +- lake-manifest.json | 4 +- lakefile.lean | 2 +- static/search/README.txt | 0 static/search/domain-mappers.js | 70 ++ static/search/fuzzysort.js | 2 + static/search/search-box.css | 128 ++++ static/search/search-box.js | 932 +++++++++++++++++++++++ static/search/search-init.js | 35 + static/search/unicode-input-component.js | 342 +++++++++ static/search/unicode-input.min.js | 1 + static/search/w3-license.md | 11 + 12 files changed, 1548 insertions(+), 5 deletions(-) create mode 100644 static/search/README.txt create mode 100644 static/search/domain-mappers.js create mode 100644 static/search/fuzzysort.js create mode 100644 static/search/search-box.css create mode 100644 static/search/search-box.js create mode 100644 static/search/search-init.js create mode 100644 static/search/unicode-input-component.js create mode 100644 static/search/unicode-input.min.js create mode 100644 static/search/w3-license.md diff --git a/Main.lean b/Main.lean index 7f1ec3aa..c1943671 100644 --- a/Main.lean +++ b/Main.lean @@ -9,14 +9,36 @@ import VersoManual open Verso.Genre.Manual +open Verso.Output.Html in +def searchModule := {{ + + }} + def main := manualMain (%doc Manual) (config := config) where config := { 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", + "/static/katex/katex.min.css" + ], + extraJs := [ + -- Search box + "/static/search/fuzzysort.js", + -- KaTeX + "/static/katex/katex.min.js", + "/static/math.js", + -- Print stylesheet improvements + "/static/print.js" + ], + extraHead := #[searchModule], emitTeX := false, emitHtmlSingle := true, -- for proofreading logo := some "/static/lean_logo.svg", diff --git a/lake-manifest.json b/lake-manifest.json index 889f587e..e22fca47 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7e93d5b3dd3d083e7824a7559cd8a8dec49265bc", + "rev": "b1484a6fe948b6a407e3d6f30b9aa073877b6954", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "custom-head", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/david-christiansen/md4lean", diff --git a/lakefile.lean b/lakefile.lean index 4739a9c8..5fd2cfb5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,7 @@ import Lake open Lake DSL open System (FilePath) -require verso from git "https://github.com/leanprover/verso.git"@"main" +require verso from git "https://github.com/leanprover/verso.git"@"custom-head" require subverso from git "https://github.com/leanprover/subverso.git"@"main" package "verso-manual" where diff --git a/static/search/README.txt b/static/search/README.txt new file mode 100644 index 00000000..e69de29b diff --git a/static/search/domain-mappers.js b/static/search/domain-mappers.js new file mode 100644 index 00000000..b9a6348b --- /dev/null +++ b/static/search/domain-mappers.js @@ -0,0 +1,70 @@ +/** + * @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: key, + address: `${value[0].address}#${value[0].id}`, + domainId: "Verso.Genre.Manual.doc.tactic", + ref: value, + })), + className: "doc-tactic-domain", + displayName: "Tactic", +}; + +/** + * @type {DomainMapper} + */ +const sectionMapper = { + dataToSearchables: (domainData) => + Object.entries(domainData.contents).map(([key, value]) => ({ + searchKey: value[0].data[value[0].data.length - 1], + address: `${value[0].address}#${value[0].id}`, + domainId: "Verso.Genre.Manual.section", + ref: value, + })), + className: "section-domain", + displayName: "Section", +}; + +export const domainMappers = { + "Verso.Genre.Manual.doc": docDomainMapper, + "Verso.Genre.Manual.doc.option": docOptionDomainMapper, + "Verso.Genre.Manual.doc.tactic": docTacticDomainMapper, + "Verso.Genre.Manual.section": sectionMapper, +}; 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/search-box.css b/static/search/search-box.css new file mode 100644 index 00000000..d91b7067 --- /dev/null +++ b/static/search/search-box.css @@ -0,0 +1,128 @@ +:root { + --selected-color: #def; +} + +#search-wrapper { + align-self: flex-end; +} + +#search-wrapper .combobox-list { + position: relative; +} + +#search-wrapper .combobox .group { + display: inline-flex; + cursor: pointer; +} + +#search-wrapper .combobox input { + 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; +} + +#search-wrapper .combobox input { + width: 16rem; + outline: none; + font-size: .9rem; + padding: .3rem .5rem; +} + +#search-wrapper .combobox .group.focus input, +#search-wrapper .combobox .group input:hover { + background-color: var(--selected-color); + outline: auto; +} + +#search-wrapper ul[role="listbox"] { + margin: 0; + padding: 0; + position: absolute; + top: calc(100%); + width: 16rem; + 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; + cursor: pointer; + z-index: 100; +} + +#search-wrapper .search-result { + margin: 0; + padding: .2rem; + + display: flex; + flex-direction: column; + gap: .2rem; + + font-family: sans-serif; + font-weight: 400; +} + +#search-wrapper .search-result.doc-domain, #search-wrapper .search-result.option-domain { + font-family: var(--verso-code-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 [role="listbox"] li: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 .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; + float: right; +} diff --git a/static/search/search-box.js b/static/search/search-box.js new file mode 100644 index 00000000..74326ea8 --- /dev/null +++ b/static/search/search-box.js @@ -0,0 +1,932 @@ +// Enable typescript +// @ts-check + +import { InputAbbreviationRewriter } from "./unicode-input-component.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[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/ + * + * More documentation to come! + */ +class SearchBox { + /** + * @type {HTMLInputElement} + */ + comboboxNode; + + /** + * @type {HTMLButtonElement | null} + */ + buttonNode; + + /** + * @type {HTMLElement} + */ + listboxNode; + + /** + * @type {boolean} + */ + comboboxHasVisualFocus; + + /** + * @type {boolean} + */ + listboxHasVisualFocus; + + /** + * @type {boolean} + */ + hasHover; + + /** + * @type {boolean} + */ + isNone; + + /** + * @type {boolean} + */ + isList; + + /** + * @type {boolean} + */ + isBoth; + + /** + * @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; + + /** + * @param {HTMLInputElement} 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 + new InputAbbreviationRewriter( + { + abbreviationCharacter: "\\", + customTranslations: [], + eagerReplacementEnabled: true, + }, + comboboxNode + ); + + this.comboboxHasVisualFocus = false; + this.listboxHasVisualFocus = false; + + this.hasHover = false; + + this.isNone = false; + this.isList = false; + this.isBoth = false; + + this.currentOption = null; + this.firstOption = null; + this.lastOption = null; + + this.filteredOptions = []; + this.filter = ""; + + const autocomplete = this.comboboxNode + .getAttribute("aria-autocomplete") + ?.toLowerCase(); + + if (typeof autocomplete === "string") { + this.isNone = autocomplete === "none"; + this.isList = autocomplete === "list"; + this.isBoth = autocomplete === "both"; + } else { + // default value of autocomplete + this.isNone = true; + } + + 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 {Element} element + */ + isElementInView(element) { + const bounding = element.getBoundingClientRect(); + return ( + bounding.top >= 0 && + bounding.left >= 0 && + bounding.bottom <= + (window.innerHeight || document.documentElement.clientHeight) && + bounding.right <= + (window.innerWidth || document.documentElement.clientWidth) + ); + } + + /** + * @param {HTMLLIElement | null | undefined} option + */ + setActiveDescendant(option) { + if (option && this.listboxHasVisualFocus) { + this.comboboxNode.setAttribute("aria-activedescendant", option.id); + if (!this.isElementInView(option)) { + option.scrollIntoView({ behavior: "smooth", 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.value = this.filter; + this.comboboxNode.setSelectionRange(this.filter.length, this.filter.length); + this.filterOptions(); + } + + /** + * @param {SearchResult} option + * @param {boolean} [setSelection] + */ + setOption(option, setSelection) { + if (option) { + this.currentOption = option; + this.setCurrentOptionStyle(this.currentOption); + this.setActiveDescendant(this.currentOption.htmlItem); + + if (this.isBoth) { + this.comboboxNode.value = resultToText(this.currentOption); + if (setSelection) { + this.comboboxNode.setSelectionRange( + resultToText(this.currentOption).length, + resultToText(this.currentOption).length + ); + } else { + this.comboboxNode.setSelectionRange( + this.filter.length, + resultToText(this.currentOption).length + ); + } + } + } + } + + 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() { + // do not filter any options if autocomplete is none + if (this.isNone) { + this.filter = ""; + } + + const currentOptionText = opt(this.currentOption, resultToText); + const filter = this.filter; + + // Empty the listbox + this.listboxNode.innerHTML = ""; + + 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: 20, + threshold: 0.5, + }); + + 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; + } + } + } + + 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.isBoth && this.filteredOptions.length > 1) + ) { + this.setOption( + this.getNextOption(this.currentOption, this.firstOption), + true + ); + this.setVisualFocusListbox(); + } else { + this.setOption(this.firstOption, true); + 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), + true + ); + } else { + this.open(); + if (!altKey) { + this.setOption(this.lastOption, true); + this.setVisualFocusListbox(); + } + } + } + eventHandled = true; + break; + + case "Esc": + case "Escape": + if (this.isOpen()) { + this.close(true); + this.filter = this.comboboxNode.value; + this.filterOptions(); + this.setVisualFocusCombobox(); + } else { + this.setValue(""); + this.comboboxNode.value = ""; + } + this.option = null; + eventHandled = true; + break; + + case "Tab": + this.close(true); + if (this.listboxHasVisualFocus) { + if (this.currentOption) { + this.setValue(resultToText(this.currentOption)); + } + } + break; + + case "Home": + this.comboboxNode.setSelectionRange(0, 0); + eventHandled = true; + break; + + case "End": + var length = this.comboboxNode.value.length; + this.comboboxNode.setSelectionRange(length, length); + eventHandled = true; + break; + + default: + break; + } + + if (eventHandled) { + event.stopPropagation(); + event.preventDefault(); + } + } + + /** + * @param {string} str + */ + isPrintableCharacter(str) { + return str.length === 1 && str.match(/\S| /); + } + + /** + * @param {KeyboardEvent} event + * @returns void + */ + onComboboxKeyUp(event) { + let eventHandled = false; + const char = event.key; + + if (this.isPrintableCharacter(char)) { + this.filter += char; + } + + // this is for the case when a selection in the textbox has been deleted + if (this.comboboxNode.value.length < this.filter.length) { + this.filter = this.comboboxNode.value; + this.option = null; + this.filterOptions(); + } + + if (event.key === "Escape" || event.key === "Esc") { + return; + } + + switch (event.key) { + case "Backspace": + this.setVisualFocusCombobox(); + this.setCurrentOptionStyle(null); + this.filter = this.comboboxNode.value; + this.option = null; + this.filterOptions(); + eventHandled = true; + break; + + case "Left": + case "ArrowLeft": + case "Right": + case "ArrowRight": + case "Home": + case "End": + if (this.isBoth) { + this.filter = this.comboboxNode.value; + } else { + this.option = null; + this.setCurrentOptionStyle(null); + } + this.setVisualFocusCombobox(); + eventHandled = true; + break; + + default: + if (this.isPrintableCharacter(char)) { + this.setVisualFocusCombobox(); + this.setCurrentOptionStyle(null); + eventHandled = true; + + if (this.isList || this.isBoth) { + const option = this.filterOptions(); + if (option) { + if (this.isClosed() && this.comboboxNode.value.length) { + this.open(); + } + + this.option = option; + if (this.isBoth || this.isList || this.listboxHasVisualFocus) { + this.setCurrentOptionStyle(option); + if (this.isBoth || this.isList) { + this.setOption(option); + } + } + } else { + this.close(); + this.option = null; + this.setActiveDescendant(null); + } + } else if (this.comboboxNode.value.length) { + this.open(); + } + } + + break; + } + + if (eventHandled) { + event.stopPropagation(); + event.preventDefault(); + } + } + + onComboboxClick() { + if (this.isOpen()) { + this.close(true); + } else { + this.open(); + } + } + + onComboboxFocus() { + this.filter = this.comboboxNode.value; + this.filterOptions(); + this.setVisualFocusCombobox(); + this.option = null; + this.setCurrentOptionStyle(null); + } + + onComboboxBlur() { + this.removeVisualFocusAll(); + } + + /** + * @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.value = 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 = searchWrapper.querySelector("input"); + + 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..5e2b0519 --- /dev/null +++ b/static/search/search-init.js @@ -0,0 +1,35 @@ +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 +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.js b/static/search/unicode-input-component.js new file mode 100644 index 00000000..7ebb45ec --- /dev/null +++ b/static/search/unicode-input-component.js @@ -0,0 +1,342 @@ +// @ts-check + +/** + * This is copied from `https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input-component/src/index.ts` + * but modified to work without compilation, and with an input element instead of a contenteditable div. This loses the + * underlining that the original had, but allows us to keep using an input element. + */ + +import { + AbbreviationProvider, + AbbreviationRewriter, + Range, +} from "./unicode-input.min.js"; + +/** + * @typedef {any} AbbreviationConfig + * @typedef {any} SelectionMoveMode + * @typedef {any} Range + * @typedef {any} Change + */ + +/** + * @param {Node} searchNode + * @param {Node} target + * @param {number} offsetInTarget + * @returns {number | undefined} + */ +function computeTextOffsetFromNodeOffset(searchNode, target, offsetInTarget) { + if (searchNode === target) { + return offsetInTarget; + } + if (!searchNode.contains(target)) { + return undefined; + } + + let totalOffset = 0; + for (const childNode of Array.from(searchNode.childNodes)) { + const childOffset = computeTextOffsetFromNodeOffset( + childNode, + target, + offsetInTarget + ); + if (childOffset !== undefined) { + totalOffset += childOffset; + return totalOffset; + } + totalOffset += childNode.textContent?.length ?? 0; + } + return undefined; +} + +/** + * @param {Node} searchNode + * @param {{ node: Node; offset: number } | undefined} rangeStart + * @param {{ node: Node; offset: number } | undefined} rangeEnd + * @returns {Range | undefined} + */ +function computeTextRangeFromNodeRange(searchNode, rangeStart, rangeEnd) { + /** @var {number | undefined} */ + let start; + /** @var {number | undefined} */ + let end; + if (rangeStart) { + start = computeTextOffsetFromNodeOffset( + searchNode, + rangeStart.node, + rangeStart.offset + ); + } + if (rangeEnd) { + end = computeTextOffsetFromNodeOffset( + searchNode, + rangeEnd.node, + rangeEnd.offset + ); + } + + if (start === undefined) { + if (end === undefined) { + return undefined; + } else { + return new Range(end, 0); + } + } else { + if (end === undefined) { + return new Range(start, 0); + } else { + if (end < start) { + [start, end] = [end, start]; + } + return new Range(start, end - start); + } + } +} + +/** + * @param {Node} searchNode + * @returns {Range | undefined} + */ +function findTextCursorSelection(searchNode) { + const sel = window.getSelection(); + if (sel === null) { + return undefined; + } + + /** @var {{ node: Node; offset: number } | undefined} */ + let rangeStart; + if (sel.anchorNode) { + rangeStart = { node: sel.anchorNode, offset: sel.anchorOffset }; + } + /** @var {{ node: Node; offset: number } | undefined} */ + let rangeEnd; + if (sel.focusNode) { + rangeStart = { node: sel.focusNode, offset: sel.focusOffset }; + } + + return computeTextRangeFromNodeRange(searchNode, rangeStart, rangeEnd); +} + +/** + * @param {Node} searchNode + * @param {number} offset + * @returns {{ found: true; node: Node; offset: number } | { found: false; remainingOffset: number }} + */ +function computeNodeOffsetFromTextOffset(searchNode, offset) { + const childNodes = Array.from(searchNode.childNodes); + if (childNodes.length === 0) { + const textContentLength = searchNode.textContent?.length ?? 0; + if (offset > textContentLength) { + return { found: false, remainingOffset: offset - textContentLength }; + } + return { found: true, node: searchNode, offset }; + } + for (const childNode of Array.from(searchNode.childNodes)) { + const result = computeNodeOffsetFromTextOffset(childNode, offset); + if (result.found) { + return result; + } + offset = /** @type {any} */ (result).remainingOffset; + } + return { found: false, remainingOffset: offset }; +} + +/** + * + * @param {Node} searchNode + * @param {number} offset + * @returns {void} + */ +function setTextCursorSelection(searchNode, offset) { + const result = computeNodeOffsetFromTextOffset(searchNode, offset); + if (!result.found) { + return; + } + + const sel = window.getSelection(); + if (sel === null) { + return; + } + + const range = document.createRange(); + range.setStart(result.node, result.offset); + range.collapse(true); + sel.removeAllRanges(); + sel.addRange(range); +} + +/** + * + * @param {string} str + * @param {{ range: Range; update: (old: string) => string }[]} updates + * @returns {string} + */ +function replaceAt(str, updates) { + updates.sort((u1, u2) => u1.range.offset - u2.range.offset); + let newStr = ""; + let lastUntouchedPos = 0; + for (const u of updates) { + newStr += str.slice(lastUntouchedPos, u.range.offset); + newStr += u.update(str.slice(u.range.offset, u.range.offsetEnd + 1)); + lastUntouchedPos = u.range.offset + u.range.length; + } + newStr += str.slice(lastUntouchedPos); + return newStr; +} + +export class InputAbbreviationRewriter { + /** @type {AbbreviationRewriter} */ + rewriter; + + /** @type {boolean} */ + isInSelectionChange = false; + + /** @type {AbbreviationConfig} */ + config; + + /** @type {HTMLInputElement} */ + textInput; + + /** + * @param {AbbreviationConfig} config + * @param {HTMLInputElement} textInput + */ + constructor(config, textInput) { + this.config = config; + this.textInput = textInput; + + const provider = new AbbreviationProvider(config); + this.rewriter = new AbbreviationRewriter(config, provider, this); + + textInput.addEventListener("beforeinput", async (inputEvent) => { + const range = new Range(this.getInput().length, 0); + const newText = inputEvent.data ?? ""; + const change = { range, newText }; + this.rewriter.changeInput([change]); + }); + + textInput.addEventListener("input", async (_) => { + await this.rewriter.triggerAbbreviationReplacement(); + await this.updateSelection(); + this.updateState(); + }); + + document.addEventListener("selectionchange", async () => { + // This happens when updating the state itself triggers a selection change. + if (this.isInSelectionChange) { + return; + } + this.isInSelectionChange = true; + await this.updateSelection(); + this.updateState(); + this.isInSelectionChange = true; + }); + + textInput.addEventListener("keydown", async (ev) => { + if (ev.key === "Tab") { + await this.rewriter.replaceAllTrackedAbbreviations(); + this.updateState(); + ev.preventDefault(); + } + }); + } + + resetAbbreviations() { + this.rewriter.resetTrackedAbbreviations(); + this.updateState(); + } + + async updateSelection() { + const selection = this.getSelection(); + if (selection === undefined) { + return; + } + await this.rewriter.changeSelections([selection]); + } + + /** + * @returns {Range | undefined} + */ + getSelection() { + return findTextCursorSelection(this.textInput); + } + + updateState() { + const query = this.getInput(); + const queryHtml = this.textInput.innerHTML; + const updates = Array.from(this.rewriter.getTrackedAbbreviations()).map( + (a) => ({ + range: a.range, + update: (/** @type {string} */ old) => `${old}`, + }) + ); + const newQueryHtml = replaceAt(query, updates); + if (queryHtml === newQueryHtml) { + return; + } + const selectionBeforeChange = this.getSelection(); + this.setInputHTML(newQueryHtml); + if (selectionBeforeChange !== undefined) { + this.setSelections([selectionBeforeChange]); + } + } + + /** + * @param {Change[]} changes + * @returns {Promise} + */ + async replaceAbbreviations(changes) { + /** @type {{ range: Range; update: (old: string) => string }[]} */ + const updates = changes.map((c) => ({ + range: c.range, + update: (_) => c.newText, + })); + this.setInputHTML(replaceAt(this.getInput(), updates)); + return true; + } + + /** + * @return {SelectionMoveMode} + */ + selectionMoveMode() { + return { kind: "MoveAllSelections" }; + } + + /** + * @return {Range[]} + */ + collectSelections() { + const selection = this.getSelection(); + if (selection === undefined) { + return []; + } + return [selection]; + } + + /** + * + * @param {Range[]} selections + * @returns {void} + */ + setSelections(selections) { + const primarySelection = selections[0]; + if (primarySelection === undefined) { + return; + } + setTextCursorSelection(this.textInput, primarySelection.offset); + } + + /** + * @param {string} html + */ + setInputHTML(html) { + this.textInput.value = html; + } + + /** + * @returns {string} + */ + getInput() { + return this.textInput.value; + } +} 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}; diff --git a/static/search/w3-license.md b/static/search/w3-license.md new file mode 100644 index 00000000..d62d37bf --- /dev/null +++ b/static/search/w3-license.md @@ -0,0 +1,11 @@ +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/" From 800ee59f45a447998d96994b6a506454e2c3c981 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 10 Jan 2025 13:55:52 +0100 Subject: [PATCH 02/37] feat: more search domains --- lake-manifest.json | 2 +- static/search/domain-mappers.js | 34 ++++++++++++++++++++++++++++++++- static/search/search-box.css | 12 +++++++++--- static/search/search-box.js | 2 +- static/search/search-init.js | 2 +- 5 files changed, 45 insertions(+), 7 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e22fca47..03b3f956 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b1484a6fe948b6a407e3d6f30b9aa073877b6954", + "rev": "9dbac26d254a8b4f6ea935cb0d4f79608f2cd274", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "custom-head", diff --git a/static/search/domain-mappers.js b/static/search/domain-mappers.js index b9a6348b..8ea287d1 100644 --- a/static/search/domain-mappers.js +++ b/static/search/domain-mappers.js @@ -38,7 +38,7 @@ const docOptionDomainMapper = { const docTacticDomainMapper = { dataToSearchables: (domainData) => Object.entries(domainData.contents).map(([key, value]) => ({ - searchKey: key, + searchKey: value[0].data.userName, address: `${value[0].address}#${value[0].id}`, domainId: "Verso.Genre.Manual.doc.tactic", ref: value, @@ -47,6 +47,21 @@ const docTacticDomainMapper = { 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: "doc-tactic-domain", + displayName: "Conv Tactic", +}; + /** * @type {DomainMapper} */ @@ -62,9 +77,26 @@ const sectionMapper = { 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", +}; + 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, }; diff --git a/static/search/search-box.css b/static/search/search-box.css index d91b7067..4e14fb8a 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -29,7 +29,7 @@ } #search-wrapper .combobox input { - width: 16rem; + width: 24rem; outline: none; font-size: .9rem; padding: .3rem .5rem; @@ -46,7 +46,7 @@ padding: 0; position: absolute; top: calc(100%); - width: 16rem; + width: 24rem; list-style: none; background-color: white; display: none; @@ -76,6 +76,10 @@ font-family: var(--verso-code-font-family); } +#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; @@ -124,5 +128,7 @@ #search-wrapper { padding: var(--verso--content-padding-x); width: fit-content; - float: right; + position: absolute; + top: 0; + right: 0; } diff --git a/static/search/search-box.js b/static/search/search-box.js index 74326ea8..4e9f2d9a 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -39,7 +39,7 @@ const dataToSearchableMap = (json, domainMappers) => return acc; } - if (!acc[cur.searchKey]) { + if (!acc.hasOwnProperty(cur.searchKey)) { acc[cur.searchKey] = []; } acc[cur.searchKey].push(cur); diff --git a/static/search/search-init.js b/static/search/search-init.js index 5e2b0519..aeea7639 100644 --- a/static/search/search-init.js +++ b/static/search/search-init.js @@ -12,7 +12,7 @@ const searchHTML = `
    class="cb_edit" type="search" role="searchbox" - placeholder="Search" + placeholder="Index" aria-autocomplete="list" aria-expanded="false" aria-controls="cb1-listbox" From 7ec1603048a176d74b8b9733d7ba400f3a862b4d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 10 Jan 2025 15:16:37 +0100 Subject: [PATCH 03/37] feat: section numbers in search box --- lake-manifest.json | 2 +- static/search/domain-mappers.js | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 03b3f956..05126291 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9dbac26d254a8b4f6ea935cb0d4f79608f2cd274", + "rev": "97e01bd21265fdc719371f20ba69bdaf26896357", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "custom-head", diff --git a/static/search/domain-mappers.js b/static/search/domain-mappers.js index 8ea287d1..f0803766 100644 --- a/static/search/domain-mappers.js +++ b/static/search/domain-mappers.js @@ -68,7 +68,7 @@ const docConvTacticDomainMapper = { const sectionMapper = { dataToSearchables: (domainData) => Object.entries(domainData.contents).map(([key, value]) => ({ - searchKey: value[0].data[value[0].data.length - 1], + searchKey: `${value[0].data.sectionNum} ${value[0].data.title}`, address: `${value[0].address}#${value[0].id}`, domainId: "Verso.Genre.Manual.section", ref: value, From b1af71edb9297cef9ce3ec01c215d73f695e2ee6 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 12 Jan 2025 12:14:35 +0100 Subject: [PATCH 04/37] feat: add z-index to searchbox, narrower on mobile --- static/search/search-box.css | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/static/search/search-box.css b/static/search/search-box.css index 4e14fb8a..34243452 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -2,8 +2,16 @@ --selected-color: #def; } -#search-wrapper { - align-self: flex-end; +@media screen and (700px < width) { + :root { + --search-bar-width: 24rem; + } +} + +@media screen and (width <= 700px) { + :root { + --search-bar-width: 12rem; + } } #search-wrapper .combobox-list { @@ -29,7 +37,7 @@ } #search-wrapper .combobox input { - width: 24rem; + width: var(--search-bar-width); outline: none; font-size: .9rem; padding: .3rem .5rem; @@ -46,7 +54,7 @@ padding: 0; position: absolute; top: calc(100%); - width: 24rem; + width: var(--search-bar-width); list-style: none; background-color: white; display: none; @@ -131,4 +139,5 @@ position: absolute; top: 0; right: 0; + z-index: 1; } From aef34db7c85e20b08acc9301fd63d8d60927b131 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 12 Jan 2025 13:13:25 +0100 Subject: [PATCH 05/37] feat: tweak searchbox padding for small screens --- static/search/search-box.css | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/static/search/search-box.css b/static/search/search-box.css index 34243452..425c9468 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -141,3 +141,16 @@ 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; + } +} \ No newline at end of file From b001196e681ecb8572aed023493f4e0d9be078e7 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 12 Jan 2025 13:42:31 +0100 Subject: [PATCH 06/37] feat: don't set the value when tabbing --- static/search/search-box.js | 5 ----- 1 file changed, 5 deletions(-) diff --git a/static/search/search-box.js b/static/search/search-box.js index 4e9f2d9a..0985960e 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -695,11 +695,6 @@ class SearchBox { case "Tab": this.close(true); - if (this.listboxHasVisualFocus) { - if (this.currentOption) { - this.setValue(resultToText(this.currentOption)); - } - } break; case "Home": From 32644d1b76d7bba3b686843f5f35901614f6c007 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 12 Jan 2025 13:44:38 +0100 Subject: [PATCH 07/37] feat: don't allow later listeners to react if the keypress is handled --- static/search/search-box.js | 2 +- static/search/unicode-input-component.js | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/static/search/search-box.js b/static/search/search-box.js index 0985960e..10c1c515 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -713,7 +713,7 @@ class SearchBox { } if (eventHandled) { - event.stopPropagation(); + event.stopImmediatePropagation(); event.preventDefault(); } } diff --git a/static/search/unicode-input-component.js b/static/search/unicode-input-component.js index 7ebb45ec..76123661 100644 --- a/static/search/unicode-input-component.js +++ b/static/search/unicode-input-component.js @@ -237,6 +237,7 @@ export class InputAbbreviationRewriter { await this.rewriter.replaceAllTrackedAbbreviations(); this.updateState(); ev.preventDefault(); + ev.stopImmediatePropagation(); } }); } From e4f8d533cb87b9e6927d0e63220e938dfd66a32c Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 19 Jan 2025 15:53:55 +0100 Subject: [PATCH 08/37] chore: add license and legal header information --- static/search/domain-mappers.js | 6 ++++++ static/search/fuzzysort-license.md | 21 +++++++++++++++++++++ static/search/search-box.css | 8 +++++++- static/search/search-box.js | 9 +++++++++ static/search/search-init.js | 6 ++++++ static/search/unicode-input-component.js | 5 +++++ 6 files changed, 54 insertions(+), 1 deletion(-) create mode 100644 static/search/fuzzysort-license.md diff --git a/static/search/domain-mappers.js b/static/search/domain-mappers.js index f0803766..d3ea71d5 100644 --- a/static/search/domain-mappers.js +++ b/static/search/domain-mappers.js @@ -1,3 +1,9 @@ +/** + * 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' */ diff --git a/static/search/fuzzysort-license.md b/static/search/fuzzysort-license.md new file mode 100644 index 00000000..736006f1 --- /dev/null +++ b/static/search/fuzzysort-license.md @@ -0,0 +1,21 @@ +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. \ No newline at end of file diff --git a/static/search/search-box.css b/static/search/search-box.css index 425c9468..6d854462 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -1,4 +1,10 @@ -:root { +/** + * 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; } diff --git a/static/search/search-box.js b/static/search/search-box.js index 10c1c515..286dc28d 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -1,3 +1,12 @@ +/** + * 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 diff --git a/static/search/search-init.js b/static/search/search-init.js index aeea7639..5737f72e 100644 --- a/static/search/search-init.js +++ b/static/search/search-init.js @@ -1,3 +1,9 @@ +/** + * 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'; diff --git a/static/search/unicode-input-component.js b/static/search/unicode-input-component.js index 76123661..6e0b030d 100644 --- a/static/search/unicode-input-component.js +++ b/static/search/unicode-input-component.js @@ -1,3 +1,8 @@ +/** + * Copyright (c) 2024 Lean FRO LLC. All rights reserved. + * Released under Apache 2.0 license as described in the file LICENSE. + */ + // @ts-check /** From 9a3cc735d4763d76d4a1a7ef7c77fe460f1fa662 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 19 Jan 2025 15:54:21 +0100 Subject: [PATCH 09/37] fix: tab navigation in search bar --- static/search/unicode-input-component.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/static/search/unicode-input-component.js b/static/search/unicode-input-component.js index 6e0b030d..6f8a48e7 100644 --- a/static/search/unicode-input-component.js +++ b/static/search/unicode-input-component.js @@ -238,7 +238,7 @@ export class InputAbbreviationRewriter { }); textInput.addEventListener("keydown", async (ev) => { - if (ev.key === "Tab") { + if (ev.key === "Tab" && this.rewriter.getTrackedAbbreviations().size > 0) { await this.rewriter.replaceAllTrackedAbbreviations(); this.updateState(); ev.preventDefault(); From cf42026a4f7ea24da21e9cd111cbc40d1e0723c9 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 19 Jan 2025 15:55:02 +0100 Subject: [PATCH 10/37] chore: add types and type configuration for easier ci integration --- static/search/fuzzysort.d.ts | 105 +++++++++++++++++++++++++++++++++++ static/search/jsconfig.json | 8 +++ 2 files changed, 113 insertions(+) create mode 100644 static/search/fuzzysort.d.ts create mode 100644 static/search/jsconfig.json 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/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 From 8b0bb9927fb99e1b1cfa423320d457574f03132a Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Sat, 25 Jan 2025 00:09:40 +0100 Subject: [PATCH 11/37] chore: CI for TypeScript check for search box --- .github/workflows/check-search-tsc.yml | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 .github/workflows/check-search-tsc.yml 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 + From e1bd3e24f26b01467bba3b018e854692e125bdff Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 26 Jan 2025 15:30:04 +0100 Subject: [PATCH 12/37] chore: consolidate licenses for search box --- static/search/fuzzysort-license.md | 21 --------------- static/search/licenses.md | 41 ++++++++++++++++++++++++++++++ static/search/search-box.js | 2 +- static/search/w3-license.md | 11 -------- 4 files changed, 42 insertions(+), 33 deletions(-) delete mode 100644 static/search/fuzzysort-license.md create mode 100644 static/search/licenses.md delete mode 100644 static/search/w3-license.md diff --git a/static/search/fuzzysort-license.md b/static/search/fuzzysort-license.md deleted file mode 100644 index 736006f1..00000000 --- a/static/search/fuzzysort-license.md +++ /dev/null @@ -1,21 +0,0 @@ -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. \ 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.js b/static/search/search-box.js index 286dc28d..c9eed437 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -121,7 +121,7 @@ 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/ * - * More documentation to come! + * The license for the combobox is in `licenses.md`. */ class SearchBox { /** diff --git a/static/search/w3-license.md b/static/search/w3-license.md deleted file mode 100644 index d62d37bf..00000000 --- a/static/search/w3-license.md +++ /dev/null @@ -1,11 +0,0 @@ -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/" From 4dbf41ecaebdcda3eebb35537bbb364bb2e42adb Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 26 Jan 2025 15:30:58 +0100 Subject: [PATCH 13/37] chore: write readme for search box --- static/search/README.txt | 59 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/static/search/README.txt b/static/search/README.txt index e69de29b..bca379fb 100644 --- a/static/search/README.txt +++ 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. From 647117425db80ad8281f7714d9a5c74404aed78e Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 26 Jan 2025 16:35:05 +0100 Subject: [PATCH 14/37] feat: remove autocomplete option This is a search box, and autocomplete functionality is not necessary. --- static/search/search-box.js | 109 +++++++----------------------------- 1 file changed, 20 insertions(+), 89 deletions(-) diff --git a/static/search/search-box.js b/static/search/search-box.js index c9eed437..0802edc1 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -154,21 +154,6 @@ class SearchBox { */ hasHover; - /** - * @type {boolean} - */ - isNone; - - /** - * @type {boolean} - */ - isList; - - /** - * @type {boolean} - */ - isBoth; - /** * @type {SearchResult | null} */ @@ -253,10 +238,6 @@ class SearchBox { this.hasHover = false; - this.isNone = false; - this.isList = false; - this.isBoth = false; - this.currentOption = null; this.firstOption = null; this.lastOption = null; @@ -264,19 +245,6 @@ class SearchBox { this.filteredOptions = []; this.filter = ""; - const autocomplete = this.comboboxNode - .getAttribute("aria-autocomplete") - ?.toLowerCase(); - - if (typeof autocomplete === "string") { - this.isNone = autocomplete === "none"; - this.isList = autocomplete === "list"; - this.isBoth = autocomplete === "both"; - } else { - // default value of autocomplete - this.isNone = true; - } - this.comboboxNode.addEventListener( "keydown", this.onComboboxKeyDown.bind(this) @@ -380,28 +348,12 @@ class SearchBox { /** * @param {SearchResult} option - * @param {boolean} [setSelection] */ - setOption(option, setSelection) { + setOption(option) { if (option) { this.currentOption = option; this.setCurrentOptionStyle(this.currentOption); this.setActiveDescendant(this.currentOption.htmlItem); - - if (this.isBoth) { - this.comboboxNode.value = resultToText(this.currentOption); - if (setSelection) { - this.comboboxNode.setSelectionRange( - resultToText(this.currentOption).length, - resultToText(this.currentOption).length - ); - } else { - this.comboboxNode.setSelectionRange( - this.filter.length, - resultToText(this.currentOption).length - ); - } - } } } @@ -433,11 +385,6 @@ class SearchBox { // ComboboxAutocomplete Events filterOptions() { - // do not filter any options if autocomplete is none - if (this.isNone) { - this.filter = ""; - } - const currentOptionText = opt(this.currentOption, resultToText); const filter = this.filter; @@ -647,16 +594,14 @@ class SearchBox { } else { this.open(); if ( - this.listboxHasVisualFocus || - (this.isBoth && this.filteredOptions.length > 1) + this.listboxHasVisualFocus ) { this.setOption( - this.getNextOption(this.currentOption, this.firstOption), - true + this.getNextOption(this.currentOption, this.firstOption) ); this.setVisualFocusListbox(); } else { - this.setOption(this.firstOption, true); + this.setOption(this.firstOption); this.setVisualFocusListbox(); } } @@ -673,13 +618,12 @@ class SearchBox { ) { if (this.listboxHasVisualFocus) { this.setOption( - this.getPreviousOption(this.currentOption, this.lastOption), - true + this.getPreviousOption(this.currentOption, this.lastOption) ); } else { this.open(); if (!altKey) { - this.setOption(this.lastOption, true); + this.setOption(this.lastOption); this.setVisualFocusListbox(); } } @@ -773,12 +717,8 @@ class SearchBox { case "ArrowRight": case "Home": case "End": - if (this.isBoth) { - this.filter = this.comboboxNode.value; - } else { - this.option = null; - this.setCurrentOptionStyle(null); - } + this.option = null; + this.setCurrentOptionStyle(null); this.setVisualFocusCombobox(); eventHandled = true; break; @@ -788,28 +728,19 @@ class SearchBox { this.setVisualFocusCombobox(); this.setCurrentOptionStyle(null); eventHandled = true; - - if (this.isList || this.isBoth) { - const option = this.filterOptions(); - if (option) { - if (this.isClosed() && this.comboboxNode.value.length) { - this.open(); - } - - this.option = option; - if (this.isBoth || this.isList || this.listboxHasVisualFocus) { - this.setCurrentOptionStyle(option); - if (this.isBoth || this.isList) { - this.setOption(option); - } - } - } else { - this.close(); - this.option = null; - this.setActiveDescendant(null); + const option = this.filterOptions(); + if (option) { + if (this.isClosed() && this.comboboxNode.value.length) { + this.open(); } - } else if (this.comboboxNode.value.length) { - this.open(); + + this.option = option; + this.setCurrentOptionStyle(option); + this.setOption(option); + } else { + this.close(); + this.option = null; + this.setActiveDescendant(null); } } From 0f06f0c52b025e8d4b27b357d0d7ac69bdfc061e Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 26 Jan 2025 16:43:32 +0100 Subject: [PATCH 15/37] feat: enable underlined IME for search box --- static/search/search-box.css | 22 +- static/search/search-box.js | 41 ++- static/search/search-init.js | 6 +- static/search/unicode-input-component.js | 348 ------------------- static/search/unicode-input-component.min.js | 2 + 5 files changed, 43 insertions(+), 376 deletions(-) delete mode 100644 static/search/unicode-input-component.js create mode 100644 static/search/unicode-input-component.min.js diff --git a/static/search/search-box.css b/static/search/search-box.css index 6d854462..373cf420 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -25,11 +25,11 @@ } #search-wrapper .combobox .group { - display: inline-flex; + display: flex; cursor: pointer; } -#search-wrapper .combobox input { +#search-wrapper .combobox .cb_edit { background-color: white; color: black; box-sizing: border-box; @@ -40,21 +40,29 @@ border-bottom: 1px solid gray; position: relative; cursor: pointer; -} - -#search-wrapper .combobox input { width: var(--search-bar-width); outline: none; font-size: .9rem; padding: .3rem .5rem; + font-family: sans-serif; } -#search-wrapper .combobox .group.focus input, -#search-wrapper .combobox .group input:hover { +#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; diff --git a/static/search/search-box.js b/static/search/search-box.js index 0802edc1..52f608d7 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -10,7 +10,7 @@ // Enable typescript // @ts-check -import { InputAbbreviationRewriter } from "./unicode-input-component.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}} */ ( @@ -125,7 +125,7 @@ const opt = (v, fn) => (v != null ? fn(v) : undefined); */ class SearchBox { /** - * @type {HTMLInputElement} + * @type {HTMLDivElement} */ comboboxNode; @@ -200,8 +200,11 @@ class SearchBox { /** @type {DomainMappers} */ domainMappers; + /** @type {InputAbbreviationRewriter} */ + imeRewriter; + /** - * @param {HTMLInputElement} comboboxNode + * @param {HTMLDivElement} comboboxNode * @param {HTMLButtonElement | null} buttonNode * @param {HTMLElement} listboxNode * @param {DomainMappers} domainMappers @@ -224,7 +227,7 @@ class SearchBox { ); // Add IME - new InputAbbreviationRewriter( + this.imeRewriter = new InputAbbreviationRewriter( { abbreviationCharacter: "\\", customTranslations: [], @@ -341,8 +344,8 @@ class SearchBox { */ setValue(value) { this.filter = value; - this.comboboxNode.value = this.filter; - this.comboboxNode.setSelectionRange(this.filter.length, this.filter.length); + this.comboboxNode.textContent = this.filter; + this.imeRewriter.setSelections([{ offset: this.filter.length }]); this.filterOptions(); } @@ -635,12 +638,12 @@ class SearchBox { case "Escape": if (this.isOpen()) { this.close(true); - this.filter = this.comboboxNode.value; + this.filter = this.comboboxNode.textContent; this.filterOptions(); this.setVisualFocusCombobox(); } else { this.setValue(""); - this.comboboxNode.value = ""; + this.comboboxNode.textContent = ""; } this.option = null; eventHandled = true; @@ -651,13 +654,13 @@ class SearchBox { break; case "Home": - this.comboboxNode.setSelectionRange(0, 0); + this.imeRewriter.setSelections([{ offset: 0 }]); eventHandled = true; break; case "End": - var length = this.comboboxNode.value.length; - this.comboboxNode.setSelectionRange(length, length); + var length = this.comboboxNode.textContent.length; + this.imeRewriter.setSelections([{ offset: length }]); eventHandled = true; break; @@ -691,8 +694,8 @@ class SearchBox { } // this is for the case when a selection in the textbox has been deleted - if (this.comboboxNode.value.length < this.filter.length) { - this.filter = this.comboboxNode.value; + if (this.comboboxNode.textContent.length < this.filter.length) { + this.filter = this.comboboxNode.textContent; this.option = null; this.filterOptions(); } @@ -705,7 +708,7 @@ class SearchBox { case "Backspace": this.setVisualFocusCombobox(); this.setCurrentOptionStyle(null); - this.filter = this.comboboxNode.value; + this.filter = this.comboboxNode.textContent; this.option = null; this.filterOptions(); eventHandled = true; @@ -730,7 +733,7 @@ class SearchBox { eventHandled = true; const option = this.filterOptions(); if (option) { - if (this.isClosed() && this.comboboxNode.value.length) { + if (this.isClosed() && this.comboboxNode.textContent.length) { this.open(); } @@ -762,7 +765,7 @@ class SearchBox { } onComboboxFocus() { - this.filter = this.comboboxNode.value; + this.filter = this.comboboxNode.textContent; this.filterOptions(); this.setVisualFocusCombobox(); this.option = null; @@ -823,7 +826,7 @@ class SearchBox { * @returns void */ return () => { - this.comboboxNode.value = resultToText(result); + this.comboboxNode.textContent = resultToText(result); this.confirmResult(result); this.close(true); }; @@ -849,7 +852,9 @@ class SearchBox { * @param {RegisterSearchArgs} args */ export const registerSearch = ({ searchWrapper, data, domainMappers }) => { - const comboboxNode = searchWrapper.querySelector("input"); + const comboboxNode = /** @type {HTMLDivElement} */ ( + searchWrapper.querySelector("div[contenteditable]") + ); const buttonNode = searchWrapper.querySelector("button"); const listboxNode = /** @type {HTMLElement | null} */ ( diff --git a/static/search/search-init.js b/static/search/search-init.js index 5737f72e..90f560f1 100644 --- a/static/search/search-init.js +++ b/static/search/search-init.js @@ -13,16 +13,16 @@ let siteRoot = typeof __versoSiteRoot !== 'undefined' ? __versoSiteRoot : ""; const searchHTML = `
    - + >
      diff --git a/static/search/unicode-input-component.js b/static/search/unicode-input-component.js deleted file mode 100644 index 6f8a48e7..00000000 --- a/static/search/unicode-input-component.js +++ /dev/null @@ -1,348 +0,0 @@ -/** - * Copyright (c) 2024 Lean FRO LLC. All rights reserved. - * Released under Apache 2.0 license as described in the file LICENSE. - */ - -// @ts-check - -/** - * This is copied from `https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input-component/src/index.ts` - * but modified to work without compilation, and with an input element instead of a contenteditable div. This loses the - * underlining that the original had, but allows us to keep using an input element. - */ - -import { - AbbreviationProvider, - AbbreviationRewriter, - Range, -} from "./unicode-input.min.js"; - -/** - * @typedef {any} AbbreviationConfig - * @typedef {any} SelectionMoveMode - * @typedef {any} Range - * @typedef {any} Change - */ - -/** - * @param {Node} searchNode - * @param {Node} target - * @param {number} offsetInTarget - * @returns {number | undefined} - */ -function computeTextOffsetFromNodeOffset(searchNode, target, offsetInTarget) { - if (searchNode === target) { - return offsetInTarget; - } - if (!searchNode.contains(target)) { - return undefined; - } - - let totalOffset = 0; - for (const childNode of Array.from(searchNode.childNodes)) { - const childOffset = computeTextOffsetFromNodeOffset( - childNode, - target, - offsetInTarget - ); - if (childOffset !== undefined) { - totalOffset += childOffset; - return totalOffset; - } - totalOffset += childNode.textContent?.length ?? 0; - } - return undefined; -} - -/** - * @param {Node} searchNode - * @param {{ node: Node; offset: number } | undefined} rangeStart - * @param {{ node: Node; offset: number } | undefined} rangeEnd - * @returns {Range | undefined} - */ -function computeTextRangeFromNodeRange(searchNode, rangeStart, rangeEnd) { - /** @var {number | undefined} */ - let start; - /** @var {number | undefined} */ - let end; - if (rangeStart) { - start = computeTextOffsetFromNodeOffset( - searchNode, - rangeStart.node, - rangeStart.offset - ); - } - if (rangeEnd) { - end = computeTextOffsetFromNodeOffset( - searchNode, - rangeEnd.node, - rangeEnd.offset - ); - } - - if (start === undefined) { - if (end === undefined) { - return undefined; - } else { - return new Range(end, 0); - } - } else { - if (end === undefined) { - return new Range(start, 0); - } else { - if (end < start) { - [start, end] = [end, start]; - } - return new Range(start, end - start); - } - } -} - -/** - * @param {Node} searchNode - * @returns {Range | undefined} - */ -function findTextCursorSelection(searchNode) { - const sel = window.getSelection(); - if (sel === null) { - return undefined; - } - - /** @var {{ node: Node; offset: number } | undefined} */ - let rangeStart; - if (sel.anchorNode) { - rangeStart = { node: sel.anchorNode, offset: sel.anchorOffset }; - } - /** @var {{ node: Node; offset: number } | undefined} */ - let rangeEnd; - if (sel.focusNode) { - rangeStart = { node: sel.focusNode, offset: sel.focusOffset }; - } - - return computeTextRangeFromNodeRange(searchNode, rangeStart, rangeEnd); -} - -/** - * @param {Node} searchNode - * @param {number} offset - * @returns {{ found: true; node: Node; offset: number } | { found: false; remainingOffset: number }} - */ -function computeNodeOffsetFromTextOffset(searchNode, offset) { - const childNodes = Array.from(searchNode.childNodes); - if (childNodes.length === 0) { - const textContentLength = searchNode.textContent?.length ?? 0; - if (offset > textContentLength) { - return { found: false, remainingOffset: offset - textContentLength }; - } - return { found: true, node: searchNode, offset }; - } - for (const childNode of Array.from(searchNode.childNodes)) { - const result = computeNodeOffsetFromTextOffset(childNode, offset); - if (result.found) { - return result; - } - offset = /** @type {any} */ (result).remainingOffset; - } - return { found: false, remainingOffset: offset }; -} - -/** - * - * @param {Node} searchNode - * @param {number} offset - * @returns {void} - */ -function setTextCursorSelection(searchNode, offset) { - const result = computeNodeOffsetFromTextOffset(searchNode, offset); - if (!result.found) { - return; - } - - const sel = window.getSelection(); - if (sel === null) { - return; - } - - const range = document.createRange(); - range.setStart(result.node, result.offset); - range.collapse(true); - sel.removeAllRanges(); - sel.addRange(range); -} - -/** - * - * @param {string} str - * @param {{ range: Range; update: (old: string) => string }[]} updates - * @returns {string} - */ -function replaceAt(str, updates) { - updates.sort((u1, u2) => u1.range.offset - u2.range.offset); - let newStr = ""; - let lastUntouchedPos = 0; - for (const u of updates) { - newStr += str.slice(lastUntouchedPos, u.range.offset); - newStr += u.update(str.slice(u.range.offset, u.range.offsetEnd + 1)); - lastUntouchedPos = u.range.offset + u.range.length; - } - newStr += str.slice(lastUntouchedPos); - return newStr; -} - -export class InputAbbreviationRewriter { - /** @type {AbbreviationRewriter} */ - rewriter; - - /** @type {boolean} */ - isInSelectionChange = false; - - /** @type {AbbreviationConfig} */ - config; - - /** @type {HTMLInputElement} */ - textInput; - - /** - * @param {AbbreviationConfig} config - * @param {HTMLInputElement} textInput - */ - constructor(config, textInput) { - this.config = config; - this.textInput = textInput; - - const provider = new AbbreviationProvider(config); - this.rewriter = new AbbreviationRewriter(config, provider, this); - - textInput.addEventListener("beforeinput", async (inputEvent) => { - const range = new Range(this.getInput().length, 0); - const newText = inputEvent.data ?? ""; - const change = { range, newText }; - this.rewriter.changeInput([change]); - }); - - textInput.addEventListener("input", async (_) => { - await this.rewriter.triggerAbbreviationReplacement(); - await this.updateSelection(); - this.updateState(); - }); - - document.addEventListener("selectionchange", async () => { - // This happens when updating the state itself triggers a selection change. - if (this.isInSelectionChange) { - return; - } - this.isInSelectionChange = true; - await this.updateSelection(); - this.updateState(); - this.isInSelectionChange = true; - }); - - textInput.addEventListener("keydown", async (ev) => { - if (ev.key === "Tab" && this.rewriter.getTrackedAbbreviations().size > 0) { - await this.rewriter.replaceAllTrackedAbbreviations(); - this.updateState(); - ev.preventDefault(); - ev.stopImmediatePropagation(); - } - }); - } - - resetAbbreviations() { - this.rewriter.resetTrackedAbbreviations(); - this.updateState(); - } - - async updateSelection() { - const selection = this.getSelection(); - if (selection === undefined) { - return; - } - await this.rewriter.changeSelections([selection]); - } - - /** - * @returns {Range | undefined} - */ - getSelection() { - return findTextCursorSelection(this.textInput); - } - - updateState() { - const query = this.getInput(); - const queryHtml = this.textInput.innerHTML; - const updates = Array.from(this.rewriter.getTrackedAbbreviations()).map( - (a) => ({ - range: a.range, - update: (/** @type {string} */ old) => `${old}`, - }) - ); - const newQueryHtml = replaceAt(query, updates); - if (queryHtml === newQueryHtml) { - return; - } - const selectionBeforeChange = this.getSelection(); - this.setInputHTML(newQueryHtml); - if (selectionBeforeChange !== undefined) { - this.setSelections([selectionBeforeChange]); - } - } - - /** - * @param {Change[]} changes - * @returns {Promise} - */ - async replaceAbbreviations(changes) { - /** @type {{ range: Range; update: (old: string) => string }[]} */ - const updates = changes.map((c) => ({ - range: c.range, - update: (_) => c.newText, - })); - this.setInputHTML(replaceAt(this.getInput(), updates)); - return true; - } - - /** - * @return {SelectionMoveMode} - */ - selectionMoveMode() { - return { kind: "MoveAllSelections" }; - } - - /** - * @return {Range[]} - */ - collectSelections() { - const selection = this.getSelection(); - if (selection === undefined) { - return []; - } - return [selection]; - } - - /** - * - * @param {Range[]} selections - * @returns {void} - */ - setSelections(selections) { - const primarySelection = selections[0]; - if (primarySelection === undefined) { - return; - } - setTextCursorSelection(this.textInput, primarySelection.offset); - } - - /** - * @param {string} html - */ - setInputHTML(html) { - this.textInput.value = html; - } - - /** - * @returns {string} - */ - getInput() { - return this.textInput.value; - } -} 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}; From fb7673f719b35db3ae600b4d661b93c7daa945bf Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 26 Jan 2025 16:44:26 +0100 Subject: [PATCH 16/37] fix: make placeholder text work again after user types and deletes --- static/search/search-box.js | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/static/search/search-box.js b/static/search/search-box.js index 52f608d7..9c34581d 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -774,6 +774,11 @@ class SearchBox { onComboboxBlur() { this.removeVisualFocusAll(); + // Remove empty space created by browser after user deletes entered text. + // Makes the placeholder appear again. + if (this.comboboxNode.innerHTML.trim().length === 0) { + this.comboboxNode.innerHTML = ""; + } } /** From ec4853a99c00ed0611dd4143ec6ef9a9768abb30 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 26 Jan 2025 16:51:21 +0100 Subject: [PATCH 17/37] feat: pass the right kind of Range to the rewriter --- static/search/search-box.js | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/static/search/search-box.js b/static/search/search-box.js index 9c34581d..f6712df7 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -10,6 +10,7 @@ // 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`. @@ -345,7 +346,7 @@ class SearchBox { setValue(value) { this.filter = value; this.comboboxNode.textContent = this.filter; - this.imeRewriter.setSelections([{ offset: this.filter.length }]); + this.imeRewriter.setSelections([new Range(this.filter.length, 0)]); this.filterOptions(); } @@ -654,13 +655,13 @@ class SearchBox { break; case "Home": - this.imeRewriter.setSelections([{ offset: 0 }]); + this.imeRewriter.setSelections([new Range(0, 0)]); eventHandled = true; break; case "End": var length = this.comboboxNode.textContent.length; - this.imeRewriter.setSelections([{ offset: length }]); + this.imeRewriter.setSelections([new Range(this.filter.length, 0)]); eventHandled = true; break; From 13d3315078bc0f1c4315cd50c62f10cfc0eaac70 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 26 Jan 2025 18:39:14 +0100 Subject: [PATCH 18/37] fix: firefox eating spaces --- static/search/search-box.css | 2 ++ static/search/search-box.js | 8 ++++---- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/static/search/search-box.css b/static/search/search-box.css index 373cf420..8f251860 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -45,6 +45,8 @@ 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, diff --git a/static/search/search-box.js b/static/search/search-box.js index f6712df7..ae2699d8 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -393,7 +393,7 @@ class SearchBox { const filter = this.filter; // Empty the listbox - this.listboxNode.innerHTML = ""; + this.listboxNode.textContent = ""; this.listboxNode.append(...this.domainFilters); @@ -752,7 +752,7 @@ class SearchBox { } if (eventHandled) { - event.stopPropagation(); + event.stopImmediatePropagation(); event.preventDefault(); } } @@ -777,8 +777,8 @@ class SearchBox { this.removeVisualFocusAll(); // Remove empty space created by browser after user deletes entered text. // Makes the placeholder appear again. - if (this.comboboxNode.innerHTML.trim().length === 0) { - this.comboboxNode.innerHTML = ""; + if (this.comboboxNode.textContent.trim().length === 0) { + this.comboboxNode.textContent = ""; } } From 260338fb37475e2c5395804e46435efd6bce2c28 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Sun, 26 Jan 2025 18:44:29 +0100 Subject: [PATCH 19/37] fix: lower the threshold for search results This fixes the issue with single character words returning fewer results than other words. We should get back to validate whether we're getting too many useless results. --- static/search/search-box.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/static/search/search-box.js b/static/search/search-box.js index ae2699d8..c2154dee 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -407,7 +407,7 @@ class SearchBox { const results = fuzzysort.go(filter, this.preparedData, { limit: 20, - threshold: 0.5, + threshold: 0.25, }); if (results.length === 0) { From 389fdf345f92d23f960ec82983dd469e51f1b65d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 27 Jan 2025 07:10:57 +0100 Subject: [PATCH 20/37] chore: bump Verso This gets the custom-head branch with the latest changes too --- lake-manifest.json | 8 ++++---- lean-toolchain | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 05126291..72012713 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,20 +15,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "97e01bd21265fdc719371f20ba69bdaf26896357", + "rev": "e174a005979b72387963e22c4f1c09ae4c68a12b", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "custom-head", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/david-christiansen/md4lean", + {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, "scope": "", - "rev": "2b381ee8dceba3b934d3d4aea4a2702a61e5664f", + "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb", "name": "MD4Lean", "manifestFile": "lake-manifest.json", - "inputRev": "parser", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}], "name": "«verso-manual»", diff --git a/lean-toolchain b/lean-toolchain index 62ccd717..2ffc30ce 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.16.0-rc1 +leanprover/lean4:v4.16.0-rc2 \ No newline at end of file From 6e73ccc71048a8f8e5409a83cef1423e8b732b50 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Mon, 27 Jan 2025 18:12:16 +0100 Subject: [PATCH 21/37] fix: autocorrect on iphone --- static/search/search-init.js | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/static/search/search-init.js b/static/search/search-init.js index 90f560f1..8489ae84 100644 --- a/static/search/search-init.js +++ b/static/search/search-init.js @@ -10,6 +10,7 @@ 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 = `
      @@ -22,6 +23,10 @@ const searchHTML = `
      aria-autocomplete="list" aria-expanded="false" aria-controls="cb1-listbox" + spellcheck="false" + autocorrect="false" + autocapitalize="none" + inputmode="search" >
        From a45dbf4d147d8684f76fbdd9b20d00e4f6f6c802 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Mon, 27 Jan 2025 18:13:10 +0100 Subject: [PATCH 22/37] feat: increase results shown in search box --- static/search/search-box.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/static/search/search-box.js b/static/search/search-box.js index c2154dee..937e6dff 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -406,7 +406,7 @@ class SearchBox { } const results = fuzzysort.go(filter, this.preparedData, { - limit: 20, + limit: 30, threshold: 0.25, }); From 4850462d56b25d9512cbf706ff7650901e597886 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Mon, 27 Jan 2025 18:14:53 +0100 Subject: [PATCH 23/37] feat: show 'showing n/m results' in search box results This was a little complex to get to work, since it didn't show up when navigating the search results with the keyboard, but it's working now. --- static/search/search-box.css | 22 +++++++++++++++++----- static/search/search-box.js | 24 ++++++------------------ 2 files changed, 23 insertions(+), 23 deletions(-) diff --git a/static/search/search-box.css b/static/search/search-box.css index 8f251860..cb3dae12 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -80,20 +80,26 @@ overflow: scroll; overflow-x: hidden; font-size: .9rem; - cursor: pointer; z-index: 100; } -#search-wrapper .search-result { - margin: 0; +/* 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-family: sans-serif; 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 { @@ -110,7 +116,7 @@ } #search-wrapper [role="listbox"].focus li[aria-selected="true"], -#search-wrapper [role="listbox"] li:hover { +#search-wrapper .search-result:hover { background-color: var(--selected-color); padding-bottom: calc(.2rem - 1px); padding-top: calc(.2rem - 1px); @@ -139,6 +145,12 @@ font-size: .7rem; } +#search-wrapper .more-results { + text-align: center; + color: #777; + font-size: .7rem; +} + #search-wrapper .domain-filter label { display: flex; gap: .5rem diff --git a/static/search/search-box.js b/static/search/search-box.js index 937e6dff..3286ead6 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -304,30 +304,13 @@ class SearchBox { this.noResultsElement.textContent = "No results"; } - /** - * @param {Element} element - */ - isElementInView(element) { - const bounding = element.getBoundingClientRect(); - return ( - bounding.top >= 0 && - bounding.left >= 0 && - bounding.bottom <= - (window.innerHeight || document.documentElement.clientHeight) && - bounding.right <= - (window.innerWidth || document.documentElement.clientWidth) - ); - } - /** * @param {HTMLLIElement | null | undefined} option */ setActiveDescendant(option) { if (option && this.listboxHasVisualFocus) { this.comboboxNode.setAttribute("aria-activedescendant", option.id); - if (!this.isElementInView(option)) { - option.scrollIntoView({ behavior: "smooth", block: "nearest" }); - } + option.scrollIntoView({ behavior: "instant", block: "nearest" }); } else { this.comboboxNode.setAttribute("aria-activedescendant", ""); } @@ -471,6 +454,11 @@ class SearchBox { } } + 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; } From c05832a8f043a1e46a3c3750f2e62ca0e1f5ed6b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 28 Jan 2025 14:49:32 +0100 Subject: [PATCH 24/37] feat: add syntax keywords to search box --- Manual/Meta/Syntax.lean | 232 ++++++++++++++++++++++++++++---- Manual/Monads/Syntax.lean | 6 +- Manual/Terms.lean | 10 +- static/search/domain-mappers.js | 19 +++ 4 files changed, 237 insertions(+), 30 deletions(-) diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean index fd1f92d3..64da7c7d 100644 --- a/Manual/Meta/Syntax.lean +++ b/Manual/Meta/Syntax.lean @@ -25,10 +25,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 @@ -251,7 +247,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 @@ -264,7 +263,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 #[] @@ -437,14 +439,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 @@ -490,6 +499,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] @@ -559,7 +580,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 := @@ -571,7 +592,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 @@ -662,6 +683,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 /-- @@ -709,7 +890,9 @@ where let bnf ← getBnf config.toFreeSyntaxConfig isFirst [FreeSyntax.decode stx] 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)} #[]) + let searchTarget := searchable config.name bnf + 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) @@ -762,7 +945,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) @@ -773,9 +957,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 @@ -968,10 +1149,11 @@ 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 + modify fun st => st.saveDomainObjectData syntaxKindDomain k.toString (json%{"category": null, "forms": $searchable}) else logError "Couldn't deserialize grammar info during traversal" pure none @@ -979,14 +1161,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 => @@ -1006,9 +1188,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 7ecd510e..0a764f3a 100644 --- a/Manual/Monads/Syntax.lean +++ b/Manual/Monads/Syntax.lean @@ -20,6 +20,8 @@ set_option pp.rawOnError true set_option linter.unusedVariables false -- set_option trace.SubVerso.Highlighting.Code true +set_option guard_msgs.diff true + #doc (Manual) "Syntax" => Lean supports programming with functors, applicative functors, and monads via special syntax: @@ -281,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`. @@ -589,7 +591,7 @@ p : α → Prop inst✝ : DecidablePred p xs : Array α out✝ : Array Nat := #[] -col✝ : Std.Range := { start := 0, stop := xs.size, step := 1 } +col✝ : Std.Range := { start := 0, stop := xs.size, step := 1, step_pos := Nat.zero_lt_one } i : Nat r✝ : Array Nat out : Array Nat := r✝ diff --git a/Manual/Terms.lean b/Manual/Terms.lean index e517c20f..791b3582 100644 --- a/Manual/Terms.lean +++ b/Manual/Terms.lean @@ -18,6 +18,8 @@ open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode set_option linter.constructorNameAsVariable false +set_option guard_msgs.diff true + #doc (Manual) "Terms" => %%% tag := "terms" @@ -811,11 +813,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 ``` ::: @@ -1056,7 +1058,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 @@ -1385,7 +1387,7 @@ is not definitionally equal to the right-hand side 3 = 5 ⊢ 3 = 3 ∨ 3 = 5 --- -info: { val := 3, val2 := ?m.1487, ok := ⋯ } : OnlyThreeOrFive +info: { val := 3, val2 := ?m.1504, ok := ⋯ } : OnlyThreeOrFive -/ #guard_msgs in #check OnlyThreeOrFive.mk 3 .. diff --git a/static/search/domain-mappers.js b/static/search/domain-mappers.js index d3ea71d5..e160b550 100644 --- a/static/search/domain-mappers.js +++ b/static/search/domain-mappers.js @@ -98,6 +98,24 @@ const techTermMapper = { 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: "Verso.Genre.Manual.doc.syntaxKind", + ref: value, + })), + className: "syntax-domain", + displayName: "Syntax", +}; + + export const domainMappers = { "Verso.Genre.Manual.doc": docDomainMapper, "Verso.Genre.Manual.doc.option": docOptionDomainMapper, @@ -105,4 +123,5 @@ export const domainMappers = { "Verso.Genre.Manual.doc.tactic.conv": docConvTacticDomainMapper, "Verso.Genre.Manual.section": sectionMapper, "Verso.Genre.Manual.doc.tech": techTermMapper, + "Verso.Genre.Manual.doc.syntaxKind": syntaxMapper, }; From ccb3faa3a92d84d6f5de0d165d711b67c619de14 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 28 Jan 2025 15:47:03 +0100 Subject: [PATCH 25/37] fix: make searching for syntax tokens more reliable --- Manual/Language/InductiveTypes.lean | 7 +++++++ Manual/Meta/Syntax.lean | 13 ++++++++++--- static/search/domain-mappers.js | 4 ++-- 3 files changed, 19 insertions(+), 5 deletions(-) diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean index 5bf708e0..ab9394e4 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/Syntax.lean b/Manual/Meta/Syntax.lean index 64da7c7d..671908fc 100644 --- a/Manual/Meta/Syntax.lean +++ b/Manual/Meta/Syntax.lean @@ -888,9 +888,11 @@ 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}````````" + + 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 => @@ -1145,6 +1147,8 @@ 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 @@ -1153,7 +1157,10 @@ partial def grammar.descr : BlockDescr where let path ← (·.path) <$> read let _ ← Verso.Genre.Manual.externalTag id path k.toString modify fun st => st.saveDomainObject syntaxKindDomain k.toString id - modify fun st => st.saveDomainObjectData syntaxKindDomain k.toString (json%{"category": null, "forms": $searchable}) + + 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 diff --git a/static/search/domain-mappers.js b/static/search/domain-mappers.js index e160b550..a2e62b15 100644 --- a/static/search/domain-mappers.js +++ b/static/search/domain-mappers.js @@ -108,7 +108,7 @@ const syntaxMapper = { // 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: "Verso.Genre.Manual.doc.syntaxKind", + domainId: "Manual.Syntax.production", ref: value, })), className: "syntax-domain", @@ -123,5 +123,5 @@ export const domainMappers = { "Verso.Genre.Manual.doc.tactic.conv": docConvTacticDomainMapper, "Verso.Genre.Manual.section": sectionMapper, "Verso.Genre.Manual.doc.tech": techTermMapper, - "Verso.Genre.Manual.doc.syntaxKind": syntaxMapper, + "Manual.Syntax.production": syntaxMapper, }; From 27d5a95f6175ca3ee93dfb7d7edf9235a0b7ee3f Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 28 Jan 2025 15:50:58 +0100 Subject: [PATCH 26/37] Mono font for syntax in search box --- static/search/search-box.css | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/static/search/search-box.css b/static/search/search-box.css index cb3dae12..ce313db6 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -102,7 +102,9 @@ scroll-margin-bottom: 1.2rem; } -#search-wrapper .search-result.doc-domain, #search-wrapper .search-result.option-domain { +#search-wrapper .search-result.doc-domain, +#search-wrapper .search-result.option-domain, +#search-wrapper .search-result.syntax-domain { font-family: var(--verso-code-font-family); } @@ -181,4 +183,4 @@ padding-top: 0.25rem; padding-right: 0.5rem; } -} \ No newline at end of file +} From 3819c8357d949fe6745f60b4315fbf5061bc5aed Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 29 Jan 2025 11:32:07 +0100 Subject: [PATCH 27/37] feat: make Lake documentation metadata searchable --- Manual/BuildTools/Lake/Config.lean | 8 +- Manual/Meta/LakeToml.lean | 552 +++-------------------------- Manual/Meta/LakeToml/Toml.lean | 509 ++++++++++++++++++++++++++ static/search/domain-mappers.js | 85 +++++ static/search/search-box.css | 4 +- 5 files changed, 644 insertions(+), 514 deletions(-) create mode 100644 Manual/Meta/LakeToml/Toml.lean 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/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 => - {{{{hl.toHtml tableLink keyLink}}}} - | .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 {{{{commentStr}}}} - {{ {{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 => + {{{{hl.toHtml tableLink keyLink}}}} + | .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 {{{{commentStr}}}} + {{ {{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/static/search/domain-mappers.js b/static/search/domain-mappers.js index a2e62b15..0833cfb1 100644 --- a/static/search/domain-mappers.js +++ b/static/search/domain-mappers.js @@ -115,6 +115,86 @@ const syntaxMapper = { 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, @@ -124,4 +204,9 @@ export const domainMappers = { "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/search-box.css b/static/search/search-box.css index ce313db6..f0ff943b 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -104,7 +104,9 @@ #search-wrapper .search-result.doc-domain, #search-wrapper .search-result.option-domain, -#search-wrapper .search-result.syntax-domain { +#search-wrapper .search-result.syntax-domain, +#search-wrapper .search-result.lake-option-domain, +#search-wrapper .search-result.lake-command-domain { font-family: var(--verso-code-font-family); } From 2a4d702e1cb03fad770959561c32cce6dd278ffe Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 29 Jan 2025 12:13:37 +0100 Subject: [PATCH 28/37] fix: Search box CSS fixes --- static/search/domain-mappers.js | 4 ++-- static/search/search-box.css | 9 +++++++++ 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/static/search/domain-mappers.js b/static/search/domain-mappers.js index 0833cfb1..2acdd1e2 100644 --- a/static/search/domain-mappers.js +++ b/static/search/domain-mappers.js @@ -49,7 +49,7 @@ const docTacticDomainMapper = { domainId: "Verso.Genre.Manual.doc.tactic", ref: value, })), - className: "doc-tactic-domain", + className: "tactic-domain", displayName: "Tactic", }; @@ -64,7 +64,7 @@ const docConvTacticDomainMapper = { domainId: "Verso.Genre.Manual.doc.tactic.conv", ref: value, })), - className: "doc-tactic-domain", + className: "conv-tactic-domain", displayName: "Conv Tactic", }; diff --git a/static/search/search-box.css b/static/search/search-box.css index f0ff943b..be1b1f7a 100644 --- a/static/search/search-box.css +++ b/static/search/search-box.css @@ -106,10 +106,19 @@ #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); } From bf37c2a1c8a1aa50099d46486cd82ae157198e5f Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Wed, 29 Jan 2025 17:02:25 +0100 Subject: [PATCH 29/37] fix: searchbox exclamation mark sometimes registered as 1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit I've changed the basic approach from reading what key the user entered to read what is in the combobox. This also means that searching for α works, which I think it didn't before. --- static/search/search-box.js | 39 ++++--------------------------------- 1 file changed, 4 insertions(+), 35 deletions(-) diff --git a/static/search/search-box.js b/static/search/search-box.js index 3286ead6..e34c7ecc 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -634,7 +634,6 @@ class SearchBox { this.setValue(""); this.comboboxNode.textContent = ""; } - this.option = null; eventHandled = true; break; @@ -649,7 +648,7 @@ class SearchBox { case "End": var length = this.comboboxNode.textContent.length; - this.imeRewriter.setSelections([new Range(this.filter.length, 0)]); + this.imeRewriter.setSelections([new Range(length, 0)]); eventHandled = true; break; @@ -663,60 +662,33 @@ class SearchBox { } } - /** - * @param {string} str - */ - isPrintableCharacter(str) { - return str.length === 1 && str.match(/\S| /); - } - /** * @param {KeyboardEvent} event * @returns void */ onComboboxKeyUp(event) { let eventHandled = false; - const char = event.key; - - if (this.isPrintableCharacter(char)) { - this.filter += char; - } - - // this is for the case when a selection in the textbox has been deleted - if (this.comboboxNode.textContent.length < this.filter.length) { - this.filter = this.comboboxNode.textContent; - this.option = null; - this.filterOptions(); - } if (event.key === "Escape" || event.key === "Esc") { return; } switch (event.key) { - case "Backspace": - this.setVisualFocusCombobox(); - this.setCurrentOptionStyle(null); - this.filter = this.comboboxNode.textContent; - this.option = null; - this.filterOptions(); - eventHandled = true; - break; - case "Left": case "ArrowLeft": case "Right": case "ArrowRight": case "Home": case "End": - this.option = null; this.setCurrentOptionStyle(null); this.setVisualFocusCombobox(); eventHandled = true; break; default: - if (this.isPrintableCharacter(char)) { + // If characters have been added or removed + if (this.comboboxNode.textContent.length !== this.filter.length) { + this.filter = this.comboboxNode.textContent; this.setVisualFocusCombobox(); this.setCurrentOptionStyle(null); eventHandled = true; @@ -726,12 +698,10 @@ class SearchBox { this.open(); } - this.option = option; this.setCurrentOptionStyle(option); this.setOption(option); } else { this.close(); - this.option = null; this.setActiveDescendant(null); } } @@ -757,7 +727,6 @@ class SearchBox { this.filter = this.comboboxNode.textContent; this.filterOptions(); this.setVisualFocusCombobox(); - this.option = null; this.setCurrentOptionStyle(null); } From dc414cb7357480ae221ef6bd682fb4d70bbd750b Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Wed, 29 Jan 2025 17:13:28 +0100 Subject: [PATCH 30/37] fix: not searching when typing while holding backspace --- static/search/search-box.js | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/static/search/search-box.js b/static/search/search-box.js index e34c7ecc..c6afa300 100644 --- a/static/search/search-box.js +++ b/static/search/search-box.js @@ -686,8 +686,7 @@ class SearchBox { break; default: - // If characters have been added or removed - if (this.comboboxNode.textContent.length !== this.filter.length) { + if (this.comboboxNode.textContent !== this.filter) { this.filter = this.comboboxNode.textContent; this.setVisualFocusCombobox(); this.setCurrentOptionStyle(null); From 6bea9b670153c555e1800d4713cf092980c9f2e5 Mon Sep 17 00:00:00 2001 From: Jakob Vase Date: Wed, 29 Jan 2025 17:24:18 +0100 Subject: [PATCH 31/37] feat: more accessible searchbox --- static/search/search-init.js | 2 ++ 1 file changed, 2 insertions(+) diff --git a/static/search/search-init.js b/static/search/search-init.js index 8489ae84..ac4766b2 100644 --- a/static/search/search-init.js +++ b/static/search/search-init.js @@ -23,6 +23,8 @@ const searchHTML = `
        aria-autocomplete="list" aria-expanded="false" aria-controls="cb1-listbox" + aria-haspopup="listbox" + aria-label="Search" spellcheck="false" autocorrect="false" autocapitalize="none" From d0cb04a5540e85ef57ad44dbffccd27c5536a8a5 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 29 Jan 2025 22:49:25 +0100 Subject: [PATCH 32/37] chore: bump Verso version This gets the Z-index fix for the ToC --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7188bc20..1334a846 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e174a005979b72387963e22c4f1c09ae4c68a12b", + "rev": "acd05c95084092d91df6b4b2b8cb4ce495d3156f", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "custom-head", From 53a026552b97246ce88c2b0cc4436e933d2ec9a3 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 29 Jan 2025 23:00:32 +0100 Subject: [PATCH 33/37] feat: add some missing high-priority section tags This makes the search box work for "IO monad" --- Manual/IO.lean | 23 ++++++++++++++++++++++- Manual/Meta/Example.lean | 6 +++--- 2 files changed, 25 insertions(+), 4 deletions(-) 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/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 From 734868bb1117bdb8296b7ee9ab4a7f616ba87a07 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 30 Jan 2025 06:58:27 +0100 Subject: [PATCH 34/37] chore: the Verso PR is merged, target deps at the main branch again --- lake-manifest.json | 22 +++++++++++----------- lakefile.lean | 3 +-- 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 1334a846..1a891df7 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": "e89e49fe1c146e08f2fe71df859037f83742dd2b", + "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": "acd05c95084092d91df6b4b2b8cb4ce495d3156f", - "name": "verso", + "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", - "inputRev": "custom-head", - "inherited": false, + "inputRev": "main", + "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 5fd2cfb5..472da612 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,8 +7,7 @@ import Lake open Lake DSL open System (FilePath) -require verso from git "https://github.com/leanprover/verso.git"@"custom-head" -require subverso from git "https://github.com/leanprover/subverso.git"@"main" +require verso from git "https://github.com/leanprover/verso.git"@"main" package "verso-manual" where -- building the C code cost much more than the optimizations save From 3b5d3f341a10dec034947ddec4c3a238aaac9045 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 31 Jan 2025 10:18:27 +0100 Subject: [PATCH 35/37] chore: more descriptive search box placeholder --- static/search/search-init.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/static/search/search-init.js b/static/search/search-init.js index ac4766b2..57ec2ea7 100644 --- a/static/search/search-init.js +++ b/static/search/search-init.js @@ -19,7 +19,7 @@ const searchHTML = `
        class="cb_edit" contenteditable="true" role="searchbox" - placeholder="Index" + placeholder="Jump to..." aria-autocomplete="list" aria-expanded="false" aria-controls="cb1-listbox" From 60963b4f8f56d6112b886d3ce7db49d4abba021b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 31 Jan 2025 15:26:51 +0100 Subject: [PATCH 36/37] Automatically track open-source license usage --- Main.lean | 96 +++++++++++++++++++++++++++++++++++++++++++--- Manual/Intro.lean | 8 ++++ lake-manifest.json | 2 +- 3 files changed, 100 insertions(+), 6 deletions(-) diff --git a/Main.lean b/Main.lean index c1943671..916e807b 100644 --- a/Main.lean +++ b/Main.lean @@ -15,10 +15,98 @@ 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", @@ -27,14 +115,10 @@ where "/static/search/search-box.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", - "/static/katex/katex.min.css" ], extraJs := [ -- Search box "/static/search/fuzzysort.js", - -- KaTeX - "/static/katex/katex.min.js", - "/static/math.js", -- Print stylesheet improvements "/static/print.js" ], @@ -44,4 +128,6 @@ where 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/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/lake-manifest.json b/lake-manifest.json index 6584c0d7..0ae3ccb2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9c0d4a38c4ed8850882a057c3073e936f5495470", + "rev": "d9c0352c9ec4f953992a1739b4c3d25b15b78702", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main", From c78da6827d17f3678070b3070793fbb2bf4531a6 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 31 Jan 2025 19:18:49 +0100 Subject: [PATCH 37/37] Exclude licenses from prose lint --- .vale/scripts/rewrite_html.py | 4 ++++ 1 file changed, 4 insertions(+) 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)