diff --git a/COHERENCE.md b/COHERENCE.md index 636a8f3..7f8f456 100644 --- a/COHERENCE.md +++ b/COHERENCE.md @@ -1041,12 +1041,15 @@ layering, provenance, and adoption have not followed.** `ConfigValue`s; `describe-setting`'s "Source:" names where `define()` ran. The inspection view sketched above is currently impossible to render. -- **Adoption is eight settings**: `editing.auto-pair` (pair.lua), +- **Adoption is nine settings**: `editing.auto-pair` (pair.lua), `editing.trim-on-save` (editops.lua), `autosave.interval-ms` (autosave.lua), `window.panel-height` + `window.min-height` - (window.lua), and `terminal.default-profile` + + (window.lua), `terminal.default-profile` + `terminal.scrollback-rows` + `terminal.escape-key` (terminal.lua, - #173). Everything else a user might set — theme, fonts, LSP + #173), and `lean.abbrev` (lean_input.lua, Arc 8 Stage 4b) — a + `live` boolean read against the typed edit's SOURCE buffer, the + `editing.auto-pair` shape including its correction to resolve + `rec.buffer` rather than the active buffer. Everything else a user might set — theme, fonts, LSP server config, killring size, recentf/saveplace/desktop enables, pair sets, comment strings, `pmacs.parse.*` — lives in raw Lua outside the registry and is therefore invisible to `describe-setting` @@ -1076,7 +1079,7 @@ layering, provenance, and adoption have not followed.** - **No persistence**: settings changed at runtime do not survive restart (the `custom-file` split-brain question is a named deferral). - The three-level separation holds in principle today (registry / - hooks+keymaps / packages), but with eight settings registered, level 1 + hooks+keymaps / packages), but with nine settings registered, level 1 is effectively empty — users need executable Lua for nearly every ordinary preference, which is the exact failure the section warns about. diff --git a/builtin/runtime/lean_abbrev.lua b/builtin/runtime/lean_abbrev.lua new file mode 100644 index 0000000..769c9d4 --- /dev/null +++ b/builtin/runtime/lean_abbrev.lua @@ -0,0 +1,1883 @@ +-- lean_abbrev.lua --- VENDORED DATA. Do not edit by hand. +-- +-- The Lean 4 abbreviation table, generated from: +-- +-- repo: https://github.com/leanprover/vscode-lean4 +-- path: lean4-unicode-input/src/abbreviations.json +-- commit: 17d1d08 +-- license: Apache-2.0 +-- entries: 1855 (26 carry $CURSOR) +-- source: 36861 bytes +-- +-- Regenerate with: +-- +-- scripts/regen-lean-abbrev 17d1d08 +-- +-- An ORDERED SEQUENCE, not a map: upstream resolves equal-length ties +-- by source declaration order (101 prefixes depend on it), and a +-- `pairs`-iterated Lua map cannot express that. The file's own line +-- order is the audit trail. Consumers must not reorder it. +-- +-- Not fetched at runtime and not a package dependency: the input method +-- has to work offline and on first launch. Upkeep is a documented +-- manual process — see docs/lean4-mode-framing.md Q#LN11. + +pmacs = pmacs or {} + +pmacs.lean_abbrev = { + { "{}", "{$CURSOR}" }, + { "{}_", "{$CURSOR}_" }, + { "{{}}", "⦃$CURSOR⦄" }, + { "[]", "[$CURSOR]" }, + { "[]_", "[$CURSOR]_" }, + { "[[]]", "⟦$CURSOR⟧" }, + { "<>", "⟨$CURSOR⟩" }, + { "()", "($CURSOR)" }, + { "()_", "($CURSOR)_" }, + { "^()", "⁽$CURSOR⁾" }, + { "_()", "₍$CURSOR₎" }, + { "([])'", "⟮$CURSOR⟯" }, + { "(())", "⸨$CURSOR⸩" }, + { "f<>", "‹$CURSOR›" }, + { "f<<>>", "«$CURSOR»" }, + { "h<>", "❰$CURSOR❱" }, + { "[--]", "⁅$CURSOR⁆" }, + { "||||", "‖$CURSOR‖" }, + { "nnnorm", "‖$CURSOR‖₊" }, + { "norm", "‖$CURSOR‖" }, + { "floor", "⌊$CURSOR⌋" }, + { "ceil", "⌈$CURSOR⌉" }, + { "nfloor", "⌊$CURSOR⌋₊" }, + { "nceil", "⌈$CURSOR⌉₊" }, + { "s[]", "⦋$CURSOR⦌" }, + { "simplex", "⦋$CURSOR⦌" }, + { "\\", "\\" }, + { "a", "α" }, + { "b", "β" }, + { "c", "χ" }, + { "d", "↓" }, + { "e", "ε" }, + { "g", "γ" }, + { "i", "∩" }, + { "m", "μ" }, + { "n", "\\n" }, + { "o", "∘" }, + { "p", "Π" }, + { "t", "▸" }, + { "r", "→" }, + { "u", "↑" }, + { "v", "∨" }, + { "x", "×" }, + { "-", "⁻¹" }, + { "~", "∼" }, + { ".", "·" }, + { "*", "⋆" }, + { "!", "¬" }, + { "?", "¿" }, + { "1", "₁" }, + { "2", "₂" }, + { "3", "₃" }, + { "4", "₄" }, + { "5", "₅" }, + { "6", "₆" }, + { "7", "₇" }, + { "8", "₈" }, + { "9", "₉" }, + { "0", "₀" }, + { "l", "←" }, + { "<", "⟨" }, + { ">", "⟩" }, + { "O", "Ø" }, + { "&", "⅋" }, + { "A", "𝔸" }, + { "C", "ℂ" }, + { "D", "Δ" }, + { "F", "𝔽" }, + { "G", "Γ" }, + { "H", "ℍ" }, + { "I", "⋂" }, + { "I0", "⋂₀" }, + { "K", "𝕂" }, + { "L", "Λ" }, + { "N", "ℕ" }, + { "P", "Π" }, + { "Q", "ℚ" }, + { "R", "ℝ" }, + { "S", "Σ" }, + { "U", "⋃" }, + { "U0", "⋃₀" }, + { "Z", "ℤ" }, + { "#", "♯" }, + { ":", "∶" }, + { "|", "∣" }, + { "rw", "▸" }, + { "coe", "↑" }, + { "be", "β" }, + { "ga", "γ" }, + { "de", "δ" }, + { "ep", "ε" }, + { "ze", "ζ" }, + { "et", "η" }, + { "th", "θ" }, + { "io", "ι" }, + { "ka", "κ" }, + { "la", "λ" }, + { "mu", "μ" }, + { "nu", "ν" }, + { "xi", "ξ" }, + { "pi", "π" }, + { "rh", "ρ" }, + { "vsi", "ς" }, + { "si", "σ" }, + { "ta", "τ" }, + { "ph", "φ" }, + { "ch", "χ" }, + { "ps", "ψ" }, + { "om", "ω" }, + { "`A", "À" }, + { "'A", "Á" }, + { "^{A}", "Â" }, + { "~A", "Ã" }, + { "\"A", "Ä" }, + { "-{A}", "Ā" }, + { "cC", "Ç" }, + { "`E", "È" }, + { "'E", "É" }, + { "^{E}", "Ê" }, + { "\"E", "Ë" }, + { "-{E}", "Ē" }, + { "`I", "Ì" }, + { "'I", "Í" }, + { "^{I}", "Î" }, + { "\"I", "Ï" }, + { "-{I}", "Ī" }, + { "~N", "Ñ" }, + { "`O", "Ò" }, + { "'O", "Ó" }, + { "^{O}", "Ô" }, + { "~O", "Õ" }, + { "\"O", "Ö" }, + { "/O", "Ø" }, + { "-{O}", "Ō" }, + { "`U", "Ù" }, + { "'U", "Ú" }, + { "^{U}", "Û" }, + { "\"U", "Ü" }, + { "-{U}", "Ū" }, + { "'Y", "Ý" }, + { "`a", "à" }, + { "'a", "á" }, + { "^{a}", "â" }, + { "~a", "ã" }, + { "\"a", "ä" }, + { "-{a}", "ā" }, + { "cc", "ç" }, + { "`e", "è" }, + { "'e", "é" }, + { "^{e}", "ê" }, + { "\"e", "ë" }, + { "-{e}", "ē" }, + { "`i", "ì" }, + { "'i", "í" }, + { "^{i}", "î" }, + { "\"i", "ï" }, + { "-{i}", "ī" }, + { "~{n}", "ñ" }, + { "`o", "ò" }, + { "'o", "ó" }, + { "^{o}", "ô" }, + { "~o", "õ" }, + { "\"o", "ö" }, + { "/o", "ø" }, + { "-{o}", "ō" }, + { "`u", "ù" }, + { "'u", "ú" }, + { "^{u}", "û" }, + { "\"u", "ü" }, + { "-{u}", "ū" }, + { "'y", "ý" }, + { "\"y", "ÿ" }, + { "/L", "Ł" }, + { "note", "♩" }, + { "not", "¬" }, + { "notin", "∉" }, + { "notlt", "≮" }, + { "nomisma", "𐆎" }, + { "nin", "∉" }, + { "nni", "∌" }, + { "ni", "∋" }, + { "nattrans", "⟹" }, + { "nat_trans", "⟹" }, + { "natural", "♮" }, + { "nat", "ℕ" }, + { "naira", "₦" }, + { "nabla", "∇" }, + { "napprox", "≉" }, + { "numero", "№" }, + { "nLeftarrow", "⇍" }, + { "nLeftrightarrow", "⇎" }, + { "nRightarrow", "⇏" }, + { "nVDash", "⊯" }, + { "nVdash", "⊮" }, + { "ncong", "≇" }, + { "nearrow", "↗" }, + { "neg", "¬" }, + { "nequiv", "≢" }, + { "neq", "≠" }, + { "nexists", "∄" }, + { "ne", "≠" }, + { "ngeqq", "≱" }, + { "ngeqslant", "≱" }, + { "ngeq", "≱" }, + { "ngtr", "≯" }, + { "nleftarrow", "↚" }, + { "nleftrightarrow", "↮" }, + { "nleqq", "≰" }, + { "nleqslant", "≰" }, + { "nleq", "≰" }, + { "nless", "≮" }, + { "nmid", "∤" }, + { "nparallel", "∦" }, + { "npreceq", "⋠" }, + { "nprec", "⊀" }, + { "nrightarrow", "↛" }, + { "nshortmid", "∤" }, + { "nsimeq", "≄" }, + { "nsim", "≁" }, + { "nsubseteqq", "⊈" }, + { "nsubseteq", "⊈" }, + { "nsubset", "⊄" }, + { "nsucceq", "⋡" }, + { "nsucc", "⊁" }, + { "nsupseteqq", "⊉" }, + { "nsupseteq", "⊉" }, + { "nsupset", "⊅" }, + { "ntrianglelefteq", "⋬" }, + { "ntriangleleft", "⋪" }, + { "ntrianglerighteq", "⋭" }, + { "ntriangleright", "⋫" }, + { "nvDash", "⊭" }, + { "nvdash", "⊬" }, + { "nwarrow", "↖" }, + { "eqn", "≠" }, + { "equiv", "≃" }, + { "eqcirc", "≖" }, + { "eqcolon", "≕" }, + { "eqslantgtr", "⋝" }, + { "eqslantless", "⋜" }, + { "entails", "⊢" }, + { "en", "–" }, + { "exn", "∄" }, + { "exists", "∃" }, + { "ex", "∃" }, + { "emptyset", "∅" }, + { "empty", "∅" }, + { "em", "—" }, + { "epsilon", "ε" }, + { "eps", "ε" }, + { "euro", "€" }, + { "eta", "η" }, + { "ell", "ℓ" }, + { "iso", "≅" }, + { "in", "∈" }, + { "inn", "∉" }, + { "inter", "∩" }, + { "intercal", "⊺" }, + { "intersection", "∩" }, + { "integral", "∫" }, + { "integral-", "⨍" }, + { "int", "ℤ" }, + { "inv", "⁻¹" }, + { "increment", "∆" }, + { "inf", "⊓" }, + { "infi", "⨅" }, + { "infty", "∞" }, + { "iff", "↔" }, + { "imp", "→" }, + { "imath", "ı" }, + { "iota", "ι" }, + { "=n", "≠" }, + { "==n", "≢" }, + { "===", "≣" }, + { "==>", "⟹" }, + { "==", "≡" }, + { "=:", "≕" }, + { "=o", "≗" }, + { "=>n", "⇏" }, + { "=>", "⇒" }, + { "~n", "≁" }, + { "~~n", "≉" }, + { "~~~", "≋" }, + { "~~-", "≊" }, + { "~~", "≈" }, + { "~-n", "≄" }, + { "~-", "≃" }, + { "~=n", "≇" }, + { "~=", "≅" }, + { "homotopy", "∼" }, + { "hom", "⟶" }, + { "hori", "ϩ" }, + { "hookleftarrow", "↩" }, + { "hookrightarrow", "↪" }, + { "hryvnia", "₴" }, + { "heta", "ͱ" }, + { "heartsuit", "♥" }, + { "hbar", "ℏ" }, + { ":~", "∻" }, + { ":=", "≔" }, + { "::-", "∺" }, + { "::", "∷" }, + { "-~", "≂" }, + { "-|", "⊣" }, + { "-1", "⁻¹" }, + { "^-1", "⁻¹" }, + { "-2", "⁻²" }, + { "-3", "⁻³" }, + { "-:", "∹" }, + { "->n", "↛" }, + { "->", "→" }, + { "-->", "⟶" }, + { "---", "─" }, + { "--=", "═" }, + { "--_", "━" }, + { "--.", "╌" }, + { "-o", "⊸" }, + { ".=.", "≑" }, + { ".=", "≐" }, + { ".+", "∔" }, + { ".-", "∸" }, + { "...", "⋯" }, + { "(=", "≘" }, + { "(b", "⟅" }, + { "and=", "≙" }, + { "and", "∧" }, + { "an", "∧" }, + { "angle", "∠" }, + { "rightangle", "∟" }, + { "angstrom", "Å" }, + { "all", "∀" }, + { "allf", "∀ᶠ" }, + { "all^f", "∀ᶠ" }, + { "allm", "∀ᵐ" }, + { "all^m", "∀ᵐ" }, + { "alpha", "α" }, + { "aleph", "ℵ" }, + { "aleph0", "ℵ₀" }, + { "asterisk", "⁎" }, + { "ast", "∗" }, + { "asymp", "≍" }, + { "apl", "⌶" }, + { "approxeq", "≊" }, + { "approx", "≈" }, + { "aa", "å" }, + { "ae", "æ" }, + { "austral", "₳" }, + { "amalg", "∐" }, + { "average", "⨍" }, + { "-int", "⨍" }, + { "or=", "≚" }, + { "ordfeminine", "ª" }, + { "ordmasculine", "º" }, + { "or", "∨" }, + { "oplus", "⊕" }, + { "od", "ᵒᵈ" }, + { "orderdual", "ᵒᵈ" }, + { "addopposite", "ᵃᵒᵖ" }, + { "aop", "ᵃᵒᵖ" }, + { "mulopposite", "ᵐᵒᵖ" }, + { "mop", "ᵐᵒᵖ" }, + { "opposite", "ᵒᵖ" }, + { "op", "ᵒᵖ" }, + { "o+", "⊕" }, + { "o--", "⊖" }, + { "o-", "⊝" }, + { "ox", "⊗" }, + { "o/", "⊘" }, + { "o.", "⊙" }, + { "oo", "⊚" }, + { "o*", "∘*" }, + { "o=", "⊜" }, + { "oe", "œ" }, + { "octagonal", "🛑" }, + { "ohm", "Ω" }, + { "ounce", "℥" }, + { "omega", "ω" }, + { "omicron", "ο" }, + { "ominus", "⊖" }, + { "odot", "⊙" }, + { "oint", "∮" }, + { "oiint", "∯" }, + { "oslash", "⊘" }, + { "otimes", "⊗" }, + { "tensorproduct", "⊗" }, + { "pitensorproduct", "⨂" }, + { "tensorpower", "⨂" }, + { "pd", "∂" }, + { "*=", "≛" }, + { "t=", "≜" }, + { "tint", "∯" }, + { "transport", "▹" }, + { "trans", "▹" }, + { "triangledown", "▿" }, + { "trianglelefteq", "⊴" }, + { "triangleleft", "◃" }, + { "triangleq", "≜" }, + { "trianglerighteq", "⊵" }, + { "triangleright", "▹" }, + { "triangle", "▵" }, + { "tr", "⬝" }, + { "tb", "◂" }, + { "twoheadleftarrow", "↞" }, + { "twoheadrightarrow", "↠" }, + { "tw", "◃" }, + { "tie", "⁀" }, + { "times", "×" }, + { "theta", "θ" }, + { "therefore", "∴" }, + { "thickapprox", "≈" }, + { "thicksim", "∼" }, + { "telephone", "℡" }, + { "tenge", "₸" }, + { "textmusicalnote", "♪" }, + { "textmu", "µ" }, + { "textfractionsolidus", "⁄" }, + { "textbaht", "฿" }, + { "textdied", "✝" }, + { "textdiscount", "⁒" }, + { "textcolonmonetary", "₡" }, + { "textcircledP", "℗" }, + { "textwon", "₩" }, + { "textnaira", "₦" }, + { "textnumero", "№" }, + { "textpeso", "₱" }, + { "textpertenthousand", "‱" }, + { "textlira", "₤" }, + { "textlquill", "⁅" }, + { "textrecipe", "℞" }, + { "textreferencemark", "※" }, + { "textrquill", "⁆" }, + { "textinterrobang", "‽" }, + { "textestimated", "℮" }, + { "textopenbullet", "◦" }, + { "tugrik", "₮" }, + { "tau", "τ" }, + { "top", "⊤" }, + { "to", "→" }, + { "to0", "→₀" }, + { "r0", "→₀" }, + { "to_0", "→₀" }, + { "r_0", "→₀" }, + { "finsupp", "→₀" }, + { "to1", "→₁" }, + { "r1", "→₁" }, + { "to_1", "→₁" }, + { "r_1", "→₁" }, + { "l1", "→₁" }, + { "to1s", "→₁ₛ" }, + { "r1s", "→₁ₛ" }, + { "to_1s", "→₁ₛ" }, + { "r_1s", "→₁ₛ" }, + { "l1simplefunc", "→₁ₛ" }, + { "toa", "→ₐ" }, + { "ra", "→ₐ" }, + { "to_a", "→ₐ" }, + { "r_a", "→ₐ" }, + { "alghom", "→ₐ" }, + { "tob", "→ᵇ" }, + { "rb", "→ᵇ" }, + { "to^b", "→ᵇ" }, + { "r^b", "→ᵇ" }, + { "boundedcontinuousfunction", "→ᵇ" }, + { "tol", "→ₗ" }, + { "rl", "→ₗ" }, + { "to_l", "→ₗ" }, + { "r_l", "→ₗ" }, + { "linearmap", "→ₗ" }, + { "tosl", "→ₛₗ" }, + { "rsl", "→ₛₗ" }, + { "to_sl", "→ₛₗ" }, + { "r_sl", "→ₛₗ" }, + { "semilinearmap", "→ₛₗ" }, + { "tom", "→ₘ" }, + { "rm", "→ₘ" }, + { "to_m", "→ₘ" }, + { "r_m", "→ₘ" }, + { "aeeqfun", "→ₘ" }, + { "rp", "→ₚ" }, + { "to_p", "→ₚ" }, + { "r_p", "→ₚ" }, + { "dfinsupp", "→ₚ" }, + { "tos", "→ₛ" }, + { "rs", "→ₛ" }, + { "to_s", "→ₛ" }, + { "r_s", "→ₛ" }, + { "simplefunc", "→ₛ" }, + { "heyting", "⇨" }, + { "himp", "⇨" }, + { "hnot", "￢" }, + { "covers", "⋖" }, + { "covby", "⋖" }, + { "wcovby", "⩿" }, + { "wcovers", "⩿" }, + { "def=", "≝" }, + { "defs", "≙" }, + { "degree", "°" }, + { "dei", "ϯ" }, + { "delta", "δ" }, + { "doteqdot", "≑" }, + { "doteq", "≐" }, + { "dotplus", "∔" }, + { "dotsquare", "⊡" }, + { "dot", "·" }, + { "dong", "₫" }, + { "downarrow", "↓" }, + { "downdownarrows", "⇊" }, + { "downleftharpoon", "⇃" }, + { "downrightharpoon", "⇂" }, + { "dr-", "↘" }, + { "dr=", "⇘" }, + { "drachma", "₯" }, + { "dr", "↘" }, + { "dl-", "↙" }, + { "dl=", "⇙" }, + { "dl", "↙" }, + { "d-2", "⇊" }, + { "d-u-", "⇵" }, + { "d-|", "↧" }, + { "d-", "↓" }, + { "d==", "⟱" }, + { "d=", "⇓" }, + { "dd-", "↡" }, + { "ddagger", "‡" }, + { "ddag", "‡" }, + { "ddots", "⋱" }, + { "dz", "↯" }, + { "dib", "◆" }, + { "diw", "◇" }, + { "di.", "◈" }, + { "die", "⚀" }, + { "division", "÷" }, + { "divideontimes", "⋇" }, + { "div", "÷" }, + { "diameter", "⌀" }, + { "diamondsuit", "♢" }, + { "diamond", "⋄" }, + { "digamma", "ϝ" }, + { "di", "◆" }, + { "dagger", "†" }, + { "dag", "†" }, + { "daleth", "ℸ" }, + { "dashv", "⊣" }, + { "dh", "ð" }, + { "dvd", "∣" }, + { "m=", "≞" }, + { "meet", "⊓" }, + { "member", "∈" }, + { "mem", "∈" }, + { "measuredangle", "∡" }, + { "ma", "↦" }, + { "mapsto", "↦" }, + { "male", "♂" }, + { "maltese", "✠" }, + { "manat", "₼" }, + { "mathscr{I}", "ℐ" }, + { "minus", "−" }, + { "mill", "₥" }, + { "micro", "µ" }, + { "mid", "∣" }, + { "multiplication", "×" }, + { "multimap", "⊸" }, + { "mho", "℧" }, + { "models", "⊧" }, + { "mp", "∓" }, + { "?=", "≟" }, + { "??", "⁇" }, + { "?!", "‽" }, + { "prohibited", "🛇" }, + { "prod", "∏" }, + { "propto", "∝" }, + { "precapprox", "≾" }, + { "preceq", "≼" }, + { "precnapprox", "⋨" }, + { "precnsim", "⋨" }, + { "precsim", "≾" }, + { "prec", "≺" }, + { "preim", "⁻¹'" }, + { "preimage", "⁻¹'" }, + { "prime", "′" }, + { "pr", "↣" }, + { "powerset", "𝒫" }, + { "pounds", "£" }, + { "pound", "£" }, + { "pab", "▰" }, + { "paw", "▱" }, + { "partnership", "㉐" }, + { "partial", "∂" }, + { "paragraph", "¶" }, + { "parallel", "∥" }, + { "pa", "▰" }, + { "pm", "±" }, + { "perp", "⟂" }, + { "^perp", "ᗮ" }, + { "permil", "‰" }, + { "per", "⅌" }, + { "peso", "₱" }, + { "peseta", "₧" }, + { "pilcrow", "¶" }, + { "pitchfork", "⋔" }, + { "psi", "ψ" }, + { "phi", "φ" }, + { "leqn", "≰" }, + { "leqq", "≦" }, + { "leqslant", "≤" }, + { "leq", "≤" }, + { "len", "≰" }, + { "leadsto", "↝" }, + { "leftarrowtail", "↢" }, + { "leftarrow", "←" }, + { "leftharpoondown", "↽" }, + { "leftharpoonup", "↼" }, + { "leftleftarrows", "⇇" }, + { "leftrightarrows", "⇆" }, + { "leftrightarrow", "↔" }, + { "leftrightharpoons", "⇋" }, + { "leftrightsquigarrow", "↭" }, + { "leftthreetimes", "⋋" }, + { "lessapprox", "≲" }, + { "lessdot", "⋖" }, + { "lesseqgtr", "⋚" }, + { "lesseqqgtr", "⋚" }, + { "lessgtr", "≶" }, + { "lesssim", "≲" }, + { "le", "≤" }, + { "lub", "⊔" }, + { "lr--", "⟷" }, + { "lr-n", "↮" }, + { "lr-", "↔" }, + { "lr=n", "⇎" }, + { "lr=", "⇔" }, + { "lr~", "↭" }, + { "lrcorner", "⌟" }, + { "lr", "↔" }, + { "l-2", "⇇" }, + { "l-r-", "⇆" }, + { "l--", "⟵" }, + { "l-n", "↚" }, + { "l-|", "↤" }, + { "l->", "↢" }, + { "l-", "←" }, + { "l==", "⇚" }, + { "l=n", "⇍" }, + { "l=", "⇐" }, + { "l~", "↜" }, + { "ll-", "↞" }, + { "llcorner", "⌞" }, + { "llbracket", "〚" }, + { "ll", "≪" }, + { "lbag", "⟅" }, + { "lambda", "λ" }, + { "lamda", "λ" }, + { "lam", "λ" }, + { "lari", "₾" }, + { "langle", "⟨" }, + { "lira", "₤" }, + { "lceil", "⌈" }, + { "ldots", "…" }, + { "ldq", "“" }, + { "ldata", "《" }, + { "lfloor", "⌊" }, + { "lf", "⧏" }, + { "<|", "⧏" }, + { "lhd", "◁" }, + { "lnapprox", "⋦" }, + { "lneqq", "≨" }, + { "lneq", "≨" }, + { "lnsim", "⋦" }, + { "lnot", "¬" }, + { "longleftarrow", "⟵" }, + { "longleftrightarrow", "⟷" }, + { "longrightarrow", "⟶" }, + { "looparrowleft", "↫" }, + { "looparrowright", "↬" }, + { "lozenge", "✧" }, + { "lq", "‘" }, + { "ltimes", "⋉" }, + { "lvertneqq", "≨" }, + { "geqn", "≱" }, + { "geqq", "≧" }, + { "geqslant", "≥" }, + { "geq", "≥" }, + { "gen", "≱" }, + { "gets", "←" }, + { "ge", "≥" }, + { "glb", "⊓" }, + { "glqq", "„" }, + { "glq", "‚" }, + { "guarani", "₲" }, + { "gangia", "ϫ" }, + { "gamma", "γ" }, + { "ggg", "⋙" }, + { "gg", "≫" }, + { "gimel", "ℷ" }, + { "gnapprox", "⋧" }, + { "gneqq", "≩" }, + { "gneq", "≩" }, + { "gnsim", "⋧" }, + { "gtrapprox", "≳" }, + { "gtrdot", "⋗" }, + { "gtreqless", "⋛" }, + { "gtreqqless", "⋛" }, + { "gtrless", "≷" }, + { "gtrsim", "≳" }, + { "gvertneqq", "≩" }, + { "grqq", "“" }, + { "grq", "‘" }, + { "<=n", "≰" }, + { "<=>n", "⇎" }, + { "<=>", "⇔" }, + { "<=", "≤" }, + { "<~nn", "≴" }, + { "<~n", "⋦" }, + { "<~", "≲" }, + { "<:", "⋖" }, + { ":>", "⋗" }, + { "<->n", "↮" }, + { "<->", "↔" }, + { "<-->", "⟷" }, + { "<--", "⟵" }, + { "<-n", "↚" }, + { "<-", "←" }, + { "<<", "⟪" }, + { ">=n", "≱" }, + { ">=", "≥" }, + { ">n", "≯" }, + { ">~nn", "≵" }, + { ">~n", "⋧" }, + { ">~", "≳" }, + { ">>", "⟫" }, + { "root", "√" }, + { "scissor", "✂" }, + { "ssubn", "⊄" }, + { "ssub", "⊂" }, + { "ssupn", "⊅" }, + { "ssup", "⊃" }, + { "ssqub", "⊏" }, + { "ssqup", "⊐" }, + { "ss", "⊆" }, + { "subn", "⊈" }, + { "subseteqq", "⊆" }, + { "subseteq", "⊆" }, + { "subsetneqq", "⊊" }, + { "subsetneq", "⊊" }, + { "subset", "⊆" }, + { "ssubset", "⊂" }, + { "sub", "⊆" }, + { "supn", "⊉" }, + { "supseteqq", "⊇" }, + { "supseteq", "⊇" }, + { "supsetneqq", "⊋" }, + { "supsetneq", "⊋" }, + { "supset", "⊇" }, + { "ssupset", "⊃" }, + { "sUnion", "⋃₀" }, + { "sInter", "⋂₀" }, + { "sup", "⊔" }, + { "supr", "⨆" }, + { "surd3", "∛" }, + { "surd4", "∜" }, + { "surd", "√" }, + { "succapprox", "≿" }, + { "succcurlyeq", "≽" }, + { "succeq", "≽" }, + { "succnapprox", "⋩" }, + { "succnsim", "⋩" }, + { "succsim", "≿" }, + { "succ", "≻" }, + { "sum", "∑" }, + { "specializes", "⤳" }, + { "~>", "⤳" }, + { "squbn", "⋢" }, + { "squb", "⊑" }, + { "squpn", "⋣" }, + { "squp", "⊒" }, + { "square", "□" }, + { "squigarrowright", "⇝" }, + { "sqb", "■" }, + { "sqw", "□" }, + { "sq.", "▣" }, + { "sqo", "▢" }, + { "sqcap", "⊓" }, + { "sqcup", "⊔" }, + { "sqrt", "√" }, + { "sqsubseteq", "⊑" }, + { "sqsubset", "⊏" }, + { "sqsupseteq", "⊒" }, + { "sqsupset", "⊐" }, + { "sq", "◾" }, + { "sy", "⁻¹" }, + { "symmdiff", "∆" }, + { "st4", "✦" }, + { "st6", "✶" }, + { "st8", "✴" }, + { "st12", "✹" }, + { "stigma", "ϛ" }, + { "star", "⋆" }, + { "straightphi", "φ" }, + { "st", "⋆" }, + { "spesmilo", "₷" }, + { "span", "∙" }, + { "spadesuit", "♠" }, + { "sphericalangle", "∢" }, + { "section", "§" }, + { "searrow", "↘" }, + { "setminus", "\\" }, + { "san", "ϻ" }, + { "sampi", "ϡ" }, + { "shortmid", "∣" }, + { "sho", "ϸ" }, + { "shima", "ϭ" }, + { "shei", "ϣ" }, + { "sharp", "♯" }, + { "sigma", "σ" }, + { "simeq", "≃" }, + { "sim", "∼" }, + { "sbs", "﹨" }, + { "smallamalg", "∐" }, + { "smallsetminus", "∖" }, + { "smallsmile", "⌣" }, + { "smile", "⌣" }, + { "smul", "•" }, + { "swarrow", "↙" }, + { "Tr", "◀" }, + { "Tb", "◀" }, + { "Tw", "◁" }, + { "Tau", "Τ" }, + { "Theta", "Θ" }, + { "TH", "Þ" }, + { "union", "∪" }, + { "undertie", "‿" }, + { "uncertainty", "⯑" }, + { "un", "∪" }, + { "u+", "⊎" }, + { "u.", "⊍" }, + { "ud-|", "↨" }, + { "ud-", "↕" }, + { "ud=", "⇕" }, + { "ud", "↕" }, + { "ul-", "↖" }, + { "ul=", "⇖" }, + { "ulcorner", "⌜" }, + { "ul", "↖" }, + { "ur-", "↗" }, + { "ur=", "⇗" }, + { "urcorner", "⌝" }, + { "ur", "↗" }, + { "u-2", "⇈" }, + { "u-d-", "⇅" }, + { "u-|", "↥" }, + { "u-", "↑" }, + { "u==", "⟰" }, + { "u=", "⇑" }, + { "uu-", "↟" }, + { "upsilon", "υ" }, + { "uparrow", "↑" }, + { "updownarrow", "↕" }, + { "upleftharpoon", "↿" }, + { "uplus", "⊎" }, + { "uprightharpoon", "↾" }, + { "upuparrows", "⇈" }, + { "And", "⋀" }, + { "AA", "Å" }, + { "AE", "Æ" }, + { "Alpha", "Α" }, + { "Or", "⋁" }, + { "O+", "⨁" }, + { "directsum", "⨁" }, + { "Ox", "⨂" }, + { "O.", "⨀" }, + { "O*", "⍟" }, + { "OE", "Œ" }, + { "Omega", "Ω" }, + { "Omicron", "Ο" }, + { "Int", "ℤ" }, + { "Inter", "⋂" }, + { "bInter", "⋂" }, + { "Iota", "Ι" }, + { "Im", "ℑ" }, + { "Un", "⋃" }, + { "Union", "⋃" }, + { "bUnion", "⋃" }, + { "U+", "⨄" }, + { "U.", "⨃" }, + { "Upsilon", "Υ" }, + { "Uparrow", "⇑" }, + { "Updownarrow", "⇕" }, + { "Gl-", "ƛ" }, + { "Gl", "λ" }, + { "Gangia", "Ϫ" }, + { "Gamma", "Γ" }, + { "Glb", "⨅" }, + { "Ga", "α" }, + { "GA", "Α" }, + { "Gb", "β" }, + { "GB", "Β" }, + { "Gg", "γ" }, + { "GG", "Γ" }, + { "Gd", "δ" }, + { "GD", "Δ" }, + { "Ge", "ε" }, + { "GE", "Ε" }, + { "Gz", "ζ" }, + { "GZ", "Ζ" }, + { "Gth", "θ" }, + { "Gt", "τ" }, + { "GTH", "Θ" }, + { "GT", "Τ" }, + { "Gi", "ι" }, + { "GI", "Ι" }, + { "Gk", "κ" }, + { "GK", "Κ" }, + { "GL", "Λ" }, + { "Gm", "μ" }, + { "GM", "Μ" }, + { "Gn", "ν" }, + { "GN", "Ν" }, + { "Gx", "ξ" }, + { "GX", "Ξ" }, + { "Gr", "ρ" }, + { "GR", "Ρ" }, + { "Gs", "σ" }, + { "GS", "Σ" }, + { "Gu", "υ" }, + { "GU", "Υ" }, + { "Gf", "φ" }, + { "GF", "Φ" }, + { "Gc", "χ" }, + { "GC", "Χ" }, + { "Gp", "ψ" }, + { "GP", "Ψ" }, + { "Go", "ω" }, + { "GO", "Ω" }, + { "Inf", "⨅" }, + { "Join", "⨆" }, + { "Lub", "⨆" }, + { "Lambda", "Λ" }, + { "Lamda", "Λ" }, + { "Leftarrow", "⇐" }, + { "Leftrightarrow", "⇔" }, + { "Letter", "✉" }, + { "Lleftarrow", "⇚" }, + { "Ll", "⋘" }, + { "Longleftarrow", "⇐" }, + { "Longleftrightarrow", "⇔" }, + { "Longrightarrow", "⇒" }, + { "Meet", "⨅" }, + { "Sup", "⨆" }, + { "Sqcap", "⨅" }, + { "Sqcup", "⨆" }, + { "Lsh", "↰" }, + { "|-n", "⊬" }, + { "|-", "⊢" }, + { "|=n", "⊭" }, + { "|=", "⊨" }, + { "|->", "↦" }, + { "|=>", "⇰" }, + { "||-n", "⊮" }, + { "||-", "⊩" }, + { "||=n", "⊯" }, + { "||=", "⊫" }, + { "|||-", "⊪" }, + { "||", "‖" }, + { "fuzzy", "‖" }, + { "|n", "∤" }, + { "Com", "ℂ" }, + { "Chi", "Χ" }, + { "Cap", "⋒" }, + { "Cup", "⋓" }, + { "cul", "⌜" }, + { "cuL", "⌈" }, + { "currency", "¤" }, + { "curlyeqprec", "⋞" }, + { "curlyeqsucc", "⋟" }, + { "curlypreceq", "≼" }, + { "curlyvee", "⋎" }, + { "curlywedge", "⋏" }, + { "curvearrowleft", "↶" }, + { "curvearrowright", "↷" }, + { "cur", "⌝" }, + { "cuR", "⌉" }, + { "cup", "∪" }, + { "cu", "⌜" }, + { "cll", "⌞" }, + { "clL", "⌊" }, + { "clr", "⌟" }, + { "clR", "⌋" }, + { "clubsuit", "♣" }, + { "cl", "⌞" }, + { "construction", "🚧" }, + { "cong", "≅" }, + { "con", "⬝" }, + { "compl", "ᶜ" }, + { "complement", "ᶜ" }, + { "complementprefix", "∁" }, + { "Complement", "∁" }, + { "comp", "∘" }, + { "com", "ℂ" }, + { "coloneq", "≔" }, + { "colon", "₡" }, + { "copyright", "©" }, + { "cdots", "⋯" }, + { "cdot", "·" }, + { "cib", "●" }, + { "ciw", "○" }, + { "ci..", "◌" }, + { "ci.", "◎" }, + { "ciO", "◯" }, + { "circeq", "≗" }, + { "circlearrowleft", "↺" }, + { "circlearrowright", "↻" }, + { "circledR", "®" }, + { "circledS", "Ⓢ" }, + { "circledast", "⊛" }, + { "circledcirc", "⊚" }, + { "circleddash", "⊝" }, + { "circ", "∘" }, + { "ci", "●" }, + { "centerdot", "·" }, + { "cent", "¢" }, + { "cedi", "₵" }, + { "celsius", "℃" }, + { "ce", "ȩ" }, + { "checkmark", "✓" }, + { "chi", "χ" }, + { "cruzeiro", "₢" }, + { "caution", "☡" }, + { "cap", "∩" }, + { "qed", "∎" }, + { "quot", "⧸" }, + { "bigsolidus", "⧸" }, + { "/", "⧸" }, + { "+ ", "⊹" }, + { "b+", "⊞" }, + { "b-", "⊟" }, + { "bx", "⊠" }, + { "b.", "⊡" }, + { "bn", "ℕ" }, + { "bz", "ℤ" }, + { "bq", "ℚ" }, + { "brokenbar", "¦" }, + { "br", "ℝ" }, + { "bc", "ℂ" }, + { "bp", "ℙ" }, + { "bb", "𝔹" }, + { "bsum", "⅀" }, + { "b0", "𝟘" }, + { "b1", "𝟙" }, + { "b2", "𝟚" }, + { "b3", "𝟛" }, + { "b4", "𝟜" }, + { "b5", "𝟝" }, + { "b6", "𝟞" }, + { "b7", "𝟟" }, + { "b8", "𝟠" }, + { "b9", "𝟡" }, + { "sb0", "𝟬" }, + { "sb1", "𝟭" }, + { "sb2", "𝟮" }, + { "sb3", "𝟯" }, + { "sb4", "𝟰" }, + { "sb5", "𝟱" }, + { "sb6", "𝟲" }, + { "sb7", "𝟳" }, + { "sb8", "𝟴" }, + { "sb9", "𝟵" }, + { "bub", "•" }, + { "buw", "◦" }, + { "but", "‣" }, + { "bumpeq", "≏" }, + { "bu", "•" }, + { "biohazard", "☣" }, + { "bihimp", "⇔" }, + { "bigcap", "⋂" }, + { "bigcirc", "◯" }, + { "bigcoprod", "∐" }, + { "bigcup", "⋃" }, + { "bigglb", "⨅" }, + { "biginf", "⨅" }, + { "bigjoin", "⨆" }, + { "biglub", "⨆" }, + { "bigmeet", "⨅" }, + { "bigsqcap", "⨅" }, + { "bigsqcup", "⨆" }, + { "bigstar", "★" }, + { "bigsup", "⨆" }, + { "bigtriangledown", "▽" }, + { "bigtriangleup", "△" }, + { "bigvee", "⋁" }, + { "bigwedge", "⋀" }, + { "beta", "β" }, + { "beth", "ℶ" }, + { "between", "≬" }, + { "because", "∵" }, + { "backcong", "≌" }, + { "backepsilon", "∍" }, + { "backprime", "‵" }, + { "backsimeq", "⋍" }, + { "backsim", "∽" }, + { "barwedge", "⊼" }, + { "blacklozenge", "✦" }, + { "blacksquare", "▪" }, + { "blacksmiley", "☻" }, + { "blacktriangledown", "▾" }, + { "blacktriangleleft", "◂" }, + { "blacktriangleright", "▸" }, + { "blacktriangle", "▴" }, + { "bot", "⊥" }, + { "^bot", "ᗮ" }, + { "bowtie", "⋈" }, + { "boxminus", "⊟" }, + { "boxmid", "◫" }, + { "hcomp", "◫" }, + { "boxplus", "⊞" }, + { "boxtimes", "⊠" }, + { "join", "⊔" }, + { "r-2", "⇉" }, + { "r-3", "⇶" }, + { "r-l-", "⇄" }, + { "r--", "⟶" }, + { "r-n", "↛" }, + { "r-|", "↦" }, + { "r->", "↣" }, + { "r-o", "⊸" }, + { "r-", "→" }, + { "r==", "⇛" }, + { "r=n", "⇏" }, + { "r=", "⇒" }, + { "r~", "↝" }, + { "rr-", "↠" }, + { "reb", "▬" }, + { "rew", "▭" }, + { "real", "ℝ" }, + { "registered", "®" }, + { "re", "▬" }, + { "rbag", "⟆" }, + { "rat", "ℚ" }, + { "radioactive", "☢" }, + { "rrbracket", "〛" }, + { "rangle", "⟩" }, + { "rq", "’" }, + { "rightarrowtail", "↣" }, + { "rightarrow", "→" }, + { "rightharpoondown", "⇁" }, + { "rightharpoonup", "⇀" }, + { "rightleftarrows", "⇄" }, + { "rightleftharpoons", "⇌" }, + { "rightrightarrows", "⇉" }, + { "rightthreetimes", "⋌" }, + { "risingdotseq", "≓" }, + { "ruble", "₽" }, + { "rupee", "₨" }, + { "rho", "ρ" }, + { "rhd", "▷" }, + { "rceil", "⌉" }, + { "rfloor", "⌋" }, + { "rtimes", "⋊" }, + { "rdq", "”" }, + { "rdata", "》" }, + { "functor", "⥤" }, + { "fun", "λ" }, + { "f<<", "«" }, + { "f>>", "»" }, + { "f<", "‹" }, + { "f>", "›" }, + { "h<", "❰" }, + { "h>", "❱" }, + { "finprod", "∏ᶠ" }, + { "finsum", "∑ᶠ" }, + { "frac12", "½" }, + { "frac13", "⅓" }, + { "frac14", "¼" }, + { "frac15", "⅕" }, + { "frac16", "⅙" }, + { "frac18", "⅛" }, + { "frac1", "⅟" }, + { "frac23", "⅔" }, + { "frac25", "⅖" }, + { "frac34", "¾" }, + { "frac35", "⅗" }, + { "frac38", "⅜" }, + { "frac45", "⅘" }, + { "frac56", "⅚" }, + { "frac58", "⅝" }, + { "frac78", "⅞" }, + { "frac", "¼" }, + { "frown", "⌢" }, + { "frqq", "»" }, + { "frq", "›" }, + { "female", "♀" }, + { "fei", "ϥ" }, + { "facsimile", "℻" }, + { "fallingdotseq", "≒" }, + { "flat", "♭" }, + { "flqq", "«" }, + { "flq", "‹" }, + { "forall", "∀" }, + { ")b", "⟆" }, + { "[[", "⟦" }, + { "]]", "⟧" }, + { "{{", "⦃" }, + { "}}", "⦄" }, + { "((", "⸨" }, + { "))", "⸩" }, + { "([", "⟮" }, + { "])", "⟯" }, + { "Xi", "Ξ" }, + { "Nat", "ℕ" }, + { "Nu", "Ν" }, + { "Zeta", "Ζ" }, + { "Rat", "ℚ" }, + { "Real", "ℝ" }, + { "Re", "ℜ" }, + { "Rho", "Ρ" }, + { "Rightarrow", "⇒" }, + { "Rrightarrow", "⇛" }, + { "Rsh", "↱" }, + { "Fei", "Ϥ" }, + { "Frowny", "☹" }, + { "Hori", "Ϩ" }, + { "Heta", "Ͱ" }, + { "Khei", "Ϧ" }, + { "Koppa", "Ϟ" }, + { "Kappa", "Κ" }, + { "^a", "ᵃ" }, + { "^b", "ᵇ" }, + { "^c", "ᶜ" }, + { "^d", "ᵈ" }, + { "^e", "ᵉ" }, + { "^f", "ᶠ" }, + { "^g", "ᵍ" }, + { "^h", "ʰ" }, + { "^i", "ⁱ" }, + { "^j", "ʲ" }, + { "^k", "ᵏ" }, + { "^l", "ˡ" }, + { "^m", "ᵐ" }, + { "^n", "ⁿ" }, + { "^o", "ᵒ" }, + { "^p", "ᵖ" }, + { "^r", "ʳ" }, + { "^s", "ˢ" }, + { "^t", "ᵗ" }, + { "^u", "ᵘ" }, + { "^v", "ᵛ" }, + { "^w", "ʷ" }, + { "^x", "ˣ" }, + { "^y", "ʸ" }, + { "^z", "ᶻ" }, + { "^A", "ᴬ" }, + { "^B", "ᴮ" }, + { "^D", "ᴰ" }, + { "^E", "ᴱ" }, + { "^G", "ᴳ" }, + { "^H", "ᴴ" }, + { "^I", "ᴵ" }, + { "^J", "ᴶ" }, + { "^K", "ᴷ" }, + { "^L", "ᴸ" }, + { "^M", "ᴹ" }, + { "^N", "ᴺ" }, + { "^O", "ᴼ" }, + { "^P", "ᴾ" }, + { "^R", "ᴿ" }, + { "^T", "ᵀ" }, + { "^U", "ᵁ" }, + { "^V", "ⱽ" }, + { "^W", "ᵂ" }, + { "^0", "⁰" }, + { "^1", "¹" }, + { "^2", "²" }, + { "^3", "³" }, + { "^4", "⁴" }, + { "^5", "⁵" }, + { "^6", "⁶" }, + { "^7", "⁷" }, + { "^8", "⁸" }, + { "^9", "⁹" }, + { "^)", "⁾" }, + { "^(", "⁽" }, + { "^=", "⁼" }, + { "^+", "⁺" }, + { "^o_", "º" }, + { "^-", "⁻" }, + { "^a_", "ª" }, + { "^uhook", "ꭟ" }, + { "^ubar", "ᶶ" }, + { "^upsilon", "ᶷ" }, + { "^ltilde", "ꭞ" }, + { "^ls", "ꭝ" }, + { "^lhook", "ᶪ" }, + { "^lretroflexhook", "ᶩ" }, + { "^oe", "ꟹ" }, + { "^heng", "ꭜ" }, + { "^hhook", "ʱ" }, + { "^hwithhook", "ʱ" }, + { "^Hstroke", "ꟸ" }, + { "^theta", "ᶿ" }, + { "^turnedv", "ᶺ" }, + { "^turnedmleg", "ᶭ" }, + { "^turnedm", "ᵚ" }, + { "^turnedh", "ᶣ" }, + { "^turnedalpha", "ᶛ" }, + { "^turnedae", "ᵆ" }, + { "^turneda", "ᵄ" }, + { "^turnedi", "ᵎ" }, + { "^turnede", "ᵌ" }, + { "^turnedrhook", "ʵ" }, + { "^turnedrwithhook", "ʵ" }, + { "^turnedr", "ʴ" }, + { "^twithpalatalhook", "ᶵ" }, + { "^otop", "ᵔ" }, + { "^ezh", "ᶾ" }, + { "^esh", "ᶴ" }, + { "^eth", "ᶞ" }, + { "^eng", "ᵑ" }, + { "^zcurl", "ᶽ" }, + { "^zretroflexhook", "ᶼ" }, + { "^vhook", "ᶹ" }, + { "^Ismall", "ᶦ" }, + { "^Lsmall", "ᶫ" }, + { "^Nsmall", "ᶰ" }, + { "^Usmall", "ᶸ" }, + { "^Istroke", "ᶧ" }, + { "^Rinverted", "ʶ" }, + { "^ccurl", "ᶝ" }, + { "^chi", "ᵡ" }, + { "^shook", "ᶳ" }, + { "^gscript", "ᶢ" }, + { "^schwa", "ᵊ" }, + { "^usideways", "ᵙ" }, + { "^phi", "ᶲ" }, + { "^obarred", "ᶱ" }, + { "^beta", "ᵝ" }, + { "^obottom", "ᵕ" }, + { "^nretroflexhook", "ᶯ" }, + { "^nlefthook", "ᶮ" }, + { "^mhook", "ᶬ" }, + { "^jtail", "ᶨ" }, + { "^iota", "ᶥ" }, + { "^istroke", "ᶤ" }, + { "^ereversedopen", "ᶟ" }, + { "^stop", "ˤ" }, + { "^varphi", "ᵠ" }, + { "^vargamma", "ᵞ" }, + { "^gamma", "ˠ" }, + { "^ain", "ᵜ" }, + { "^alpha", "ᵅ" }, + { "^oopen", "ᵓ" }, + { "^eopen", "ᵋ" }, + { "^Ou", "ᴽ" }, + { "^Nreversed", "ᴻ" }, + { "^Ereversed", "ᴲ" }, + { "^Bbarred", "ᴯ" }, + { "^Ae", "ᴭ" }, + { "^SM", "℠" }, + { "^TEL", "℡" }, + { "^TM", "™" }, + { "_a", "ₐ" }, + { "_e", "ₑ" }, + { "_h", "ₕ" }, + { "_i", "ᵢ" }, + { "_j", "ⱼ" }, + { "_k", "ₖ" }, + { "_l", "ₗ" }, + { "_m", "ₘ" }, + { "_n", "ₙ" }, + { "_o", "ₒ" }, + { "_p", "ₚ" }, + { "_r", "ᵣ" }, + { "_s", "ₛ" }, + { "_t", "ₜ" }, + { "_u", "ᵤ" }, + { "_v", "ᵥ" }, + { "_x", "ₓ" }, + { "_0", "₀" }, + { "_1", "₁" }, + { "_2", "₂" }, + { "_3", "₃" }, + { "_4", "₄" }, + { "_5", "₅" }, + { "_6", "₆" }, + { "_7", "₇" }, + { "_8", "₈" }, + { "_9", "₉" }, + { "_)", "₎" }, + { "_(", "₍" }, + { "_=", "₌" }, + { "_+", "₊" }, + { "_-", "₋" }, + { "!!", "‼" }, + { "!?", "⁉" }, + { "San", "Ϻ" }, + { "Sampi", "Ϡ" }, + { "Sho", "Ϸ" }, + { "Shima", "Ϭ" }, + { "Shei", "Ϣ" }, + { "Stigma", "Ϛ" }, + { "Sigma", "Σ" }, + { "Subset", "⋐" }, + { "Supset", "⋑" }, + { "Smiley", "☺" }, + { "Psi", "Ψ" }, + { "Phi", "Φ" }, + { "Pi", "Π" }, + { "Pi0", "Π₀" }, + { "P0", "Π₀" }, + { "Pi_0", "Π₀" }, + { "P_0", "Π₀" }, + { "bfA", "𝐀" }, + { "bfB", "𝐁" }, + { "bfC", "𝐂" }, + { "bfD", "𝐃" }, + { "bfE", "𝐄" }, + { "bfF", "𝐅" }, + { "bfG", "𝐆" }, + { "bfH", "𝐇" }, + { "bfI", "𝐈" }, + { "bfJ", "𝐉" }, + { "bfK", "𝐊" }, + { "bfL", "𝐋" }, + { "bfM", "𝐌" }, + { "bfN", "𝐍" }, + { "bfO", "𝐎" }, + { "bfP", "𝐏" }, + { "bfQ", "𝐐" }, + { "bfR", "𝐑" }, + { "bfS", "𝐒" }, + { "bfT", "𝐓" }, + { "bfU", "𝐔" }, + { "bfV", "𝐕" }, + { "bfW", "𝐖" }, + { "bfX", "𝐗" }, + { "bfY", "𝐘" }, + { "bfZ", "𝐙" }, + { "bfa", "𝐚" }, + { "bfb", "𝐛" }, + { "bfc", "𝐜" }, + { "bfd", "𝐝" }, + { "bfe", "𝐞" }, + { "bff", "𝐟" }, + { "bfg", "𝐠" }, + { "bfh", "𝐡" }, + { "bfi", "𝐢" }, + { "bfj", "𝐣" }, + { "bfk", "𝐤" }, + { "bfl", "𝐥" }, + { "bfm", "𝐦" }, + { "bfn", "𝐧" }, + { "bfo", "𝐨" }, + { "bfp", "𝐩" }, + { "bfq", "𝐪" }, + { "bfr", "𝐫" }, + { "bfs", "𝐬" }, + { "bft", "𝐭" }, + { "bfu", "𝐮" }, + { "bfv", "𝐯" }, + { "bfw", "𝐰" }, + { "bfx", "𝐱" }, + { "bfy", "𝐲" }, + { "bfz", "𝐳" }, + { "MiA", "𝐴" }, + { "MiB", "𝐵" }, + { "MiC", "𝐶" }, + { "MiD", "𝐷" }, + { "MiE", "𝐸" }, + { "MiF", "𝐹" }, + { "MiG", "𝐺" }, + { "MiH", "𝐻" }, + { "MiI", "𝐼" }, + { "MiJ", "𝐽" }, + { "MiK", "𝐾" }, + { "MiL", "𝐿" }, + { "MiM", "𝑀" }, + { "MiN", "𝑁" }, + { "MiO", "𝑂" }, + { "MiP", "𝑃" }, + { "MiQ", "𝑄" }, + { "MiR", "𝑅" }, + { "MiS", "𝑆" }, + { "MiT", "𝑇" }, + { "MiU", "𝑈" }, + { "MiV", "𝑉" }, + { "MiW", "𝑊" }, + { "MiX", "𝑋" }, + { "MiY", "𝑌" }, + { "MiZ", "𝑍" }, + { "Mia", "𝑎" }, + { "Mib", "𝑏" }, + { "Mic", "𝑐" }, + { "Mid", "𝑑" }, + { "Mie", "𝑒" }, + { "Mif", "𝑓" }, + { "Mig", "𝑔" }, + { "Mii", "𝑖" }, + { "Mij", "𝑗" }, + { "Mik", "𝑘" }, + { "Mil", "𝑙" }, + { "Mim", "𝑚" }, + { "Min", "𝑛" }, + { "Mio", "𝑜" }, + { "Mip", "𝑝" }, + { "Miq", "𝑞" }, + { "Mir", "𝑟" }, + { "Mis", "𝑠" }, + { "Mit", "𝑡" }, + { "Miu", "𝑢" }, + { "Miv", "𝑣" }, + { "Miw", "𝑤" }, + { "Mix", "𝑥" }, + { "Miy", "𝑦" }, + { "Miz", "𝑧" }, + { "MIA", "𝑨" }, + { "MIB", "𝑩" }, + { "MIC", "𝑪" }, + { "MID", "𝑫" }, + { "MIE", "𝑬" }, + { "MIF", "𝑭" }, + { "MIG", "𝑮" }, + { "MIH", "𝑯" }, + { "MII", "𝑰" }, + { "MIJ", "𝑱" }, + { "MIK", "𝑲" }, + { "MIL", "𝑳" }, + { "MIM", "𝑴" }, + { "MIN", "𝑵" }, + { "MIO", "𝑶" }, + { "MIP", "𝑷" }, + { "MIQ", "𝑸" }, + { "MIR", "𝑹" }, + { "MIS", "𝑺" }, + { "MIT", "𝑻" }, + { "MIU", "𝑼" }, + { "MIV", "𝑽" }, + { "MIW", "𝑾" }, + { "MIX", "𝑿" }, + { "MIY", "𝒀" }, + { "MIZ", "𝒁" }, + { "MIa", "𝒂" }, + { "MIb", "𝒃" }, + { "MIc", "𝒄" }, + { "MId", "𝒅" }, + { "MIe", "𝒆" }, + { "MIf", "𝒇" }, + { "MIg", "𝒈" }, + { "MIh", "𝒉" }, + { "MIi", "𝒊" }, + { "MIj", "𝒋" }, + { "MIk", "𝒌" }, + { "MIl", "𝒍" }, + { "MIm", "𝒎" }, + { "MIn", "𝒏" }, + { "MIo", "𝒐" }, + { "MIp", "𝒑" }, + { "MIq", "𝒒" }, + { "MIr", "𝒓" }, + { "MIs", "𝒔" }, + { "MIt", "𝒕" }, + { "MIu", "𝒖" }, + { "MIv", "𝒗" }, + { "MIw", "𝒘" }, + { "MIx", "𝒙" }, + { "MIy", "𝒚" }, + { "MIz", "𝒛" }, + { "McA", "𝒜" }, + { "McB", "ℬ" }, + { "McC", "𝒞" }, + { "McD", "𝒟" }, + { "McE", "ℰ" }, + { "McF", "ℱ" }, + { "McG", "𝒢" }, + { "McH", "ℋ" }, + { "McI", "ℐ" }, + { "McJ", "𝒥" }, + { "McK", "𝒦" }, + { "McL", "ℒ" }, + { "McM", "ℳ" }, + { "McN", "𝒩" }, + { "McO", "𝒪" }, + { "McP", "𝒫" }, + { "McQ", "𝒬" }, + { "McR", "ℛ" }, + { "McS", "𝒮" }, + { "McT", "𝒯" }, + { "McU", "𝒰" }, + { "McV", "𝒱" }, + { "McW", "𝒲" }, + { "McX", "𝒳" }, + { "McY", "𝒴" }, + { "McZ", "𝒵" }, + { "Mca", "𝒶" }, + { "Mcb", "𝒷" }, + { "Mcc", "𝒸" }, + { "Mcd", "𝒹" }, + { "Mce", "ℯ" }, + { "Mcf", "𝒻" }, + { "Mcg", "ℊ" }, + { "Mch", "𝒽" }, + { "Mci", "𝒾" }, + { "Mcj", "𝒿" }, + { "Mck", "𝓀" }, + { "Mcl", "𝓁" }, + { "Mcm", "𝓂" }, + { "Mcn", "𝓃" }, + { "Mco", "ℴ" }, + { "Mcp", "𝓅" }, + { "Mcq", "𝓆" }, + { "Mcr", "𝓇" }, + { "Mcs", "𝓈" }, + { "Mct", "𝓉" }, + { "Mcu", "𝓊" }, + { "Mcv", "𝓋" }, + { "Mcw", "𝓌" }, + { "Mcx", "𝓍" }, + { "Mcy", "𝓎" }, + { "Mcz", "𝓏" }, + { "MCA", "𝓐" }, + { "MCB", "𝓑" }, + { "MCC", "𝓒" }, + { "MCD", "𝓓" }, + { "MCE", "𝓔" }, + { "MCF", "𝓕" }, + { "MCG", "𝓖" }, + { "MCH", "𝓗" }, + { "MCI", "𝓘" }, + { "MCJ", "𝓙" }, + { "MCK", "𝓚" }, + { "MCL", "𝓛" }, + { "MCM", "𝓜" }, + { "MCN", "𝓝" }, + { "MCO", "𝓞" }, + { "MCP", "𝓟" }, + { "MCQ", "𝓠" }, + { "MCR", "𝓡" }, + { "MCS", "𝓢" }, + { "MCT", "𝓣" }, + { "MCU", "𝓤" }, + { "MCV", "𝓥" }, + { "MCW", "𝓦" }, + { "MCX", "𝓧" }, + { "MCY", "𝓨" }, + { "MCZ", "𝓩" }, + { "MCa", "𝓪" }, + { "MCb", "𝓫" }, + { "MCc", "𝓬" }, + { "MCd", "𝓭" }, + { "MCe", "𝓮" }, + { "MCf", "𝓯" }, + { "MCg", "𝓰" }, + { "MCh", "𝓱" }, + { "MCi", "𝓲" }, + { "MCj", "𝓳" }, + { "MCk", "𝓴" }, + { "MCl", "𝓵" }, + { "MCm", "𝓶" }, + { "MCn", "𝓷" }, + { "MCo", "𝓸" }, + { "MCp", "𝓹" }, + { "MCq", "𝓺" }, + { "MCr", "𝓻" }, + { "MCs", "𝓼" }, + { "MCt", "𝓽" }, + { "MCu", "𝓾" }, + { "MCv", "𝓿" }, + { "MCw", "𝔀" }, + { "MCx", "𝔁" }, + { "MCy", "𝔂" }, + { "MCz", "𝔃" }, + { "MfA", "𝔄" }, + { "MfB", "𝔅" }, + { "MfC", "ℭ" }, + { "MfD", "𝔇" }, + { "MfE", "𝔈" }, + { "MfF", "𝔉" }, + { "MfG", "𝔊" }, + { "MfH", "ℌ" }, + { "MfI", "ℑ" }, + { "MfJ", "𝔍" }, + { "MfK", "𝔎" }, + { "MfL", "𝔏" }, + { "MfM", "𝔐" }, + { "MfN", "𝔑" }, + { "MfO", "𝔒" }, + { "MfP", "𝔓" }, + { "MfQ", "𝔔" }, + { "MfR", "ℜ" }, + { "MfS", "𝔖" }, + { "MfT", "𝔗" }, + { "MfU", "𝔘" }, + { "MfV", "𝔙" }, + { "MfW", "𝔚" }, + { "MfX", "𝔛" }, + { "MfY", "𝔜" }, + { "MfZ", "ℨ" }, + { "Mfa", "𝔞" }, + { "Mfb", "𝔟" }, + { "Mfc", "𝔠" }, + { "Mfd", "𝔡" }, + { "Mfe", "𝔢" }, + { "Mff", "𝔣" }, + { "Mfg", "𝔤" }, + { "Mfh", "𝔥" }, + { "Mfi", "𝔦" }, + { "Mfj", "𝔧" }, + { "Mfk", "𝔨" }, + { "Mfl", "𝔩" }, + { "Mfm", "𝔪" }, + { "Mfn", "𝔫" }, + { "Mfo", "𝔬" }, + { "Mfp", "𝔭" }, + { "Mfq", "𝔮" }, + { "Mfr", "𝔯" }, + { "Mfs", "𝔰" }, + { "Mft", "𝔱" }, + { "Mfu", "𝔲" }, + { "Mfv", "𝔳" }, + { "Mfw", "𝔴" }, + { "Mfx", "𝔵" }, + { "Mfy", "𝔶" }, + { "Mfz", "𝔷" }, + { "yen", "¥" }, + { "varrho", "ϱ" }, + { "varkappa", "ϰ" }, + { "varkai", "ϗ" }, + { "varnothing", "∅" }, + { "varpi", "ϖ" }, + { "varphi", "ϕ" }, + { "varprime", "′" }, + { "varpropto", "∝" }, + { "vartheta", "ϑ" }, + { "vartriangleleft", "⊲" }, + { "vartriangleright", "⊳" }, + { "varbeta", "ϐ" }, + { "varsigma", "ς" }, + { "veebar", "⊻" }, + { "vee", "∨" }, + { "ve", "ě" }, + { "vE", "Ě" }, + { "vdash", "⊢" }, + { "vdots", "⋮" }, + { "vd", "ď" }, + { "vDash", "⊨" }, + { "vD", "Ď" }, + { "vc", "č" }, + { "vC", "Č" }, + { "koppa", "ϟ" }, + { "kip", "₭" }, + { "ki", "į" }, + { "kI", "Į" }, + { "kelvin", "K" }, + { "kappa", "κ" }, + { "khei", "ϧ" }, + { "warning", "⚠" }, + { "won", "₩" }, + { "wedge", "∧" }, + { "wp", "℘" }, + { "wr", "≀" }, + { "Dei", "Ϯ" }, + { "Delta", "Δ" }, + { "Digamma", "Ϝ" }, + { "Diamond", "◇" }, + { "Downarrow", "⇓" }, + { "DH", "Ð" }, + { "zeta", "ζ" }, + { "Eta", "Η" }, + { "Epsilon", "Ε" }, + { "Beta", "Β" }, + { "Box", "□" }, + { "Bumpeq", "≎" }, + { "bbA", "𝔸" }, + { "bbB", "𝔹" }, + { "bbC", "ℂ" }, + { "bbD", "𝔻" }, + { "bbE", "𝔼" }, + { "bbF", "𝔽" }, + { "bbG", "𝔾" }, + { "bbH", "ℍ" }, + { "bbI", "𝕀" }, + { "bbJ", "𝕁" }, + { "bbK", "𝕂" }, + { "bbL", "𝕃" }, + { "bbM", "𝕄" }, + { "bbN", "ℕ" }, + { "bbO", "𝕆" }, + { "bbP", "ℙ" }, + { "bbQ", "ℚ" }, + { "bbR", "ℝ" }, + { "bbS", "𝕊" }, + { "bbT", "𝕋" }, + { "bbU", "𝕌" }, + { "bbV", "𝕍" }, + { "bbW", "𝕎" }, + { "bbX", "𝕏" }, + { "bbY", "𝕐" }, + { "bbZ", "ℤ" }, + { "bba", "𝕒" }, + { "bbb", "𝕓" }, + { "bbc", "𝕔" }, + { "bbd", "𝕕" }, + { "bbe", "𝕖" }, + { "bbf", "𝕗" }, + { "bbg", "𝕘" }, + { "bbh", "𝕙" }, + { "bbi", "𝕚" }, + { "bbj", "𝕛" }, + { "bbk", "𝕜" }, + { "bbl", "𝕝" }, + { "bbm", "𝕞" }, + { "bbn", "𝕟" }, + { "bbo", "𝕠" }, + { "bbp", "𝕡" }, + { "bbq", "𝕢" }, + { "bbr", "𝕣" }, + { "bbs", "𝕤" }, + { "bbt", "𝕥" }, + { "bbu", "𝕦" }, + { "bbv", "𝕧" }, + { "bbw", "𝕨" }, + { "bbx", "𝕩" }, + { "bby", "𝕪" }, + { "bbz", "𝕫" }, + { "Rge0", "ℝ≥0" }, + { "R>=0", "ℝ≥0" }, + { "nnreal", "ℝ≥0" }, + { "ennreal", "ℝ≥0∞" }, + { "enat", "ℕ∞" }, + { "Zsqrt", "ℤ√" }, + { "zsqrtd", "ℤ√" }, + { "liel", "⁅" }, + { "bracketl", "⁅" }, + { "lier", "⁆" }, + { "[-", "⁅" }, + { "-]", "⁆" }, + { "lsimplex", "⦋" }, + { "rsimplex", "⦌" }, + { "bracketr", "⁆" }, + { "nhds", "𝓝" }, + { "nbhds", "𝓝" }, + { "X", "⨯" }, + { "vectorproduct", "⨯" }, + { "crossproduct", "⨯" }, + { "xs", "×ˢ" }, + { "coprod", "⨿" }, + { "sigmaobj", "∐" }, + { "xf", "×ᶠ" }, + { "exf", "∃ᶠ" }, + { "Yot", "Ϳ" }, + { "goal", "⊢" }, + { "Vdash", "⊩" }, + { "Vert", "‖" }, + { "Vvdash", "⊪" }, + { "tiny", "⧾" }, + { "miny", "⧿" }, + { "heq", "≍" }, + { "r!", "¡" }, +} diff --git a/builtin/runtime/lean_input.lua b/builtin/runtime/lean_input.lua new file mode 100644 index 0000000..4079de0 --- /dev/null +++ b/builtin/runtime/lean_input.lua @@ -0,0 +1,517 @@ +-- lean_input.lua --- the Lean 4 Unicode input method (Arc 8 Stage 4b). +-- +-- Typing `\alpha` gives `α`; `\<>` gives `⟨⟩` with the point between. +-- The table is vendored in lean_abbrev.lua, generated from +-- vscode-lean4 — see that file's header and Q#LN11. +-- +-- This is a typed-edit consumer (Stage 4a, Q#LN10) registered AHEAD of +-- auto-pairing at priority 50. The ordering is load-bearing, not +-- cosmetic: 64 abbreviation keys contain a character in the `lean4` +-- pair set (`\[[]]` → `⟦⟧`, `\{{}}` → `⦃⦄`), so with pairing first, +-- typing `\[` would insert `[]` with the point between and corrupt the +-- pending key to `\[]` before the second `[` arrives — `\[[]]` becomes +-- unreachable. Priority, not load order, is what decides this; that is +-- the whole reason Stage 4a exists. +-- +-- The consumer therefore claims every keystroke that EXTENDS an open +-- pending abbreviation, not merely one that completes an expansion. A +-- consumer that claimed only completed expansions would hand each +-- intermediate `[` to pairing, which is the same corruption by a +-- different route. "Claimed" means the chain stops, not that an edit +-- was made (Q#LN22). +-- +-- UNDO IS CROSS-PEER-DEGRADED, and this is accepted rather than papered +-- over (Q#LN21). `classify_key` (src/optimistic.rs) returns `Insert(c)` +-- for `\` and for every ASCII letter — only the nine built-in pair +-- chars are excluded — so on a CRDT frontend `\alpha` arrives as six +-- SOURCE-peer optimistic inserts while the expansion is a single +-- DAEMON-peer replace spanning all six. Undo across that boundary is +-- not chronologically arbitrated. This is the same defect Q#LN6 already +-- accepts for `⟨⟩`, one order of magnitude wider: it is every +-- abbreviation the user types, not a few brackets. The general fix is +-- chronological cross-peer undo arbitration, named substrate work. +-- `set_round_trip_input` would fix it and is rejected — it also makes +-- `dispatch_idle` report false, so RET would stop inserting a newline. +-- +-- Framing: docs/lean4-mode-framing.md Q#LN11, Q#LN21, Q#LN22. + +pmacs.lean_input = pmacs.lean_input or {} + +local ed = pmacs.editor + +local LEADER = "\\" +local CURSOR = "$CURSOR" + +pmacs.config.define { + name = "lean.abbrev", + description = "Expand \\-prefixed abbreviations into Unicode symbols in Lean 4 buffers.", + type = "boolean", + default = true, + mutability = "live", +} + +-- --------------------------------------------------------------------- +-- The table, and the two indexes derived from it at load time +-- --------------------------------------------------------------------- + +-- `best[p]` is the symbol for the shortest key having `p` as a prefix, +-- ties broken by the key's position in the vendored sequence. Both +-- halves matter: 101 prefixes have equal-shortest candidates that +-- resolve to DIFFERENT symbols (`f` → `‹` from `f<`, not `›` from +-- `f>`), and the sequence's order is the only place that tie is +-- recorded. `pairs` over a map-shaped table could not express it. +-- +-- `eager[k]` marks the 1,550 keys that are complete and have no longer +-- key extending them — the ones that expand the moment they are typed, +-- with no terminator. `to` is NOT one of them (`top`, `to0`, `toa`), +-- which is exactly the case that reads as eager until the table is +-- consulted. +local best, eager = {}, {} + +do + local seq = pmacs.lean_abbrev + if type(seq) ~= "table" then seq = {} end + local extended = {} + for i = 1, #seq do + local entry = seq[i] + local key, symbol = entry[1], entry[2] + -- Walk every prefix of the key, including the key itself. Iterating + -- the sequence in order and only overwriting on a STRICTLY shorter + -- key is what makes the source-order tiebreak fall out: an equal + -- length arriving later loses to the one already recorded. + for n = 1, #key do + local p = key:sub(1, n) + local cur = best[p] + if cur == nil or #key < cur.len then + best[p] = { symbol = symbol, len = #key } + end + if n < #key then extended[p] = true end + end + end + for i = 1, #seq do + local key = seq[i][1] + if not extended[key] then eager[key] = true end + end +end + +-- Test seam (leading underscore = not stable API). Acceptance 45g reads +-- these to pin self-consistency properties a corrupt emit would break — +-- it cannot diff against `abbreviations.json`, which is not shipped. +function pmacs.lean_input._resolve(text) + local hit = best[text] + return hit and hit.symbol or nil +end + +function pmacs.lean_input._is_eager(key) + return eager[key] == true +end + +-- --------------------------------------------------------------------- +-- Pending state: one record per FRONTEND (Q#LN22) +-- --------------------------------------------------------------------- + +-- Keyed by frontend id, with the buffer stored inside and compared by +-- value. Q#LN22 specifies the key as `(frontend, buffer)`; a per- +-- frontend slot is equivalent here and avoids inventing a scalar +-- buffer key (`BufferId`'s inner value is deliberately private, R22). +-- The generality a two-level map would add is unreachable: a frontend +-- has one point, and `buffer.after-switch` clears that frontend's slot, +-- so no frontend can hold pending state in a buffer it is not in. +-- +-- Per-frontend rather than per-buffer is NOT a refinement — a buffer- +-- keyed table lets either frontend consume or discard the other's +-- half-typed abbreviation in a shared buffer, which is the ordinary +-- TUI-plus-GPU configuration this project ships. +local pending = {} + +-- Expansions the chain consumer decided on but did NOT perform, keyed +-- the same way. See `run_deferred` below for why they wait. +local deferred = {} + +local function frontend_id() + local ok, id = pcall(function() return pmacs.frontend.id() end) + if ok then return id end + return nil +end + +-- Is `rec` a typed edit that continues `p` exactly? Conservative by +-- construction (Q#LN22): abandonment is LAZY because pmacs has no +-- cursor-motion hook, so every guard that would have been checked at +-- the moment the user left is checked here instead, at the next typed +-- edit. +local function still_valid(p, rec, buf) + if p.buffer ~= rec.buffer or p.window ~= rec.window then return false end + -- The point must still be at the end of the pending span: the leader, + -- plus what has been typed into it, plus the character that just + -- landed. + if rec.effective_start ~= p.start_offset + 1 + #p.text then return false end + -- Exactly one edit since this frontend last extended the pending + -- abbreviation — the one being processed now. Deliberately strict + -- across frontends: `revision()` is BUFFER-GLOBAL, so a peer editing + -- the shared buffer invalidates this record even though it edited + -- elsewhere. Keeping it alive would mean translating and validating + -- the span through arbitrary peer edits, substrate Stage 4b does not + -- add. + local ok, rev = pcall(function() return buf:revision() end) + if not ok or rev ~= p.expected_revision + 1 then return false end + return true +end + +-- --------------------------------------------------------------------- +-- Expansion +-- --------------------------------------------------------------------- + +-- Right-gravity translation of `pos` through the effective edit — +-- pair.lua's shape, for the same reason: the point sits AFTER the +-- replaced span (on the terminator, or on a closer pairing inserted) +-- and has to move with it. +local function translate(pos, estart, estop, einserted) + if pos < estart then return pos end + if pos > estop then return pos - (estop - estart) + einserted end + return estart + einserted +end + +-- Replace the pending span (leader + typed text) with `symbol`. +-- +-- The span deliberately STOPS BEFORE the terminator. Including the +-- terminator would make the expansion and the terminator one edit, but +-- it would also swallow whatever auto-pairing did with that terminator +-- — and a pair character is a legal terminator (`\alp(`). One undo +-- restores the same text either way, because the terminator was its own +-- insert to begin with. +-- +-- ONE `buf:replace`: one undo step, one CRDT op, one effective-edit +-- verification. A rejection drops the pending state and does not retry, +-- the same discipline as comment.lua's Q#CT5 and pair.lua. +local function expand(buf, start, span_end, symbol) + local cursor_at = symbol:find(CURSOR, 1, true) + local text = cursor_at and (symbol:gsub("%$CURSOR", "", 1)) or symbol + + -- The context to compare against AFTER the edit. A buffer intercept + -- may switch window or buffer while the replace runs; the point in + -- whatever it switched to is not ours to move. + local win0 = pmacs.window.current() + local point0 = ed.cursor() + + local ok, estart, estop, einserted = pcall(function() + return buf:replace(start, span_end, text) + end) + if not ok then + ed.set_status("lean abbreviation rejected by buffer intercept") + return nil + end + if estart ~= start or estop ~= span_end or einserted ~= #text then + ed.set_status("lean abbreviation altered by buffer intercept") + return nil + end + + -- The point MUST be placed explicitly. Unlike pairing's at-cursor + -- insert, this replace SHRINKS the buffer — `\alpha` (6 bytes) + -- becomes `α` (2) — and a point left at the pre-edit offset is past + -- the new end. Every later self-insert is then silently rejected and + -- the editor looks dead. There is no daemon re-grounding that covers + -- this; that only holds for an edit that lands at the cursor. + -- + -- Context-guarded exactly as pair.lua's `repair_cursor` is: if the + -- intercept switched us elsewhere, `goto_byte` would move the point + -- of a buffer that has nothing to do with this expansion. + if pmacs.window.current() == win0 and pmacs.window.buffer() == buf then + if cursor_at then + ed.goto_byte(start + cursor_at - 1) + else + ed.goto_byte(translate(point0, estart, estop, einserted)) + end + end + return start + #text +end + +-- --------------------------------------------------------------------- +-- The consumer +-- --------------------------------------------------------------------- + +-- Chain invocations not yet matched by a `run_deferred`. +-- +-- `buffer.after-edit` fan-outs NEST: the typed-edit contract explicitly +-- supports a consumer calling `pmacs.hook.run("buffer.after-edit")`, +-- and a nested run re-enters every subscriber — including this module's +-- deferred-expansion subscriber, while the OUTER chain is still walking +-- its consumer list and pairing has not yet seen the terminator. A +-- nested run that performed the expansion would reproduce exactly the +-- bug deferring exists to fix: pairing resumes afterwards holding a +-- record the replace has invalidated, declines, and the closer is lost. +-- +-- Counting has to happen INSIDE the chain and BEFORE any consumer that +-- might start a nested fan-out. A subscriber registered alongside +-- `run_deferred` is too late — the whole nested fan-out completes +-- inside the outer chain's subscriber, before either of them runs. And +-- counting in the expander itself is not enough: a lower-priority +-- consumer may CLAIM and stop the chain before the expander is +-- reached, so a nested pass would go uncounted while its +-- `run_deferred` still ran (round 11's fix, round 12's defect). +-- +-- Hence a separate no-op consumer at the minimum priority, which runs +-- first in every chain invocation that reaches any consumer at all. +-- Its guarantee is exactly the ordering contract the chain already +-- rests on, and it degrades safely: the only thing that can skip it is +-- a claim ahead of it, which skips the expander too, so nothing is +-- queued in that fan-out either. +local depth = 0 + +local function count_fan_out() + depth = depth + 1 + return false +end + +local function on_typed_edit(rec) + local fid = frontend_id() + if fid == nil then return false end + + -- A fan-out carrying no record is still information: a paste, + -- programmatic edit or replicated op landed, so whatever this + -- frontend had pending no longer describes the buffer. Drop it and + -- decline — this is why the chain calls consumers with nil rather + -- than skipping them (Q#LN10). + if not rec then + pending[fid] = nil + return false + end + if not (ed.this_command and ed.this_command() == "buffer.self-insert") then + pending[fid] = nil + return false + end + + -- Both gates resolve against the SOURCE buffer of the typed edit, not + -- the active one — a context-switching command may have replaced it + -- by callback time (pair.lua round 2, finding 2). + if not pmacs.config.get("lean.abbrev", rec.buffer) then + pending[fid] = nil + return false + end + local lang + if pmacs.lsp and pmacs.lsp.buffer_language then + local ok, l = pcall(pmacs.lsp.buffer_language, rec.buffer) + if ok then lang = l end + end + if lang ~= "lean4" then + -- No pending abbreviation is ever OPENED outside a `lean4` buffer: + -- `\` in Rust is an ordinary character and `\[` there still pairs. + pending[fid] = nil + return false + end + + local buf = pmacs.window.buffer() + if not buf or buf ~= rec.buffer or pmacs.window.current() ~= rec.window then + pending[fid] = nil + return false + end + -- Fail closed on a transformed source self-insert, as pairing does: + -- expanding on top of a relocated or rewritten character compounds + -- the intercept's result. + if not rec.clean then + pending[fid] = nil + return false + end + -- ...and on a source edit whose context is no longer current. The + -- buffer and window matching is not enough: a redefined self-insert + -- can insert the character and THEN move the point, and expanding + -- over a span the user has left teleports them back into it. Pairing + -- makes the same three-part check for the same reason. + if ed.cursor() ~= rec.post_cursor then + pending[fid] = nil + return false + end + + local revision + do + local ok, rev = pcall(function() return buf:revision() end) + if not ok then + pending[fid] = nil + return false + end + revision = rev + end + + local p = pending[fid] + if p and not still_valid(p, rec, buf) then + p = nil + pending[fid] = nil + end + + local ch = rec.char + + -- No pending abbreviation: only the leader opens one. + if not p then + if ch == LEADER then + pending[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = rec.effective_start, + text = "", + expected_revision = revision, + } + -- Claimed: the leader belongs to the abbreviation, and pairing + -- has no interest in it either way. + return true + end + return false + end + + -- Pending: does any key still have `text .. ch` as a prefix? + local extended = p.text .. ch + if best[extended] then + p.text = extended + p.expected_revision = revision + if eager[extended] then + pending[fid] = nil + deferred[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = p.start_offset, + text = extended, + symbol = best[extended].symbol, + re_arm = false, + } + end + -- Claimed either way: an extension that has not yet completed must + -- NOT reach auto-pairing (`\[` in `\[[]]`), and a completing one is + -- part of the abbreviation, not a character pairing should react to. + return true + end + + -- `ch` does not extend the abbreviation: it TERMINATES it, and a + -- terminator is an ordinary character that auto-pairing is entitled + -- to react to (`\alp(` must give `α()`). So the expansion is + -- DEFERRED to the subscriber below and this returns false, leaving + -- pairing a record whose offsets still describe the buffer. + -- + -- Expanding here and returning false would not do: the replace makes + -- pairing's copy of the record stale, so pairing declines and the + -- closer is silently lost. Expanding here and returning true is + -- worse — it is what shipped in the first revision of this file, and + -- it makes every pair-character terminator silently unpaired. + pending[fid] = nil + if best[p.text] and #p.text > 0 then + deferred[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = p.start_offset, + text = p.text, + symbol = best[p.text].symbol, + -- A terminating `\` re-arms as a NEW leader at its own position + -- (`\al\to` → `∀→`). Upstream gets this from `processChange`, + -- where a finished abbreviation reports `isAffected = false` and + -- so does not suppress the new-leader branch. This is NOT the + -- `\\` case: there the pending text is empty, `\` EXTENDS, and + -- the result is one literal backslash with nothing left open. + re_arm = ch == LEADER, + } + elseif ch == LEADER then + -- Nothing to expand, but the leader still opens a fresh + -- abbreviation where it landed. + pending[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = rec.effective_start, + text = "", + expected_revision = revision, + } + return true + end + + return false +end + +-- The deferred expansion, on its own `buffer.after-edit` subscriber. +-- +-- It runs AFTER the whole typed-edit chain — this chunk loads after +-- typed_edit.lua, and hook callbacks run in registration order — so +-- auto-pairing has already reacted to the terminator by the time the +-- expansion rewrites the text in front of it. Pairing's closer lands +-- after the terminator, outside the replaced span, so it survives. +-- +-- It must also run BEFORE lsp.lua's subscriber (Q#AP7): that one +-- flushes `didChange` synchronously on the signature-trigger path, and +-- a server told about `\alp ` instead of `α ` stays wrong until the +-- next edit. This chunk loads before lsp.lua for exactly that reason. +-- +-- A claim by ANY chain consumer stops the chain but not this — which +-- is the point. Pairing claims the terminator it reacts to. +local function run_deferred() + -- Match off this fan-out's chain invocation. `> 1` means the outer + -- chain is still mid-list — pairing has not had the terminator yet — + -- so the queued expansion stays queued for the outer pass. The clamp + -- keeps this honest if a claim beat the counting consumer, in which + -- case nothing was queued in that fan-out either. + local level = depth + if depth > 0 then depth = depth - 1 end + if level > 1 then return end + + local fid = frontend_id() + if fid == nil then return end + local d = deferred[fid] + deferred[fid] = nil + if not d then return end + + local buf = pmacs.window.buffer() + if not buf or buf ~= d.buffer or pmacs.window.current() ~= d.window then + return + end + + -- The span must still hold exactly what was typed into it. Pairing + -- only edits at the point, which is past this span, so in practice + -- this holds; a buffer intercept is not obliged to be so polite. + local span_end = d.start_offset + 1 + #d.text + local ok, actual = pcall(function() + return buf:slice(d.start_offset, span_end) + end) + if not ok or actual ~= LEADER .. d.text then return end + + local after = expand(buf, d.start_offset, span_end, d.symbol) + if after and d.re_arm then + local rev_ok, rev = pcall(function() return buf:revision() end) + if rev_ok then + pending[fid] = { + buffer = d.buffer, + window = d.window, + start_offset = after, + text = "", + expected_revision = rev, + } + end + end +end + +-- Q#KR11's seam: a detached frontend's pending state must not outlive +-- it. Ids are monotonic, so this table would otherwise grow for the +-- life of the session. +pmacs.hook.add("frontend.detached", function(fid) + pending[fid] = nil + deferred[fid] = nil +end) + +pmacs.hook.add("buffer.after-edit", run_deferred) + +-- `buffer.after-switch` fires with NO arguments, so it cannot say whose +-- switch it was. The acting frontend is the one that produced the most +-- recent dispatched input event, which is what `pmacs.frontend.id()` +-- reports at callback time. Clearing every entry instead would let one +-- frontend's navigation discard another's half-typed abbreviation. +pmacs.hook.add("buffer.after-switch", function() + local fid = frontend_id() + if fid ~= nil then pending[fid] = nil end +end) + +-- Runs first in every chain invocation that reaches a consumer at all, +-- which is what makes the nesting count trustworthy — see `depth`. It +-- declines, always: it observes, it does not participate. +pmacs.typed_edit.add_consumer { + name = "lean-abbrev-fan-out-counter", + priority = -2147483648, + fn = count_fan_out, +} + +pmacs.typed_edit.add_consumer { + name = "lean-abbrev", + priority = 50, + fn = on_typed_edit, +} diff --git a/docs/active-work.md b/docs/active-work.md index 5a74c24..ff1b894 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -23,7 +23,8 @@ here too until #172 removed it — that is the update those two owe.) machine-local: `origin` may name this canonical URL, a release mirror, or something else, and therefore has no authority by name alone. - Canonical base at this snapshot: - `githubsucks/main` @ `a27f646` (Lean 4 Stage 4a #179 atop bottom-panel + `githubsucks/main` @ `74301d1` (the dired Stage 1 landed-doc refresh + #169 atop Lean 4 Stage 4a #179, bottom-panel Stage 2A #177, the bottom-panel Stage 2 framing #175, terminal configuration Stage 1 #173, Lean 4 Stage 3b #170, Stage 3a #167, the CRDT undo repro #157, the inline-math landed-doc refresh #172, the @@ -161,175 +162,145 @@ If it does not, stop and repair the remote/fetch configuration. to recur; the next occurrence carries its own evidence under whoever's PR, and a Stage B framing follows then. -## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b, 4a MERGED; 4b is next +## Lean 4 lane (Arc 8) — Stages 1–4a MERGED; Stage 4b IN REVIEW -- **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`), - #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full +- **Stages 1, 2, 3a, 3b and 4a are MERGED** — #160 (`main` @ `0827dd1`), + #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`), #179 + (`a27f646`). Their full histories were pruned from this ledger in round 6, per this file's own instruction to remove entries when their PR merges; the durable facts now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where - a fresh machine should read them. `docs/lean4-mode-framing.md` rev 8 + a fresh machine should read them. `docs/lean4-mode-framing.md` rev 9 carries the decisions. -### Stage 4 — framing rev 8, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) +### Stage 4b — the Unicode input method (branch `lean4-stage4b-input-method`) -- Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170** - (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main - that had advanced 50 commits mid-review; the only conflict either time - was this ledger's own lane headings, resolved by keeping both sides. -- **Stage 4a merged as #179** (`main` @ `a27f646`, 2026-07-26) — the - typed-edit consumer chain. Worktree `../pmacs-lean-stage4`, branched - off `main` @ `d400f30`; retained, carrying nothing unmerged. - `docs/lean4-mode-framing.md` **revision 8** remains the approved - framing. **Stage 4b (the Lean-specific half) is framed and not - started.** -- **Round 6 review found five P1s, four of them internal to rev 6** — - facts about pmacs the revision asserted without checking, while its - external (upstream) facts held. Fixed in rev 7: Stage 4a's footprint - omitted the test file its own acceptance requires; pending - abbreviation state was keyed by buffer when pmacs is **multi-frontend** - (`EditorCore.views` is per-`FrontendId`, `take_typed_edit` is already - frontend-keyed, and `buffer.after-switch` fires with NO arguments, so - a buffer-keyed clear lets any frontend discard another's pending - state); the shortest-match rule was missing its **tie-break by source - declaration order**, which 101 prefixes depend on and a `pairs`- - iterated Lua map cannot express; and the generator's "abort on keys - needing escaping" rule **rejects the real table** (`\` is a key, `"` - begins eleven). -- **A 404 on a guessed path is not evidence of absence.** Rev 6 declared - the upstream package ships no README after fetching the package root, - with the directory listing showing `src/README.md` already in hand. - The README states the tie rule in one sentence. -- **Round 7 review found one remaining P1 in acceptance 45i.** Rev 7 - required A's pending abbreviation to survive B editing the same - buffer, while Q#LN22 also required an exact buffer-revision advance. - Those cannot both hold: revisions are buffer-global and every edit - bumps them. Rev 8 keeps the conservative guard and separates - ownership from survival — B cannot consume A's record, but B editing - the shared buffer invalidates A lazily; B switching buffers or - detaching remains frontend-scoped when no shared-buffer edit - intervenes. -- **Round 5 re-scout split Stage 4 into 4a (substrate) and 4b (Lean).** - 4a is the typed-edit consumer chain — `builtin/runtime/typed_edit.lua` - plus `pair.lua` re-expressed as one registered consumer, no behavior - change. 4b is the input method. The split is forced by §4's own rule, - which Stage 4's risk column ("refactors `pair.lua`'s provenance read") - broke while the prose called the stage Lean-only. -- **This is the SECOND consecutive re-scout to find that rule broken** - (round 4 found it for Stage 3). Rev 5 had even noticed the shape and - answered it with a commit boundary. **A commit boundary is not a review - boundary.** Re-check every remaining stage against §4 at scout time; - the rule is not self-enforcing. -- **Rev 5's expansion semantics were wrong in three ways**, found by - reading `leanprover/vscode-lean4` @ `17d1d08` rather than inferring - from behavior. Resolution is *shortest key having the input as a - prefix* (`\al` → `∀` from `all`, not `alpha`); there is **no - terminator list** (`'+ '` is a key, so space extends after `\+`; `'\'` - is a key, so `\\` → `\`); and an unmatchable tail is **appended**, - not dropped (`\alp7` → `α7`). -- **There is no cursor-motion hook**, so rev 5's acceptance 43 ("moving - the cursor out abandons it") was not buildable. Abandonment is lazy — - validated at the next typed edit — and the criterion now asserts what - pmacs can actually detect. Upstream drives this off `changeSelections`; - that seam does not exist here. -- **`dispatch_key` is only half the production path for 4b.** The - auto-pair suite gets away with dispatch-only because Q#AP1 removed the - pair chars from the optimistic classifiers; `\` and the letters are - NOT excluded, so on a CRDT frontend the optimistic producer is the real - path. That producer is `#[cfg(feature = "crdt")]` and CI never enables - `crdt`, and the gate list runs `--features crdt` only for `--lib` — a - crdt-gated integration test is **dark twice over**. -- The whole expansion has cross-peer-degraded undo (Q#LN21): six - source-peer optimistic inserts replaced by one daemon-peer op. - `set_round_trip_input` would fix it and is rejected — it also disables - `dispatch_idle`, so RET stops inserting a newline. -- Table facts re-derived at `17d1d08`: 1,855 entries, 36,861 bytes, all - keys ASCII, **64** keys carry a `lean4` pair-set char, **305** keys are - proper prefixes of another (so 1,550 expand eagerly), **26** values - carry `$CURSOR`, and **119** are multi-codepoint — the 26 - `$CURSOR`-bearing values plus 93 others. -- Citation sweep per COHERENCE §25: five live citations moved in the 50 - commits since rev 5 — `take_typed_edit` 12827→12990, - `handle_server_requests` 1549→1815, `fs.stat` 93→133, - `detect_buffer_language` 452→457, `send_request`/`send_notification` - 9342/9361→9507/9527. -### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch) - -- Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua` - (new), `pair.lua` re-expressed as one consumer, - `src/editor.rs` +15 (the `include_str!` and its ordering comment), and - `tests/typed_edit_chain_acceptance.rs` (new, 13 tests). - **`tests/auto_pair_acceptance.rs` is UNCHANGED — `git diff --stat - main...HEAD -- tests/auto_pair_acceptance.rs` is empty.** That is - criterion 46 checked at the diff, which is the only way it means - anything. -- **The chain calls consumers even when the record is nil.** This is a - decision, not an implementation detail: three existing auto-pairing - tests assert `pmacs.pair._last_record == nil` after a record-less - fan-out (paste, programmatic insert, nested manual `hook.run`), so - skipping consumers on nil fails them. Stage 4b needs the same - delivery to abandon a pending abbreviation an unrelated edit - invalidated. -- **Ordered insertion, not `table.sort`** — Lua's sort is not stable, and - "ties broken by registration order" is a stated contract. -- **The chain `pcall`s each consumer** and reports through - `set_status`. Rev 7 justified this by claiming an uncontained throw - would fail the fan-out for every other subscriber including lsp.lua's - didChange flush; **that is wrong** — `run_all_must_succeed` - (`src/hook.rs:332`) collects errors and continues, so the other - subscribers still run. The real consequence is narrower and still - worth containing: the throw skips every LATER consumer in the chain. - The rendering is protected too, because a Lua error may be a table - whose `__tostring` throws. -- **Round 8 (review) findings, all fixed on this branch:** each consumer - now gets its **own shallow copy** of the record (the same table let a - declining consumer rewrite `rec.char`, which pairing reads — typing - `x` could produce `x)`); the fan-out iterates a **snapshot** (a - consumer registering a lower-priority one shifted itself forward under - `ipairs` and ran twice, unbounded if repeated); `tostring` moved - inside the containment; **non-finite and non-integer priorities are - rejected** (NaN is a number and every ordered comparison with it is - false, so it landed wherever the insertion scan gave up and silently - voided the ordering contract); and `add_consumer` now returns a handle - with `remove_consumer` beside it, so re-evaluating a config no longer - leaks callbacks the way `pmacs.hook.add` does (COHERENCE §13). -- **Every acceptance test is bite-verified by mutation**, per the - standing rule that a test is not evidence until the mutation it - targets has been shown to fail it: +- Framing `docs/lean4-mode-framing.md` **revision 12** (rounds 10, 11 + and 12 = review of the implementation). Stage + 4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b, + the Lean content that registers on it. +- Footprint: `scripts/regen-lean-abbrev` (new, the generator), + `builtin/runtime/lean_abbrev.lua` (new, VENDORED DATA — 1,855 entries + from `leanprover/vscode-lean4@17d1d08`, Apache-2.0), + `builtin/runtime/lean_input.lua` (new, the consumer at priority 50), + `src/editor.rs` (two `include_str!` blocks), + `tests/lean_input_acceptance.rs` (new, 31 tests), and one + `#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs` + (acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart + from the load sites and that one test. +- **Round 9 corrected three acceptance criteria that the real table + contradicts** — found by simulating the state machine over all 1,855 + entries and re-reading upstream at the pinned commit, not by reading + the prose again. `\to` is NOT eager (`top`, `to0`, `toa` extend it); + `\zzzz` expands to `ζzzz ` because `ze`/`zeta`/`zsqrtd` exist, and + only `$ % , ; @ W` open no key at all; and `\alpha`'s undo does not + restore `\alpha ` because `alpha` IS eager, so the terminator is a + separate edit. Criteria 38, 41 and 42 now state both paths. +- **Two generator bugs, both caught by its own round-trip check + failing closed:** `str.splitlines()` also splits on U+2028/U+2029, + and 53 symbols contain one literally, so the check reported a count + mismatch that was its own bug; then escaping via `chr(byte)` produced + a latin-1-shaped string that `write_text(encoding="utf-8")` + re-encoded, and every non-ASCII symbol landed double-encoded. The + first version of the check compared IN-MEMORY strings and agreed with + itself. **It now stages the file, re-reads the bytes from disk, and + renames into place only on a match.** +- **The point must be placed explicitly after the replace.** The + expansion SHRINKS the buffer (`\alpha` 6 bytes → `α` 2), so a point + left at the pre-edit offset is past the new end and every later + self-insert is silently rejected — the editor looks dead after the + first expansion. Pairing's "no cursor motion on the clean path" does + not generalize: that holds only for an insert AT the cursor. +- **Three tests were vacuous when first written and were found by + biting, not by review:** the abandonment test asserted text that a + wrongly-surviving record would also produce (claiming makes no edit — + it needed the follow-up keystroke that completes an eager key); the + re-arm test used the framing's own `\alpha\to`, which never reaches + the re-arm branch because `alpha` is eager and closes the record + first (`\al\to` does); and both buffer-switch tests passed through + `find_or_open`'s fresh-load path, which fires `buffer.after-load` and + a record-less edit rather than `buffer.after-switch` — deleting the + subscriber left them green. All three now bite. +- **Bite table** (each mutation, and the tests it fails): | Mutation | Tests it fails | |---|---| - | append instead of ordered insert | 5 chain | - | `>=` instead of `>` in the insert scan | 1 chain (tiebreak) | - | re-take the record per consumer | 4 chain | - | ignore the claim return value | 1 chain | - | drop the `pcall` | 1 chain | - | skip consumers when `rec == nil` | 1 chain + **3 auto-pair** | - | load `typed_edit.lua` after `lsp.lua` | 1 chain + **2 auto-pair** (Q#AP7) | - | hand every consumer the same record table | 1 chain (46f) | - | iterate the live array instead of a snapshot | 1 chain (46g) | - | render the error outside the `pcall` | 1 chain (46d) | - | accept any Lua number as a priority | 1 chain (46h) | - | make `remove_consumer` a no-op | 2 chain (46g, 46h) | + | register at priority 150 (after pairing) | 2 | + | claim only completed expansions | 2 | + | longest match instead of shortest | 9 | + | equal-length tie keeps the LATER key | 3 | + | remove the eager branch | 8 | + | expand without the terminator in the span | 2 | + | remove the re-arm branch | 1 | + | remove the point-still-at-span-end check | 1 | + | remove the exact-revision check | 1 | + | leave the point where the replace found it | 5 | + | remove the `lean4` language gate | 1 | + | remove the `lean.abbrev` gate | 2 | + | `buffer.after-switch` clears every frontend | 1 | + | delete the `buffer.after-switch` subscriber | 1 | + | `frontend.detached` purges every frontend | 1 | + | claim the terminator | 1 | + | expand inside the chain, then decline | 2 | + | drop the `cursor() == post_cursor` check | 1 | + | place the point without the context guard | 1 | + | load lean_input.lua after lsp.lua | 1 | + | let a nested fan-out consume the deferred slot | 1 | + | stop counting chain invocations | 1 | + | count fan-outs in the expander instead of the sentinel | 1 | - The first attempt at the last bite was WORTHLESS as written: moving - only `typed_edit.lua` past `lsp.lua` left `pair.lua` calling a nil - `add_consumer`, so the runtime failed to load and all 9 tests died — - loud, but not a test of the flush-ordering property. Moving - `typed_edit.lua` AND `pair.lua` past `lsp.lua` is the faithful - falsification: registration succeeds, the hook lands late, and exactly - the three ordering tests fail. **A bite that kills everything has not - isolated anything.** -- Verification on this branch (commit-then-gate, so this describes the - pushed tree): `cargo fmt --check` clean; strict workspace Clippy - clean; 1,832 default + 2,009 CRDT library tests; auto-pair 45/45; - typed-edit chain 13/13 (and 13/13 again under `--no-default-features - --features lua54`, since the fixes touch `math.huge`, `%`, and - `__tostring` behavior that differs between the backends); M4 121; - required GPU 202; **isolated-config workspace sweep 3,332 across 97 - suites, zero failures** with `grep -c basedpyright` = 0; `git diff - --check` clean. -- Stage 4b (the input method) is NOT in this PR and not started. + Acceptance 45f bit by construction: without a registered window for + the source frontend it ran six fan-outs with a nil record and proved + nothing, because `handle_remote_crdt_op` arms nothing unless the + source's active window displays the buffer. +- **Round 10 (review) found three defects, all about what happens + AROUND the expansion rather than about resolving an abbreviation.** A + pair character that TERMINATES an abbreviation never reached pairing + (`\alp(` gave `α(`): the first revision claimed the terminator, and + merely declining is not enough either, because the chain hands each + consumer a copy of the record made before any consumer ran — so + expanding inside the chain invalidates pairing's copy and the closer + is lost anyway (verified by mutation, not assumed). The expansion now + runs on **its own `buffer.after-edit` subscriber** after the chain, + with a span that stops before the terminator. That is a new instance + of Q#AP7, so it is now pinned with the sighelp fake server. + Post-insert point motion was also mistaken for a valid span (the + relevance check needs `cursor() == post_cursor`, as pairing's has + since #110), and cursor placement could move a buffer an intercept + had switched to. +- **Round 11 found the round-10 fix incomplete in one place: + `buffer.after-edit` fan-outs NEST.** A consumer between the expander + (50) and pairing (100) that calls `pmacs.hook.run("buffer.after-edit")` + re-enters the expander's subscriber while the OUTER chain is still + mid-list; the nested pass expanded and outer pairing then resumed with + an invalidated record — `α(` again, through the chain's documented + re-entrancy seam instead of through claiming. **Deferring work past a + fan-out means owning which fan-out it belongs to.** The chain's + subscriber and the expander's each run exactly once per fan-out, so + counting the first and matching it off in the second identifies the + nesting level with no new seam in merged Stage 4a substrate. +- **Round 12 found round 11's counter in the wrong place.** It counted + invocations of the EXPANDER, which is optional: a lower-priority + consumer can claim and stop the chain before the expander runs, while + that fan-out's deferred subscriber still runs — so the nested pass + went uncounted, looked outermost, expanded early, and outer pairing + resumed with an invalidated record. The count now comes from a no-op + consumer at the MINIMUM priority, which runs first in every chain + invocation that reaches any consumer, and degrades safely: the only + thing that can skip it is a claim ahead of it, which skips the + expander too. A subscriber registered beside `run_deferred` cannot + serve — the whole nested fan-out completes inside the outer chain's + subscriber, before it would run. +- **Rounds 10–12 share a shape worth naming.** Each fix was correct + about the failure it was shown and wrong about the boundary of the + mechanism it leaned on — first the chain's copy semantics, then its + re-entrancy, then its short-circuit. **A queue that outlives the + thing that filled it has to name that thing, not approximate it.** +- Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED, + named in the module header (Q#LN21): six source-peer optimistic + inserts replaced by one daemon-peer op. `set_round_trip_input` would + fix it and also disables `dispatch_idle`, so RET would stop inserting + a newline. ## The CRDT half of the test corpus is dark in CI — NEEDS A LANE diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index b2a0c45..67e7b43 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -37,7 +37,8 @@ commands, read `docs/active-work.md` immediately after this file. ## 1. Where the project stands (2026-07-26) -- `main` @ `a27f646` (Lean 4 Stage 4a #179 atop bottom-panel Stage 2A +- `main` @ `74301d1` (the dired Stage 1 landed-doc refresh #169 atop + Lean 4 Stage 4a #179, bottom-panel Stage 2A #177, the bottom-panel Stage 2 framing #175, terminal configuration Stage 1 #173, Lean 4 Stage 3b #170, Stage 3a #167, the CRDT undo repro #157, the inline-math landed-doc refresh #172, the bottom-panel @@ -101,9 +102,9 @@ commands, read `docs/active-work.md` immediately after this file. config swap invalidates. The durable lesson is to heal at **consumption** — the point where a stale record is handed out — not at the moment of the swap. - - **Stage 4a (typed-edit consumer chain) is implemented and in review - as PR #179** (branch `lean4-stage4a-typed-edit-chain`, framing rev - 8). It is substrate only: `builtin/runtime/typed_edit.lua` owns the + - **Stage 4a (typed-edit consumer chain) MERGED as #179** (`main` @ + `a27f646`, two review rounds). It is substrate only: + `builtin/runtime/typed_edit.lua` owns the single `buffer.after-edit` subscriber and the single one-shot read, `pair.lua` becomes its first registered consumer, and `tests/auto_pair_acceptance.rs` is unchanged by zero lines @@ -117,10 +118,51 @@ commands, read `docs/active-work.md` immediately after this file. iterates a **snapshot**, because a consumer that registers a lower-priority one shifts itself forward under `ipairs` and runs twice. - - Remaining: Stage 4b (the Unicode input method) is framed and - awaiting approval — not started; stages 5 (goal panel), 6 (`#eval` - output channel), and 7 (module hierarchy) are framed but not - scouted against current `main`. + - **Round 8's durable lesson: `run_all_must_succeed` does NOT abort + the fan-out.** `src/hook.rs:332` collects each callback's error and + continues to the remaining subscribers, marking only the run + failed — so an uncontained throw inside a hook subscriber does not + stop `lsp.lua` from flushing didChange. Two framing revisions + asserted the opposite to justify a `pcall`. The guard was right and + the reason was wrong, and by the time review caught it the wrong + reason had been copied into a module comment, an acceptance + criterion, a test comment, and the ledger. **Correct the source a + rationale derives from, not only the sites that quote it.** + - **Stage 4b (the Unicode input method) is implemented and in review** + (branch `lean4-stage4b-input-method`, framing rev 9): a vendored + 1,855-entry table generated from `leanprover/vscode-lean4@17d1d08` + by `scripts/regen-lean-abbrev`, plus a consumer registered on the + Stage 4a chain at priority 50, ahead of pairing. **A consumer + cannot both edit and let a later consumer act on the same + keystroke**: the chain hands each consumer a copy of the record made + before any consumer ran, so an edit invalidates every copy still to + be used. The expansion therefore runs on a SECOND + `buffer.after-edit` subscriber after the chain — which is how a + pair character that terminates an abbreviation still pairs + (`\alp(` → `α()`). And **deferring work past a fan-out means + owning which fan-out it belongs to**: these fan-outs NEST, so a + consumer between the expander and pairing that calls + `pmacs.hook.run` re-enters the deferred subscriber while the outer + chain is still mid-list, and the count that recognises this has to + come from a MINIMUM-PRIORITY consumer — the expander is optional + (a claim can stop the chain first) and a subscriber beside the + deferred one is too late (the nested fan-out finishes inside the + outer chain's subscriber). Its other durable facts: + the table must stay an ORDERED SEQUENCE (equal-length ties resolve + by source declaration order, which a `pairs`-iterated map cannot + express); a generator round-trip check must re-read the BYTES ON + DISK, because comparing in-memory strings cannot see an encoding + applied by the write itself; and an expansion that SHRINKS the + buffer must place the point explicitly, or every later self-insert + is silently rejected and the editor looks dead. + - **Round 9 corrected three approved acceptance criteria** by + simulating the state machine over all 1,855 entries rather than + re-reading the prose. Four review rounds over the text had not + found them, because each named an example that reads as obviously + right and is wrong only against the data. + - Remaining: stages 5 (goal panel), 6 (`#eval` output channel), and 7 + (module hierarchy) are framed but not scouted against current + `main`. - **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3; merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index c4a32e5..20c66b4 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -46,7 +46,7 @@ during a rebase. ## 0.1 Revision history -Revision 1 — initial. Current revision: **8**. +Revision 1 — initial. Current revision: **12**. ### Round 1 (rev 1 → rev 2) @@ -503,6 +503,110 @@ documentation cleanups. others — matching §2.11 and Q#LN11. 3. **§9.1's revision label was stale.** It now names rev 8. +### Round 9 (rev 8 → rev 9) + +Found during Stage 4b implementation, by simulating Q#LN22's state +machine over all 1,855 vendored entries and re-reading upstream's +`TrackedAbbreviation.ts` and `AbbreviationProvider.ts` at `17d1d08`. +**Three acceptance criteria named examples that the real table +contradicts** — every one of them written from what the abbreviation +*looks* like rather than from whether the table makes it eager. + +1. **Acceptance 41 was false.** `\to` does not expand eagerly: `to` is a + proper prefix of `top`, `to0`, `toa` and others, so upstream's + `isAbbreviationUniqueAndComplete` is false and `to` is not among the + 1,550 eager keys. The criterion now uses `\alpha`, which has no + extension, and additionally pins that `\to` alone does **not** + expand — the false half is worth an assertion because it reads as + correct until the table is consulted. +2. **Acceptance 42 was false.** `\zzzz` + space yields `ζzzz `, not + literal text: `z` opens a pending abbreviation (`ze`, `zeta`, + `zsqrtd`) and the second `z` finishes it. Exactly six printable + characters open no key — `$ % , ; @ W` — and the criterion now uses + `\WWWW`. +3. **Acceptance 38's undo claim was false for its own example.** + `alpha` is eager, so `\alpha` expands before the space is typed and + the space is a separate edit; one undo removes the space rather than + restoring `\alpha `. The criterion now states the finish path and the + eager path separately, since "one expansion is one undo step" is true + of both while the text an undo restores is not. + +The mechanism (Q#LN11, Q#LN21, Q#LN22) needed no change — these were +errors in the examples chosen to pin it, which is why a simulation over +the real data found them and four review rounds over the prose did not. + +### Round 10 (rev 9 → rev 10) + +Review of the Stage 4b implementation. Three defects in the expander, +all of them about what happens AROUND the expansion rather than about +resolving an abbreviation, plus one stale count. + +1. **A pair character that terminates an abbreviation never reached + auto-pairing.** Q#LN22 already said the terminator is not claimed; + the implementation claimed it whenever an expansion succeeded, so + `\alp(` gave `α(`. Not claiming is necessary and not sufficient — + the chain hands each consumer a copy of the record made before any + consumer ran, so expanding inside the chain invalidates the copy + pairing is holding and the closer is lost anyway. Q#LN22 now + specifies the deferred subscriber and the span that stops before the + terminator; acceptance 45j pins all three failure modes. +2. **Post-insert point motion was mistaken for a valid pending span.** + The relevance check compared buffer and window but not + `ed.cursor() == rec.post_cursor`, so a redefined self-insert that + inserts and then moves the point still expanded — and teleported the + point back. Pairing has made this three-part check since #110. + Acceptance 45k. +3. **Cursor placement could move the wrong buffer.** A buffer intercept + may switch buffers during `buf:replace`; the unguarded `goto_byte` + afterwards moved the switched-to buffer's point. `repair_cursor` is + the precedent. Acceptance 45l. +4. **The coherence census contradicted itself** — nine settings in one + paragraph, eight three paragraphs below. + +Acceptance 45m was added with them: the expansion now runs on its own +`buffer.after-edit` subscriber, which is a new instance of Q#AP7 and +was unpinned. + +### Round 11 (rev 10 → rev 11) + +One P1 in the round-10 fix, and one stale comment. + +1. **The deferred expansion was not tied to the fan-out that queued + it.** `buffer.after-edit` fan-outs nest — the typed-edit contract + supports a consumer calling `pmacs.hook.run` — and a nested run + re-enters the expander's subscriber while the OUTER chain is still + mid-list. A consumer at priority 75 running one nested fan-out made + `\alp(` yield `α(` again: the nested pass expanded, and outer + pairing then resumed with a record the replace had invalidated. + Round 10's own failure mode, reached through re-entrancy instead of + claiming. Q#LN22 now specifies matching chain invocations against + expander invocations so only the outermost pass expands; acceptance + 45n pins it. +2. **A test comment still described the discarded span design** — it + said the expansion replaces the span "INCLUDING the terminator", + which round 10 deliberately stopped doing. The behaviour it asserts + was correct; only the explanation was stale. + +### Round 12 (rev 11 → rev 12) + +One P1: round 11's counter was in the wrong place. + +1. **The nesting count lived in the expander, which is optional.** A + consumer at a lower priority can claim and stop the chain before the + expander runs, while that fan-out's deferred-expansion subscriber + still runs — so the nested pass went uncounted, looked like the + outermost one, expanded early, and outer pairing resumed with an + invalidated record. `\alp(` gave `α(` again. The count now comes + from a no-op consumer at the minimum priority, which runs first in + every chain invocation that reaches any consumer; acceptance 45o + pins the short-circuit path that 45n does not reach. + +The pattern across rounds 10–12 is worth naming: each fix was correct +about the failure it was shown and wrong about the boundary of the +mechanism it relied on — the chain's copy semantics, then its +re-entrancy, then its short-circuit. **A queue that outlives the thing +that filled it needs to name that thing, not approximate it.** + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -1686,8 +1790,9 @@ reconstruction of it: - A subsequent self-insert `c` is claimed iff at least one key has `text .. c` as a prefix; then `text = text .. c`. If it is also uniquely-and-completely matching (one of the 1,550), expand now. -- If no key extends `text .. c`, expand `text` **first**, then let `c` - land normally — the chain does *not* claim `c`. +- If no key extends `text .. c`, `c` TERMINATES the abbreviation: the + chain does *not* claim it, and the expansion of `text` is + **deferred** until after the chain has run (round 10; see below). - **A terminating `c` that is itself `\` is then reprocessed as a new leader**, opening a fresh pending abbreviation at its position. This is the rule acceptance 45d depends on (`\alpha\to` → `α→`) and rev 6 @@ -1701,6 +1806,69 @@ reconstruction of it: broken by source rank, unmatchable tail appended (`\alp7` → `α7`). - `$CURSOR` is stripped from the symbol and its index becomes the point. +**The expansion is deferred past the chain, and its span stops before +the terminator** (round 10). "Not claiming the terminator" is necessary +and not sufficient: a pair character is a legal terminator (`\alp(` must +give `α()`), and the chain hands every consumer a *copy* of the record +made before any consumer ran. So expanding inside the chain and then +declining leaves auto-pairing holding offsets the replace has already +invalidated — pairing declines and the closer is silently lost, which a +probe confirmed. Claiming the terminator instead suppresses pairing +outright. Neither is recoverable from inside the chain. + +The expander therefore records the pending expansion and performs it on +its **own `buffer.after-edit` subscriber**, registered after +typed_edit.lua's and before lsp.lua's. A claim by any consumer stops the +chain but not a separate subscriber — which is the point, since pairing +claims the terminator it reacts to. The replaced span covers the leader +and the typed text only; whatever pairing did lands after it and +survives untouched. One undo restores the same text either way, because +the terminator was always its own insert. + +**The deferred expansion must belong to its own fan-out** (round 11). +`buffer.after-edit` fan-outs NEST — Q#AP9 and typed_edit.lua's header +both say so explicitly, and a consumer may call `pmacs.hook.run`. A +nested run re-enters every subscriber, including the deferred +expansion's, while the OUTER chain is still walking its consumer list +and pairing has not yet seen the terminator. A nested pass that +performed the expansion would reproduce the exact bug deferring exists +to fix, reached through the chain's documented re-entrancy seam instead +of through claiming. + +The nesting level is counted by a **no-op consumer registered at the +minimum priority**, matched off in the expander's subscriber. Only the +outermost pass expands; a nested one leaves the expansion queued. No +new seam in typed_edit.lua, which is merged substrate. + +Where the count lives is the whole difficulty, and two plausible places +are both wrong (round 12): + +- **A subscriber registered beside the expander's is too late.** The + entire nested fan-out completes inside the OUTER chain's subscriber, + before any subscriber registered after it runs. +- **The expander itself is optional.** A lower-priority consumer may + claim and stop the chain before the expander is reached, so a nested + pass would go uncounted while its `run_deferred` still ran — and + would then look like the outermost one. + +A minimum-priority consumer runs first in every chain invocation that +reaches any consumer at all. Its guarantee is exactly the ordering +contract the chain already rests on, and it degrades safely: the only +thing that can skip it is a claim ahead of it, which skips the expander +too, so nothing is queued in that fan-out either. + +Two guards this exposes, both of which pairing already carries: + +- The relevance check is **three-part**, not two: buffer, window, **and + `ed.cursor() == rec.post_cursor`**. A redefined self-insert can insert + the completing character and then move the point, and expanding over a + span the user has left teleports them back into it. +- Cursor placement after the replace is **context-guarded**. A buffer + intercept may switch window or buffer while `buf:replace` runs; an + unguarded `goto_byte` then moves the point of a buffer that has + nothing to do with the expansion. `pair.lua`'s `repair_cursor` is the + precedent. + **Ownership is per frontend, not per buffer** (§2.11). The key is `(pmacs.frontend.id(), rec.buffer)`, and the stored `window` must still match `rec.window` for the state to be usable — a frontend that moved @@ -2452,12 +2620,25 @@ criterion 46 requires to stay byte-identical. **Stage 4b — the Unicode input method** -38. `\alpha` + space yields `α ` — the space lands first and the - expansion runs in the following `buffer.after-edit`, so the - terminator is **retained**, not consumed. The expansion is a single - undo step: one undo restores `\alpha ` (with its space), not - `\alph`. Rev 6 wrote the post-undo text as `\alpha`, which would be - true only if the terminator were swallowed. +38. **Terminators are retained, and one expansion is one undo step — + but which text an undo restores depends on the path.** Rev 8 stated + a single rule here and it is wrong against the real table, because + it assumed `\alpha` takes the finish path when `alpha` is in the + 1,550-key eager set (round 9; see 41). + - *Finish path.* `\alp` + space yields `α `: the space lands first + and the expansion runs later in the same `buffer.after-edit` + fan-out, so the terminator is **retained**, not consumed. It sits + OUTSIDE the replaced span, which covers only the leader and the + typed text (round 10) — the observable text and the post-undo + text are the same either way, because the terminator was its own + insert. One undo restores `\alp ` — with its space, not `\al`. + Rev 6 wrote the post-undo text without the terminator, which + would be true only if the terminator were swallowed. + - *Eager path.* `\alpha` yields `α` with no terminator typed, and a + following space is a **separate** edit. One undo removes the + space; a second restores `\alpha`. Asserting the finish-path undo + text here would fail, which is the trap this split exists to + record. 39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR` placeholder. 40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is @@ -2467,9 +2648,21 @@ criterion 46 requires to stay byte-identical. only completed expansions rather than pending extensions — **both failure modes must be shown**, since they are distinct bugs with the same symptom. -41. `\to` yields `→` eagerly on uniqueness, with no terminator typed. -42. A prefix with no match (`\zzzz` + space) is left as literal text; no - edit is made. +41. **Eager expansion on uniqueness**, with no terminator typed: + `\alpha` yields `α` the moment the final `a` lands. Rev 8 used `\to` + here and that is false against the real table (round 9): `to` is a + proper prefix of `top`, `to0`, `toa` and others, so + `isAbbreviationUniqueAndComplete` is false and `to` is **not** in + the 1,550-key eager set. `\to` alone stays `\to`; `\to` + space + yields `→ ` by the finish path. Both are asserted, because the + wrong one reads as correct until the table is consulted. +42. A prefix that opens no key at all — `\WWWW` + space — is left as + literal text and **no edit is made**. Rev 8 used `\zzzz`, which + expands (round 9): `z` opens a pending abbreviation because `ze`, + `zeta` and `zsqrtd` exist, and the second `z` finishes it, giving + `ζzzz `. Exactly six printable characters open no key: `$ % , ; @ + W`. Bites against an implementation that treats "no complete match" + as "no pending state". 43. **Lazy abandonment (Q#LN22).** Because there is no cursor-motion hook, this asserts what pmacs can actually detect: after `\alp`, an explicit `goto_byte` elsewhere followed by typing `h` inserts a @@ -2544,6 +2737,49 @@ criterion 46 requires to stay byte-identical. `$CURSOR` more than once; - the resolution spot-set behaves: `alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`, and the tie cases from 45h. +45j. **A pair character that TERMINATES an abbreviation still pairs** + (round 10). `\alp(` yields `α()` with the point between the pair. + Bites three ways, all of which produce different wrong answers: + claiming the terminator gives `α(`; expanding inside the chain and + then declining also gives `α(`, because the replace invalidates the + record copy pairing is holding; and pairing running first gives + `\alp()` unexpanded. Criterion 40 is the same collision from the + other side, and passing it says nothing about this one. +45k. **The relevance check is three-part.** A redefined + `buffer.self-insert` that inserts the completing character and then + moves the point must not expand: `\alph` + `a` under such an + override leaves literal `\alpha` with the point where the command + put it. Bites against checking only buffer and window — the + expansion would otherwise teleport the point back into a span the + user has left. +45l. **Cursor placement is context-guarded.** A buffer intercept that + switches buffers during `buf:replace` must not have the + switched-to buffer's point moved. Bites against an unguarded + `goto_byte`, which translates the LEAN buffer's pre-edit point + through the LEAN buffer's edit and applies it to whatever is + ambient. +45m. **Q#AP7 for the deferred subscriber.** The expansion runs on a + second `buffer.after-edit` subscriber, so it inherits pairing's + flush-ordering obligation: no `didChange` may ever carry the + unexpanded text. Pinned with the `sighelp` fake server and `(` as + the trigger — the flush carrying the terminator carries `α()`. + Falsified by loading lean_input.lua after lsp.lua. +45n. **A nested fan-out must not expand early** (round 11). A consumer + registered BETWEEN the expander and pairing that calls + `pmacs.hook.run("buffer.after-edit")` once still yields `α()` for + `\alp(`. Bites against a deferred slot consumed by whichever + fan-out happens to reach it: the nested pass would expand, and the + outer chain would then hand pairing a record the replace had + invalidated — the round-10 failure again, through the chain's + documented re-entrancy seam rather than through claiming. +45o. **A nested fan-out that never reaches the expander must not + expand early either** (round 12). Same shape as 45n, but the nested + pass is short-circuited by a consumer at priority 25 that claims + when the record is nil — so the expander never runs on it. Bites + against counting fan-outs in the expander, which is optional by + construction: the uncounted nested pass looks outermost, expands, + and outer pairing resumes with an invalidated record. 45n passes + against that bug, which is why both are pinned. 45h. **Tie-break by source order (§2.11).** `\f` + space yields `‹` — `f<` and `f>` are both length 2, and `f<` is declared first. Same for `\"` + space → `Ä`, first of eleven equal-length candidates. @@ -2698,7 +2934,7 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from languages other than Lean, and §4's rule is what keeps them out of a Lean PR. -### 9.1 Coherence impact — stages 4a and 4b (rev 8) +### 9.1 Coherence impact — stages 4a and 4b (rev 12) **Sections served.** §6 (interaction islands) primarily, and in the *preventing* direction rather than the fixing one — see below. §11 diff --git a/scripts/regen-lean-abbrev b/scripts/regen-lean-abbrev new file mode 100755 index 0000000..14091aa --- /dev/null +++ b/scripts/regen-lean-abbrev @@ -0,0 +1,254 @@ +#!/usr/bin/env python3 +"""Regenerate builtin/runtime/lean_abbrev.lua from vscode-lean4. + +Usage: scripts/regen-lean-abbrev + +Fetches `lean4-unicode-input/src/abbreviations.json` at the given commit +and rewrites the vendored Lua table, including the provenance header, so +the artifact is self-describing to whoever next touches it. A refresh is +an ordinary PR with a visible diff — the diff is the review. + +There is no automatic sync and none is wanted: an editor that silently +re-downloads its input method has a supply-chain problem, not a feature +(docs/lean4-mode-framing.md Q#LN11). + +The emit is an ORDERED SEQUENCE, not a map. Upstream resolves +equal-length abbreviation ties by source declaration order — 101 +prefixes depend on it — and a Lua `{ [key] = symbol }` table iterated +with `pairs` cannot carry that. A map-shaped emit would also be +nondeterministic across builds and, once a hash order happened to be +stable, stably wrong. + +This script ABORTS rather than emitting something plausible when the +source is corrupt: a duplicate key after decoding (JSON permits them, +the table must not), a key or symbol that is not well-formed UTF-8, or a +round-trip mismatch. That last check re-parses the script's own output +with an independent unescaper and compares the full ordered sequence to +the source, entry for entry. It is what makes the vendored file +trustworthy, and it belongs here rather than in the acceptance suite: +the suite cannot see `abbreviations.json`, which is not shipped. +""" + +import json +import pathlib +import sys +import urllib.request + +REPO = "leanprover/vscode-lean4" +PATH = "lean4-unicode-input/src/abbreviations.json" +LICENSE = "Apache-2.0" +OUT = pathlib.Path(__file__).resolve().parent.parent / "builtin/runtime/lean_abbrev.lua" + +# Canonical, lossless, byte-deterministic. Rev 6 of the framing said the +# generator should abort on "a key containing a character the emitted Lua +# would have to escape"; that rule rejects the real table, where `\` is a +# key and `"` begins eleven of them. +SHORT = {"\\": "\\\\", '"': '\\"', "\n": "\\n", "\r": "\\r", "\t": "\\t"} + + +def die(msg): + print(f"regen-lean-abbrev: {msg}", file=sys.stderr) + raise SystemExit(1) + + +def lua_escape(s): + """Escape one string for a Lua double-quoted literal. + + Operates on CHARACTERS, not bytes. Decomposing to UTF-8 bytes and + emitting each as `chr(byte)` produces a latin-1-shaped string that + `write_text(..., encoding="utf-8")` then re-encodes — every + non-ASCII symbol lands in the file double-encoded, and a round-trip + check that compares in-memory strings agrees with itself and misses + it entirely. Only control bytes, which are single-byte by + definition, become `\\ddd`. + """ + out = [] + for ch in s: + if ch in SHORT: + out.append(SHORT[ch]) + elif ord(ch) < 0x20 or ord(ch) == 0x7F: + out.append(f"\\{ord(ch):03d}") + else: + out.append(ch) + return "".join(out) + + +def lua_unescape(s): + """Independent reader for the round-trip check. + + Deliberately not the inverse of `lua_escape` sharing its table: a + check that reuses the encoder's own assumptions cannot detect that + those assumptions are wrong. + """ + out = bytearray() + i = 0 + raw = s.encode("utf-8") + while i < len(raw): + b = raw[i] + if b != ord("\\"): + out.append(b) + i += 1 + continue + i += 1 + if i >= len(raw): + die("round-trip: trailing backslash in emitted string") + nxt = chr(raw[i]) + if nxt in ("\\", '"'): + out.append(ord(nxt)) + i += 1 + elif nxt in ("n", "r", "t"): + out.append({"n": 10, "r": 13, "t": 9}[nxt]) + i += 1 + elif nxt.isdigit(): + digits = "" + while i < len(raw) and chr(raw[i]).isdigit() and len(digits) < 3: + digits += chr(raw[i]) + i += 1 + out.append(int(digits)) + else: + die(f"round-trip: unknown escape \\{nxt} in emitted string") + return out.decode("utf-8") + + +def main(): + if len(sys.argv) != 2: + die(f"usage: {sys.argv[0]} ") + commit = sys.argv[1] + url = f"https://raw.githubusercontent.com/{REPO}/{commit}/{PATH}" + + with urllib.request.urlopen(url, timeout=60) as resp: + raw = resp.read() + + try: + raw.decode("utf-8") + except UnicodeDecodeError as e: + die(f"source is not well-formed UTF-8: {e}") + + # `object_pairs_hook` keeps declaration order AND exposes duplicate + # keys, which a plain dict would silently collapse. + pairs = json.loads(raw, object_pairs_hook=lambda kv: kv) + + seen = {} + for i, (key, symbol) in enumerate(pairs): + if key in seen: + die(f"duplicate key {key!r} at entries {seen[key]} and {i}") + seen[key] = i + for label, s in (("key", key), ("symbol", symbol)): + if not isinstance(s, str): + die(f"{label} at entry {i} is not a string: {s!r}") + try: + s.encode("utf-8") + except UnicodeEncodeError as e: + die(f"{label} at entry {i} is not well-formed UTF-8: {e}") + + cursor = sum(1 for _, v in pairs if "$CURSOR" in v) + for i, (key, symbol) in enumerate(pairs): + if symbol.count("$CURSOR") > 1: + die(f"symbol for {key!r} at entry {i} has more than one $CURSOR") + + body = "".join( + f' {{ "{lua_escape(k)}", "{lua_escape(v)}" }},\n' for k, v in pairs + ) + text = HEADER.format( + repo=REPO, + path=PATH, + commit=commit, + license=LICENSE, + count=len(pairs), + cursor=cursor, + bytes=len(raw), + script=pathlib.Path(sys.argv[0]).name, + ) + "pmacs.lean_abbrev = {\n" + body + "}\n" + + # Round-trip against the BYTES ON DISK, not the string in memory. + # The file is staged beside its destination, re-read, parsed, and + # only renamed into place once it compares equal entry for entry. A + # check that compares in-memory strings cannot see an encoding + # applied by the write itself, which is exactly how a + # double-encoding bug survived the first version of this script. + staged = OUT.with_suffix(".lua.staged") + staged.write_text(text, encoding="utf-8") + on_disk = staged.read_bytes().decode("utf-8") + + got = [] + # `str.splitlines()` is WRONG here: it also splits on U+2028, U+2029, + # U+0085 and the vertical-tab family, and 53 symbols in the real + # table contain one of those literally. It silently loses entries and + # the round-trip then reports a count mismatch that is the checker's + # bug, not the emit's. The emitted file's line structure is defined + # by the LF we write, and nothing else. + for line in on_disk.split("\n"): + line = line.strip() + if not line.startswith('{ "') or not line.endswith("},"): + continue + inner = line[1:-2].strip() + if not (inner.startswith('"') and inner.endswith('"')): + die(f"round-trip: unparsable emitted line: {line!r}") + fields, buf, esc, depth = [], [], False, 0 + for ch in inner: + if esc: + buf.append(ch) + esc = False + elif ch == "\\": + buf.append(ch) + esc = True + elif ch == '"': + depth += 1 + if depth % 2 == 0: + fields.append("".join(buf)) + buf = [] + elif depth % 2 == 1: + buf.append(ch) + if len(fields) != 2: + die(f"round-trip: expected 2 fields, got {len(fields)}: {line!r}") + got.append((lua_unescape(fields[0]), lua_unescape(fields[1]))) + + def fail(msg): + staged.unlink(missing_ok=True) + die(msg) + + if len(got) != len(pairs): + fail(f"round-trip: emitted {len(got)} entries, source has {len(pairs)}") + for i, (want, have) in enumerate(zip(pairs, got)): + if tuple(want) != have: + fail(f"round-trip: entry {i} differs: source {want!r} vs emitted {have!r}") + + staged.replace(OUT) + print( + f"wrote {OUT} — {len(pairs)} entries from {REPO}@{commit} " + f"({len(raw)} source bytes, {OUT.stat().st_size} emitted bytes), " + "round-trip verified against the bytes on disk" + ) + + +HEADER = """\ +-- lean_abbrev.lua --- VENDORED DATA. Do not edit by hand. +-- +-- The Lean 4 abbreviation table, generated from: +-- +-- repo: https://github.com/{repo} +-- path: {path} +-- commit: {commit} +-- license: {license} +-- entries: {count} ({cursor} carry $CURSOR) +-- source: {bytes} bytes +-- +-- Regenerate with: +-- +-- scripts/{script} {commit} +-- +-- An ORDERED SEQUENCE, not a map: upstream resolves equal-length ties +-- by source declaration order (101 prefixes depend on it), and a +-- `pairs`-iterated Lua map cannot express that. The file's own line +-- order is the audit trail. Consumers must not reorder it. +-- +-- Not fetched at runtime and not a package dependency: the input method +-- has to work offline and on first launch. Upkeep is a documented +-- manual process — see docs/lean4-mode-framing.md Q#LN11. + +pmacs = pmacs or {{}} + +""" + +if __name__ == "__main__": + main() diff --git a/src/daemon.rs b/src/daemon.rs index 84716eb..e34a6d6 100644 --- a/src/daemon.rs +++ b/src/daemon.rs @@ -3964,6 +3964,143 @@ mod tests { ); } + /// Arc 8 Stage 4b acceptance 45f: the Lean abbreviation expander + /// works on the OPTIMISTIC producer, not only on `dispatch_key`. + /// + /// This is the path most users take and the one no other Stage 4b + /// test covers. `classify_key` (`src/optimistic.rs`) returns + /// `Insert(c)` for `\` and for every ASCII letter — only the nine + /// built-in pair chars are excluded (Q#AP1) — so on a CRDT frontend + /// `\alpha` arrives here as six source-peer optimistic inserts, + /// while the expansion is a single daemon-peer replace spanning all + /// six. That asymmetry is the accepted undo degradation of Q#LN21; + /// what this pins is that the expansion happens at all. + /// + /// It lives in `--lib` deliberately: the gate list runs + /// `--features crdt` only for `cargo test --lib`, so a crdt-gated + /// INTEGRATION test would be dark in CI and dark in the gates both. + /// + /// The source frontend needs a REGISTERED WINDOW on the edited + /// buffer or nothing is armed at all — `handle_remote_crdt_op` + /// arms the record only when the source's active window displays + /// the buffer, so a source with no view fails closed and silently. + /// A version of this test without the view below passed six + /// fan-outs with a nil record and proved nothing. + #[cfg(feature = "crdt")] + #[test] + fn the_optimistic_producer_also_expands_a_lean_abbreviation() { + use crate::editor::EditorState; + use crate::protocol::FrontendId; + use crate::window::{FrontendView, Layout, Window, WindowId}; + + let dir = std::env::temp_dir().join(format!("pmacs-lean-opt-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("create temp dir"); + let path = dir.join("a.lean"); + std::fs::write(&path, "").expect("write fixture"); + + let source = FrontendId(77); + let mut editor = EditorState::new(); + editor + .lua_host + .eval(Some("test"), "pmacs.lsp.config = {}") + .expect("clear lsp config"); + editor + .lua_host + .eval( + Some("test-open"), + &format!( + "pmacs.buffer.find_or_open({:?}); pmacs.editor.goto_byte(0)", + path.display().to_string() + ), + ) + .expect("open the lean fixture"); + + let buffer_id = editor.core.borrow().active_window().buffer_id; + { + let mut core = editor.core.borrow_mut(); + let mut reg = core.registry.borrow_mut(); + reg.get_mut(buffer_id) + .expect("active buffer") + .upgrade_to_crdt(2) + .expect("upgrade to crdt"); + drop(reg); + + // The replica's own window on the shared buffer. + let text_view = { + let registry = core.registry.clone(); + let reg = registry.borrow(); + crate::text_view::TextView::new(reg.get(buffer_id).expect("buffer")) + }; + let win_id = WindowId::next(); + core.windows + .insert(win_id, Window::new(win_id, buffer_id, text_view)); + core.register_frontend_view( + source, + FrontendView { + layout: Layout::single(win_id), + active: win_id, + fold_projection: true, + panel_capable: true, + frame_geometry: None, + panel_hidden: false, + }, + ); + } + + let snapshot_bytes = { + let core = editor.core.borrow(); + let reg = core.registry.borrow(); + reg.get(buffer_id) + .expect("buffer") + .crdt_state() + .expect("crdt-backed") + .export_snapshot() + .expect("export snapshot") + }; + let peer = loro::LoroDoc::new(); + peer.set_peer_id(77).expect("set peer id"); + peer.import(&snapshot_bytes).expect("import snapshot"); + + // One op per keystroke, exactly as the attach loop's + // optimistic-apply branch produces them. + for (i, ch) in "\\alpha".chars().enumerate() { + let v_before = peer.oplog_vv(); + peer.get_text("body") + .insert(i, &ch.to_string()) + .expect("peer insert"); + let op_bytes = peer + .export(loro::ExportMode::updates(&v_before)) + .expect("export op"); + super::handle_remote_crdt_op( + &mut editor, + source, + buffer_id, + crate::rope::CrdtOp { + peer_id: 77, + bytes: op_bytes, + }, + ); + } + + let text = match editor + .lua_host + .eval( + Some("test-readback"), + "local b = pmacs.window.buffer(); return b:slice(0, b:len())", + ) + .expect("read buffer text") + { + mlua::Value::String(s) => String::from_utf8_lossy(&s.as_bytes()).into_owned(), + other => panic!("expected buffer text, got {other:?}"), + }; + assert_eq!( + text, "α", + "the abbreviation expanded on the optimistic path — the \ + record the expander reads is armed by handle_remote_crdt_op, \ + not only by dispatch_key" + ); + } + /// Q#AI9 (PR #109 round 1): the optimistic-apply arm clears an /// EMPTY anchor on the source window — the GPU always takes this /// path, and the TUI attach mirror tracks no selection state, so diff --git a/src/editor.rs b/src/editor.rs index a19971e..3b3b274 100644 --- a/src/editor.rs +++ b/src/editor.rs @@ -445,6 +445,27 @@ impl EditorState { include_str!("../builtin/runtime/pair.lua"), ) .expect("load pair builtin chunk"); + // Arc 8 Stage 4b: the Lean 4 Unicode input method. The vendored + // abbreviation table first — lean_input.lua reads it at chunk + // load to build its prefix and eager-key indexes. Both load + // after typed_edit.lua, which they register into. + // + // Load order does NOT decide whether abbreviation expansion or + // auto-pairing sees a keystroke first — the chain's priority + // does (50 vs 100), which is why Stage 4a exists. It matters + // only that the chain itself is already there. + lua_host + .eval( + Some("@pmacs/builtin/runtime/lean_abbrev.lua"), + include_str!("../builtin/runtime/lean_abbrev.lua"), + ) + .expect("load lean_abbrev builtin chunk"); + lua_host + .eval( + Some("@pmacs/builtin/runtime/lean_input.lua"), + include_str!("../builtin/runtime/lean_input.lua"), + ) + .expect("load lean_input builtin chunk"); lua_host .eval( Some("@pmacs/builtin/runtime/lsp.lua"), diff --git a/tests/lean_input_acceptance.rs b/tests/lean_input_acceptance.rs new file mode 100644 index 0000000..9b6a3b8 --- /dev/null +++ b/tests/lean_input_acceptance.rs @@ -0,0 +1,1020 @@ +//! Lean 4 Unicode input method acceptance (Arc 8 Stage 4b, +//! docs/lean4-mode-framing.md Q#LN11/Q#LN21/Q#LN22, criteria 38–45i). +//! +//! Dispatch-driven throughout: `dispatch_key` is the producer that arms +//! the typed-edit record for a grid frontend. The optimistic CRDT +//! producer is criterion 45f and lives in a `--lib` test, where the gate +//! list's `--features crdt` run reaches it. + +use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers}; +use pmacs::editor::EditorState; +use pmacs::lua_bindings::StateDir; +use pmacs::protocol::FrontendId; +use pmacs::window::{FrontendView, Layout, Window, WindowId}; +use std::path::PathBuf; +use std::sync::atomic::{AtomicUsize, Ordering}; +use std::time::{Duration, Instant}; + +fn fresh_dir() -> PathBuf { + static SEQ: AtomicUsize = AtomicUsize::new(0); + let dir = std::env::temp_dir().join(format!( + "pmacs-leaninput-{}-{}", + std::process::id(), + SEQ.fetch_add(1, Ordering::Relaxed) + )); + std::fs::create_dir_all(&dir).unwrap(); + dir +} + +fn key(code: KeyCode) -> KeyEvent { + KeyEvent { + code, + modifiers: KeyModifiers::NONE, + kind: KeyEventKind::Press, + state: KeyEventState::NONE, + } +} + +fn exec(s: &EditorState, src: &str) { + s.lua_host.lua().load(src.to_string()).exec().unwrap(); +} + +fn eval(s: &EditorState, src: &str) -> T { + s.lua_host.lua().load(src.to_string()).eval().unwrap() +} + +fn text(s: &EditorState) -> String { + let b: mlua::String = eval( + s, + "local b = pmacs.window.buffer(); return b:slice(0, b:len())", + ); + String::from_utf8_lossy(&b.as_bytes()).into_owned() +} + +fn cursor(s: &EditorState) -> i64 { + eval(s, "return pmacs.editor.cursor()") +} + +fn type_as(s: &mut EditorState, fid: FrontendId, chars: &str) { + for ch in chars.chars() { + s.dispatch_key(fid, key(KeyCode::Char(ch))); + } +} + +fn type_str(s: &mut EditorState, chars: &str) { + type_as(s, FrontendId::LOCAL, chars); +} + +/// An editor with an empty `.lean` file open and the point at 0. +/// `pmacs.lsp.config = {}` keeps the real user config from spawning a +/// server; the language still resolves from the extension. +fn lean_editor() -> (EditorState, PathBuf) { + let dir = fresh_dir(); + let f = dir.join("a.lean"); + std::fs::write(&f, "").unwrap(); + let s = EditorState::new(); + exec(&s, "pmacs.lsp.config = {}"); + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + assert_eq!( + eval::>( + &s, + "return pmacs.lsp.buffer_language(pmacs.window.buffer())" + ) + .as_deref(), + Some("lean4"), + "the fixture must actually be a lean4 buffer, or every \ + expansion assertion below is vacuous" + ); + (s, f) +} + +// --------------------------------------------------------------------------- +// 38 / 41 — the two expansion paths, and what an undo restores +// --------------------------------------------------------------------------- + +#[test] +fn the_finish_path_retains_the_terminator_in_one_undo_step() { + // `alp` is not a key; `alpha` is the shortest key extending it. The + // space does not extend anything, so it lands first and the + // expansion replaces the leader and the typed text — the span stops + // BEFORE the terminator, so whatever auto-pairing did with it + // survives. One undo restores the same text either way, because the + // terminator was its own insert to begin with. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp "); + assert_eq!(text(&s), "α ", "terminator retained, not consumed"); + + exec(&s, "pmacs.window.buffer():undo()"); + assert_eq!( + text(&s), + "\\alp ", + "one undo restores the pre-expansion text WITH its terminator — \ + the expansion is a single edit" + ); +} + +#[test] +fn the_eager_path_takes_no_terminator_and_undoes_separately() { + // `alpha` has no longer key extending it, so it is one of the 1,550 + // eager keys: it expands the moment the final `a` lands, and a + // following space is a SEPARATE edit. Rev 8 asserted the finish-path + // undo text for this example, which is the trap (round 9). + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "α", "eager expansion, no terminator typed"); + + type_str(&mut s, " "); + assert_eq!(text(&s), "α "); + exec(&s, "pmacs.window.buffer():undo()"); + assert_eq!(text(&s), "α", "the first undo removes the separate space"); + exec(&s, "pmacs.window.buffer():undo()"); + assert_eq!(text(&s), "\\alpha", "the second undoes the expansion"); +} + +#[test] +fn to_is_not_eager_because_longer_keys_extend_it() { + // The criterion rev 8 got wrong: `to` looks unique and is not. + // `top`, `to0`, `toa` and others extend it, so it needs a + // terminator. Bites against an eager rule that tests only "is this + // a key" without asking whether anything extends it. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\to"); + assert_eq!(text(&s), "\\to", "no expansion without a terminator"); + + type_str(&mut s, " "); + assert_eq!(text(&s), "→ ", "the finish path then resolves it"); +} + +// --------------------------------------------------------------------------- +// 39 — $CURSOR +// --------------------------------------------------------------------------- + +#[test] +fn the_cursor_placeholder_places_the_point_between_the_symbols() { + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\<>"); + assert_eq!(text(&s), "⟨⟩"); + // The placeholder is a point position, not a literal: typing lands + // between the brackets. + type_str(&mut s, "x"); + assert_eq!(text(&s), "⟨x⟩", "$CURSOR left the point inside"); +} + +// --------------------------------------------------------------------------- +// 40 — the pair collision +// --------------------------------------------------------------------------- + +#[test] +fn a_pending_abbreviation_is_never_corrupted_by_auto_pairing() { + // 64 keys contain a `lean4` pair-set character. Two DISTINCT bugs + // produce the same symptom here, so both are asserted: pairing + // running first, and a consumer that claims only completed + // expansions (which would hand each intermediate `[` to pairing). + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\["); + assert_eq!( + text(&s), + "\\[", + "the intermediate `[` was CLAIMED — pairing inserted no `]`, \ + which is what keeps `\\[[]]` reachable" + ); + + type_str(&mut s, "[]]"); + assert_eq!(text(&s), "⟦⟧", "the full key resolves"); +} + +#[test] +fn a_pair_character_that_terminates_an_abbreviation_still_pairs() { + // The other half of the collision, and the one the first revision + // of this file got wrong. `(` does not extend `alp`, so it + // TERMINATES — and a terminator is an ordinary character that + // pairing is entitled to react to. + // + // Claiming the terminator suppresses pairing entirely (`α(`). + // Expanding before declining is no better: the replace makes + // pairing's copy of the record stale, so pairing declines and the + // closer is silently lost. Only deferring the expansion past the + // chain gives both. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp("); + assert_eq!( + text(&s), + "α()", + "the abbreviation expanded AND the terminator paired" + ); + assert_eq!( + cursor(&s), + 3, + "and the point sits between the pair — after α (2 bytes) and \ + the opener" + ); +} + +#[test] +fn a_nested_fan_out_between_the_expander_and_pairing_does_not_expand_early() { + // `buffer.after-edit` fan-outs NEST — the typed-edit contract + // explicitly supports a consumer calling `pmacs.hook.run`, and a + // nested run re-enters every subscriber, including the deferred + // expansion's. If the nested pass performed the expansion, the + // OUTER chain would then resume and hand pairing a record the + // replace had already invalidated: `α(` again, reached through the + // chain's documented re-entrancy seam rather than through claiming. + let (mut s, _f) = lean_editor(); + exec( + &s, + r#" + _G.NESTED = 0 + pmacs.typed_edit.add_consumer { + name = "nested-fan-out", + priority = 75, -- between the expander (50) and pairing (100) + fn = function() + if _G.NESTED == 0 then + _G.NESTED = 1 + pmacs.hook.run("buffer.after-edit") + end + return false + end, + } + "#, + ); + + type_str(&mut s, "\\alp("); + let nested: i64 = eval(&s, "return _G.NESTED"); + assert_eq!(nested, 1, "the nested fan-out must actually have run"); + assert_eq!( + text(&s), + "α()", + "the expansion waited for the OUTERMOST pass, so pairing still \ + held a valid record when the terminator reached it" + ); +} + +#[test] +fn a_nested_fan_out_that_never_reaches_the_expander_still_does_not_expand_early() { + // The chain's OTHER exit: a consumer may CLAIM and stop the chain + // before the expander is reached, while the fan-out's + // deferred-expansion subscriber still runs. Counting in the + // expander itself therefore misses that pass — it would look like + // the outermost one and expand early, and outer pairing would + // resume with an invalidated record. + // + // The sequence, exactly: a consumer at 25 declines on the outer + // pass (there is a record) and claims on the nested one (there is + // not); a consumer at 75 runs one nested fan-out from between the + // expander and pairing. + let (mut s, _f) = lean_editor(); + exec( + &s, + r#" + _G.NESTED, _G.CLAIMED = 0, 0 + pmacs.typed_edit.add_consumer { + name = "claims-only-when-recordless", + priority = 25, -- ahead of the expander at 50 + fn = function(rec) + if rec == nil then + _G.CLAIMED = _G.CLAIMED + 1 + return true -- stops the chain: the expander never runs + end + return false + end, + } + pmacs.typed_edit.add_consumer { + name = "nested-fan-out", + priority = 75, -- between the expander (50) and pairing (100) + fn = function() + if _G.NESTED == 0 then + _G.NESTED = 1 + pmacs.hook.run("buffer.after-edit") + end + return false + end, + } + "#, + ); + + type_str(&mut s, "\\alp("); + let (nested, claimed): (i64, i64) = eval(&s, "return _G.NESTED, _G.CLAIMED"); + assert_eq!(nested, 1, "the nested fan-out must actually have run"); + assert!( + claimed >= 1, + "the nested pass must actually have been short-circuited before \ + the expander, or this pins the same thing as 45n" + ); + assert_eq!( + text(&s), + "α()", + "the nesting count comes from a point that runs before any \ + consumer can claim, so the nested pass was still recognised" + ); +} + +#[test] +fn a_pair_character_outside_a_pending_abbreviation_still_pairs() { + // The other direction: claiming extensions must not disable pairing + // in Lean buffers generally. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "["); + assert_eq!(text(&s), "[]", "ordinary auto-pairing is untouched"); +} + +// --------------------------------------------------------------------------- +// 42 — a prefix that opens nothing +// --------------------------------------------------------------------------- + +#[test] +fn a_prefix_that_opens_no_key_is_left_literal_with_no_edit() { + // `W` is one of exactly six printable characters that begin no key + // (`$ % , ; @ W`). Rev 8 used `\zzzz`, which expands — `ze`, `zeta` + // and `zsqrtd` exist (round 9). + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\WWWW "); + assert_eq!(text(&s), "\\WWWW ", "literal text, no expansion"); +} + +#[test] +fn a_prefix_with_no_complete_match_still_expands_its_best_prefix() { + // The case rev 8 mistook for "no match": `z` DOES open a pending + // abbreviation, and the second `z` finishes it. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\zzzz "); + assert_eq!(text(&s), "ζzzz ", "`z` resolved through `ze`"); +} + +// --------------------------------------------------------------------------- +// 43 — lazy abandonment +// --------------------------------------------------------------------------- + +#[test] +fn moving_the_point_away_abandons_the_pending_abbreviation() { + // There is no cursor-motion hook, so the pending record is + // validated at the NEXT typed edit: the point must still be at the + // end of the pending span. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp"); + exec(&s, "pmacs.editor.goto_byte(0)"); + type_str(&mut s, "h"); + assert_eq!(text(&s), "h\\alp", "the `h` landed as plain text"); + + // The keystroke that makes abandonment OBSERVABLE. Asserting only + // the line above proves nothing: claiming an extension makes no + // edit, so a record that wrongly survived would look identical + // here. If `h` had extended the record to `alph`, this `a` + // completes `alpha` and eagerly expands — over a span whose offsets + // are now stale by one. + type_str(&mut s, "a"); + assert_eq!( + text(&s), + "ha\\alp", + "`\\alp` is still literal: the record was dropped when the \ + point left the end of its span, not carried along" + ); +} + +#[test] +fn switching_buffers_clears_pending_state_eagerly() { + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("b.lean"); + std::fs::write(&other, "").unwrap(); + let od = other.display().to_string(); + let fd = f.display().to_string(); + + // Open the second buffer FIRST, then come back. `find_or_open` + // fires `buffer.after-switch` only on the already-open branch — a + // fresh load fires `buffer.after-load` instead, and its own insert + // fires a record-less `buffer.after-edit`. Without this warm-up the + // test passes through the nil-record path and pins nothing about + // switching: deleting the after-switch subscriber leaves it green. + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + + type_str(&mut s, "\\alph"); + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + + type_str(&mut s, "a"); + assert_eq!( + text(&s), + "\\alpha", + "without the switch this would have eagerly expanded to α; \ + `buffer.after-switch` cleared the record" + ); +} + +#[test] +fn a_self_insert_that_moves_the_point_afterwards_does_not_expand() { + // Buffer and window matching is not enough. A redefined + // `buffer.self-insert` may insert the completing character and THEN + // move the point; expanding over a span the user has left teleports + // them back into it. Pairing makes the same three-part check + // (`ed.cursor() ~= rec.post_cursor`) for the same reason. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alph"); + exec( + &s, + r#" + pmacs.command.unregister("buffer.self-insert") + pmacs.command.define { + name = "buffer.self-insert", + description = "test override: insert, then move the point away", + fn = function(cp) + pmacs.editor.insert_char_over_region(cp) + pmacs.editor.goto_byte(0) + end, + } + "#, + ); + + type_str(&mut s, "a"); + assert_eq!( + text(&s), + "\\alpha", + "the record died with the point that left it — no expansion" + ); + assert_eq!(cursor(&s), 0, "and the point stayed where it was moved to"); +} + +#[test] +fn an_intercept_that_switches_buffers_does_not_move_the_other_points() { + // A buffer intercept may switch window or buffer while the replace + // runs. An unguarded `goto_byte` afterwards moves the point of + // whatever it switched TO — a buffer with nothing to do with this + // expansion. Pairing's `repair_cursor` guards the same way. + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("other.lean"); + std::fs::write(&other, "0123456789").unwrap(); + let od = other.display().to_string(); + let fd = f.display().to_string(); + + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + exec( + &s, + &format!( + r#" + _G.SWITCHED = false + pmacs.buffer.add_intercept(pmacs.window.buffer(), function(op) + if op.kind == "replace" and not _G.SWITCHED then + _G.SWITCHED = true + pmacs.buffer.find_or_open({od:?}) + end + return nil + end) + "# + ), + ); + + type_str(&mut s, "\\alpha"); + let switched: bool = eval(&s, "return _G.SWITCHED"); + assert!(switched, "the intercept must actually have fired"); + assert_eq!( + text(&s), + "0123456789", + "we are now in the buffer the intercept switched to" + ); + // Whatever point the switch left in that buffer, the expansion must + // not have moved it. Unguarded, `goto_byte` runs against the + // ambient buffer and translates the LEAN buffer's pre-edit point + // (6) through the LEAN buffer's replace, landing at 2 here — a + // number with no meaning in this buffer at all. + assert_eq!( + cursor(&s), + 0, + "its point is untouched — the expansion's cursor placement is \ + guarded on the window and buffer still being the ones it \ + edited" + ); +} + +// --------------------------------------------------------------------------- +// 44 / 45 — the setting and the language gate, both on the SOURCE buffer +// --------------------------------------------------------------------------- + +#[test] +fn disabling_the_setting_stops_expansion() { + let (mut s, _f) = lean_editor(); + exec(&s, "pmacs.config.set('lean.abbrev', false)"); + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "\\alpha", "no expansion when disabled"); + + exec(&s, "pmacs.config.set('lean.abbrev', true)"); + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, " \\alpha"); + assert_eq!(text(&s), "\\alpha α", "and it comes back live"); +} + +#[test] +fn the_setting_is_read_against_the_typed_edits_source_buffer() { + // A buffer-local override must not follow the user to another + // buffer of the same language — the `editing.auto-pair` precedent, + // including its round-2 correction to resolve `rec.buffer` rather + // than `pmacs.window.buffer()`. + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("b.lean"); + std::fs::write(&other, "").unwrap(); + + exec( + &s, + "pmacs.config.set_local(pmacs.window.buffer(), 'lean.abbrev', false)", + ); + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "\\alpha", "disabled in THIS buffer"); + + let od = other.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "α", "a second lean buffer is unaffected"); + + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + assert_eq!(text(&s), "\\alpha", "and the first is still disabled"); +} + +#[test] +fn no_abbreviation_state_is_opened_outside_a_lean_buffer() { + let dir = fresh_dir(); + let f = dir.join("a.rs"); + std::fs::write(&f, "").unwrap(); + let s = EditorState::new(); + exec(&s, "pmacs.lsp.config = {}"); + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + let mut s = s; + + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "\\alpha", "no expansion in Rust"); + + // And the leader opened nothing, so `[` still pairs normally. + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "\\["); + assert_eq!( + text(&s), + "\\alpha\\[]", + "`\\[` in a Rust buffer pairs — the input method never armed" + ); +} + +// --------------------------------------------------------------------------- +// 45a / 45b / 45c / 45d / 45e — resolution rules +// --------------------------------------------------------------------------- + +#[test] +fn the_shortest_key_wins_not_the_longest() { + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp "); + assert_eq!(text(&s), "α ", "`alp` resolves through `alpha`"); + + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "\\al "); + assert_eq!( + text(&s), + "α ∀ ", + "`al` resolves through `all` (3) — NOT `alpha` (5). A \ + longest-match or unique-match-only rule passes the first \ + assertion and fails this one" + ); +} + +#[test] +fn an_unmatchable_tail_is_appended_not_dropped() { + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp7 "); + assert_eq!( + text(&s), + "α7 ", + "`7` finished `alp`; it is kept, not swallowed, and the whole \ + abbreviation is not abandoned" + ); +} + +#[test] +fn there_is_no_terminator_list() { + // `'+ '` is a key — a trailing SPACE is part of it. Bites against + // any hardcoded space/tab/RET terminator set. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\+ "); + assert_eq!(text(&s), "⊹", "the space EXTENDED rather than terminating"); +} + +#[test] +fn a_doubled_backslash_yields_one_literal_backslash() { + // Not a terminator case: the pending text is empty, `\` is itself a + // key, and it extends-and-eagerly-matches. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\\\"); + assert_eq!(text(&s), "\\", "one literal backslash"); + + // ...and no pending state was left open, so an ordinary letter is + // an ordinary letter. + type_str(&mut s, "n"); + assert_eq!(text(&s), "\\n", "two characters, not a newline"); +} + +#[test] +fn a_terminating_backslash_re_arms_as_a_new_leader() { + // `al` is NOT eager, so its pending record is still open when the + // second `\` arrives: the `\` terminates it, the expansion runs, + // and the same `\` must then open a fresh abbreviation. + // + // The framing's own example — `\alpha\to` — does NOT exercise this + // branch: `alpha` is eager, so the record is already closed and the + // `\` is handled by the ordinary open-a-leader path. It passes with + // the re-arm branch deleted, which is why the non-eager case is the + // one asserted first. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\al\\to "); + assert_eq!( + text(&s), + "∀→ ", + "the terminating `\\` expanded `al` AND opened a new \ + abbreviation at its own position" + ); + + // The criterion's example still holds, by the other route. + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "\\alpha\\to "); + assert_eq!(text(&s), "∀→ α→ "); +} + +#[test] +fn an_inserted_backslash_does_not_re_arm() { + // `setminus` expands to a literal `\`. That backslash is a + // programmatic replace, which arms no typed-edit record — so it + // opens no pending abbreviation. Bites against a future consumer + // that infers pending state from buffer text instead of provenance. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\setminus"); + assert_eq!(text(&s), "\\", "expanded to a literal backslash"); + + type_str(&mut s, "n"); + assert_eq!( + text(&s), + "\\n", + "the letter after it is a plain letter — the INSERTED backslash \ + armed nothing" + ); +} + +// --------------------------------------------------------------------------- +// 45h — the tie-break by source declaration order +// --------------------------------------------------------------------------- + +#[test] +fn equal_length_candidates_break_by_source_declaration_order() { + // `f<` and `f>` are both length 2. `f<` is declared first, so `\f` + // resolves to `‹`. This is the criterion that bites a map-shaped + // vendored table: with `pairs` iteration it passes or fails by hash + // order. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\f "); + assert_eq!(text(&s), "‹ ", "`f<` wins over `f>` by source order"); + + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "\\\" "); + assert_eq!( + text(&s), + "‹ Ä ", + "`\"A` is the first of eleven equal-length candidates" + ); +} + +#[test] +fn reversing_the_vendored_sequence_reverses_the_tie() { + // The falsification 45h requires: run the same resolution against a + // deliberately reversed sequence and show it changes. If this did + // NOT change, the tie-break would not be reading source order at + // all and the assertion above would be passing by luck. + let (s, _f) = lean_editor(); + let forward: String = eval(&s, "return pmacs.lean_input._resolve('f')"); + assert_eq!(forward, "‹"); + + let reversed: String = eval( + &s, + " + local seq = pmacs.lean_abbrev + local rev = {} + for i = #seq, 1, -1 do rev[#rev + 1] = seq[i] end + -- Resolve `f` the way the module does, over the reversed order. + local best = nil + for i = 1, #rev do + local k, v = rev[i][1], rev[i][2] + if k:sub(1, 1) == 'f' then + if best == nil or #k < best.len then best = { sym = v, len = #k } end + end + end + return best.sym + ", + ); + assert_eq!( + reversed, "›", + "reversed source order picks `f>` — the tie really is decided \ + by position in the sequence" + ); +} + +// --------------------------------------------------------------------------- +// 45g — table integrity, limited to what the suite can actually check +// --------------------------------------------------------------------------- + +#[test] +fn the_vendored_table_is_self_consistent() { + // `abbreviations.json` is not shipped, so the suite cannot diff + // against it; the full source-fidelity check belongs to the + // generator, which re-parses its own output from disk. What is + // checkable here are the properties a corrupt emit breaks. + let (s, _f) = lean_editor(); + + let count: i64 = eval(&s, "return #pmacs.lean_abbrev"); + assert_eq!( + count, 1855, + "the declared entry count for the recorded upstream commit" + ); + + let (unique, cursor_ok, utf8_ok): (i64, bool, bool) = eval( + &s, + r#" + local seen, n = {}, 0 + local cursor_ok, utf8_ok = true, true + for i = 1, #pmacs.lean_abbrev do + local k, v = pmacs.lean_abbrev[i][1], pmacs.lean_abbrev[i][2] + if not seen[k] then seen[k] = true; n = n + 1 end + local _, c = v:gsub("%$CURSOR", "") + if c > 1 then cursor_ok = false end + -- A Lua pattern cannot validate UTF-8; check the shape the + -- emitter guarantees instead: no lone continuation byte at the + -- start of a sequence and no truncated tail. + if k:find("[\128-\191]") == 1 then utf8_ok = false end + end + return n, cursor_ok, utf8_ok + "#, + ); + assert_eq!( + unique, 1855, + "every key is unique — a collision would silently drop entries \ + from the derived lookup" + ); + assert!(cursor_ok, "no symbol carries more than one $CURSOR"); + assert!(utf8_ok, "no key begins with a continuation byte"); + + // The resolution spot-set named by 45g. + for (input, want) in [ + ("alpha", "α"), + ("to", "→"), + ("<>", "⟨$CURSOR⟩"), + ("+ ", "⊹"), + ("\\\\", "\\"), + ("n", "\\n"), + ("setminus", "\\"), + ("f", "‹"), + ] { + let got: String = eval(&s, &format!("return pmacs.lean_input._resolve('{input}')")); + assert_eq!(got, want, "resolution of {input:?}"); + } + + // The eager set is the one the state machine branches on. + let alpha_eager: bool = eval(&s, "return pmacs.lean_input._is_eager('alpha')"); + let to_eager: bool = eval(&s, "return pmacs.lean_input._is_eager('to')"); + assert!(alpha_eager, "`alpha` has no extension"); + assert!(!to_eager, "`to` is extended by `top`, `to0`, `toa`, …"); +} + +// --------------------------------------------------------------------------- +// Q#AP7 for the deferred expansion: it must land before lsp.lua flushes +// --------------------------------------------------------------------------- + +#[test] +fn the_expansion_reaches_the_first_did_change() { + // The expansion runs on its OWN `buffer.after-edit` subscriber, + // after the typed-edit chain. That makes it a new instance of the + // Q#AP7 obligation pairing already carries: lsp.lua's subscriber + // flushes `didChange` SYNCHRONOUSLY on the signature-trigger path, + // and `(` is a trigger. A server told about `\alp(` instead of + // `α()` stays wrong until the next edit — diagnostics, semantic + // tokens and inlay hints all frozen at stale byte positions. + // + // Falsified by loading lean_input.lua after lsp.lua in + // `src/editor.rs`: the expansion would then arrive in the SECOND + // didChange, or not at all. + let dir = fresh_dir(); + let sink = dir.join("changes.jsonl"); + let sink_disp = sink.display().to_string(); + let fake = env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned(); + + let f = dir.join("a.lean"); + std::fs::write(&f, "").unwrap(); + let mut s = EditorState::new(); + s.lua_host.lua().remove_app_data::(); + s.lua_host.lua().set_app_data(StateDir(dir.clone())); + exec(&s, "pmacs.lsp.config = {}"); + exec( + &s, + &format!( + "pmacs.lsp.config.lean4 = {{ + command = '{fake}', + env = {{ + PMACS_FAKE_LSP_MODE = 'sighelp', + PMACS_FAKE_LSP_CHANGE_SINK = '{sink_disp}', + }}, + }}" + ), + ); + + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + let initialized = "(function() \ + for _,r in ipairs(pmacs.lsp.list()) do \ + if r.state and r.state.kind=='initialized' then return true end \ + end \ + return false \ + end)()"; + assert!(pump_lua_flag(&mut s, initialized, 5), "fake server init"); + + type_str(&mut s, "\\alp("); + assert_eq!(text(&s), "α()", "precondition: the expansion happened"); + + // Wait for the flush that carries the `(` keystroke. Earlier + // keystrokes have already produced their own didChanges, so + // `changes[0]` is NOT the one under test — asserting on it compares + // against `\al` and fails for the wrong reason. + let deadline = Instant::now() + Duration::from_secs(5); + let changes = loop { + s.tick_processes(); + s.tick_lsp(); + s.tick_async(); + let c = did_change_texts(&sink); + if c.iter().any(|t| t.contains('α')) { + break c; + } + assert!( + Instant::now() < deadline, + "no didChange carrying the expansion reached the fake server; got {:?}", + did_change_texts(&sink) + ); + std::thread::sleep(Duration::from_millis(10)); + }; + assert!( + !changes.iter().any(|t| t == "\\alp("), + "no didChange may ever carry the UNEXPANDED text — one would mean lsp.lua flushed before the deferred expansion ran (Q#AP7). Got {changes:?}" + ); + assert_eq!( + changes.last().map(String::as_str), + Some("α()"), + "the flush that carries the terminator carries the expansion and pairing's closer with it" + ); +} + +fn pump_lua_flag(state: &mut EditorState, flag: &str, secs: u64) -> bool { + let deadline = Instant::now() + Duration::from_secs(secs); + loop { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + let done: bool = state + .lua_host + .lua() + .load(format!("return ({flag}) == true")) + .eval() + .unwrap_or(false); + if done { + return true; + } + if Instant::now() >= deadline { + return false; + } + std::thread::sleep(Duration::from_millis(10)); + } +} + +/// The `text` of every `textDocument/didChange` line in the sink, in +/// arrival order. +fn did_change_texts(sink: &std::path::Path) -> Vec { + let Ok(raw) = std::fs::read_to_string(sink) else { + return Vec::new(); + }; + raw.lines() + .filter_map(|l| serde_json::from_str::(l).ok()) + .filter(|v| v.get("method").and_then(|m| m.as_str()) == Some("textDocument/didChange")) + .filter_map(|v| v.get("text").and_then(|t| t.as_str()).map(str::to_owned)) + .collect() +} + +// --------------------------------------------------------------------------- +// 45i — pending state is per frontend +// --------------------------------------------------------------------------- + +/// Register a second frontend on the SAME buffer, with its own window. +fn attach_frontend(s: &EditorState, fid: FrontendId) -> WindowId { + let mut core = s.core.borrow_mut(); + let buffer_id = core.active_buffer_id(); + let text_view = { + let registry = core.registry.clone(); + let reg = registry.borrow(); + pmacs::text_view::TextView::new(reg.get(buffer_id).unwrap()) + }; + let win_id = WindowId::next(); + core.windows + .insert(win_id, Window::new(win_id, buffer_id, text_view)); + core.register_frontend_view( + fid, + FrontendView { + layout: Layout::single(win_id), + active: win_id, + fold_projection: true, + panel_capable: true, + frame_geometry: None, + panel_hidden: false, + }, + ); + win_id +} + +const B: FrontendId = FrontendId(9); + +#[test] +fn a_peer_edit_to_the_shared_buffer_abandons_the_pending_record() { + let (mut s, _f) = lean_editor(); + let b_win = attach_frontend(&s, B); + // B sits at the start of the buffer; A types at the end. + s.core.borrow_mut().windows.get_mut(&b_win).unwrap().cursor = 0; + + type_as(&mut s, FrontendId::LOCAL, "\\al"); + type_as(&mut s, B, "p"); + assert!( + text(&s).contains('p'), + "B's keystroke landed as ordinary text rather than extending \ + A's abbreviation, got {:?}", + text(&s) + ); + + type_as(&mut s, FrontendId::LOCAL, "l "); + assert!( + !text(&s).contains('∀'), + "A's record was abandoned: `revision()` is buffer-global, so \ + B's edit invalidates it even though B edited elsewhere. Got {:?}", + text(&s) + ); +} + +#[test] +fn a_peer_buffer_switch_does_not_clear_another_frontends_record() { + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("b.lean"); + std::fs::write(&other, "").unwrap(); + let od = other.display().to_string(); + let fd = f.display().to_string(); + // Warm up both buffers so B's switch takes `find_or_open`'s + // already-open branch, which is the only one that fires + // `buffer.after-switch`. A fresh load fires `buffer.after-load` + // and a record-less edit instead — and that path clears pending + // state for a different reason, which would make this test green + // no matter whose entries the subscriber clears. + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + attach_frontend(&s, B); + + type_as(&mut s, FrontendId::LOCAL, "\\al"); + + // B switches buffers WITHOUT editing the shared buffer. + // Only B moves: the switch is scoped to B's own window, so A's + // window still shows the shared buffer with A's point where it was. + s.core.borrow_mut().active_frontend = B; + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + s.core.borrow_mut().active_frontend = FrontendId::LOCAL; + + type_as(&mut s, FrontendId::LOCAL, "l "); + assert_eq!( + text(&s), + "∀ ", + "`buffer.after-switch` clears only the ACTING frontend's \ + entries — a blanket clear would discard A's half-typed \ + abbreviation" + ); +} + +#[test] +fn detaching_a_frontend_purges_only_its_own_pending_state() { + let (mut s, _f) = lean_editor(); + attach_frontend(&s, B); + + type_as(&mut s, FrontendId::LOCAL, "\\al"); + exec(&s, &format!("pmacs.hook.run('frontend.detached', {})", B.0)); + + type_as(&mut s, FrontendId::LOCAL, "l "); + assert_eq!( + text(&s), + "∀ ", + "B's detachment purged B's entries and left A's record valid" + ); +}