max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: pre-filter completion items mod ascii casing (#11140)

Browse source 
This PR ensures that we pre-filter auto-completion items modulo ASCII
casing for consistency with the VS Code fuzzy matching.
This commit is contained in:
Marc Huisinga 2025-11-11 15:11:05 +01:00 • committed by GitHub
parent aaceb3dbf5
commit c2647cdbf5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 26 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/Completion/CompletionUtils.lean
View file

@ -22,7 +22,7 @@ where
let ac := aPos.get' a ha
let bc := bPos.get' b hb
let bPos := bPos.next' b hb
if ac == bc then
if ac.toLower == bc.toLower then
let aPos := aPos.next' a ha
go aPos bPos
else

25
tests/lean/interactive/completionOption.lean.expected.out
View file

@ -273,6 +273,19 @@ Resolution of format.indent:
"detail":
"(false), enable/disable tracing for the given module and submodules",
"data": ["«external:file:///completionOption.lean»", 7, 23, 0]},
{"textEdit":
{"replace":
{"start": {"line": 7, "character": 11},
"end": {"line": 7, "character": 23}},
"newText": "trace.PrettyPrinter.parenthesize.backtrack",
"insert":
{"start": {"line": 7, "character": 11},
"end": {"line": 7, "character": 23}}},
"label": "trace.PrettyPrinter.parenthesize.backtrack",
"kind": 10,
"detail":
"(false), enable/disable tracing for the given module and submodules",
"data": ["«external:file:///completionOption.lean»", 7, 23, 0]},
{"textEdit":
{"replace":
{"start": {"line": 7, "character": 11},
@ -337,6 +350,18 @@ Resolution of trace.pp.analyze.error:
"detail":
"(false), enable/disable tracing for the given module and submodules",
"data": ["«external:file:///completionOption.lean»", 7, 23, 0]}
Resolution of trace.PrettyPrinter.parenthesize.backtrack:
{"textEdit":
{"replace":
{"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 23}},
"newText": "trace.PrettyPrinter.parenthesize.backtrack",
"insert":
{"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 23}}},
"label": "trace.PrettyPrinter.parenthesize.backtrack",
"kind": 10,
"detail":
"(false), enable/disable tracing for the given module and submodules",
"data": ["«external:file:///completionOption.lean»", 7, 23, 0]}
Resolution of trace.pp.analyze:
{"textEdit":
{"replace":