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

fix: prefix check in set_option completion

Browse source
This commit is contained in:
larsk21 2021-11-26 10:31:01 +01:00 • committed by Sebastian Ullrich
parent 3ccd44fafa
commit e641ae4eae
3 changed files with 106 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Server/Completion.lean
View file

@ -252,15 +252,18 @@ private def optionCompletion (ctx : ContextInfo) (stx : Syntax) : IO (Option Com
let opts ← getOptions
let mut items := #[]
for ⟨name, decl⟩ in decls do
if partialName.isPrefixOf name ||
(match partialName, name with
| Name.str p₁ s₁ _, Name.str p₂ s₂ _ => p₁ == p₂ && s₁.isPrefixOf s₂
| _, _ => false) then
if isPrefixOf partialName name then
items := items.push
{ label := name.toString
detail? := s!"({opts.get name decl.defValue}), {decl.descr}"
documentation? := none }
return some { items := sortCompletionItems items, isIncomplete := true }
where
isPrefixOf (pref? : Name) (name : Name) : Bool :=
match pref?, name with
| Name.anonymous, _ => true
| p@(Name.str pn ps _), Name.str n s _ => if pn == n then ps.isPrefixOf s else isPrefixOf p n
| _, _ => false
private def tacticCompletion (ctx : ContextInfo) : IO (Option CompletionList) :=
-- Just return the list of tactics for now.

21
tests/lean/interactive/completionOption.lean
View file

@ -1,2 +1,21 @@
set_option pp.proofs
set_option fo
--^ textDocument/completion
set_option format
--^ textDocument/completion
set_option format.in
--^ textDocument/completion
set_option trace.p
--^ textDocument/completion
set_option trace.pp
--^ textDocument/completion
set_option trace.pp.ana
--^ textDocument/completion
set_option trace.pp.analyze
--^ textDocument/completion

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

@ -1,10 +1,82 @@
{"textDocument": {"uri": "file://completionOption.lean"},
"position": {"line": 0, "character": 20}}
"position": {"line": 1, "character": 13}}
{"items":
[{"label": "pp.proofs",
"detail":
"(false), (pretty printer) if set to false, replace proofs appearing as an argument to a function with a placeholder"},
{"label": "pp.proofs.withType",
"detail":
"(true), (pretty printer) when eliding a proof (see `pp.proofs`), show its type instead"}],
[{"label": "format.indent", "detail": "(2), indentation"},
{"label": "format.unicode", "detail": "(true), unicode characters"},
{"label": "format.width", "detail": "(120), indentation"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completionOption.lean"},
"position": {"line": 4, "character": 17}}
{"items":
[{"label": "format.indent", "detail": "(2), indentation"},
{"label": "format.unicode", "detail": "(true), unicode characters"},
{"label": "format.width", "detail": "(120), indentation"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completionOption.lean"},
"position": {"line": 7, "character": 20}}
{"items": [{"label": "format.indent", "detail": "(2), indentation"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completionOption.lean"},
"position": {"line": 10, "character": 18}}
{"items":
[{"label": "trace.pp.analyze",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.annotate",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.error",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.tryUnify",
"detail":
"(false), enable/disable tracing for the given module and submodules"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completionOption.lean"},
"position": {"line": 13, "character": 19}}
{"items":
[{"label": "trace.pp.analyze",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.annotate",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.error",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.tryUnify",
"detail":
"(false), enable/disable tracing for the given module and submodules"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completionOption.lean"},
"position": {"line": 16, "character": 23}}
{"items":
[{"label": "trace.pp.analyze",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.annotate",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.error",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.tryUnify",
"detail":
"(false), enable/disable tracing for the given module and submodules"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completionOption.lean"},
"position": {"line": 19, "character": 27}}
{"items":
[{"label": "trace.pp.analyze",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.annotate",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.error",
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"label": "trace.pp.analyze.tryUnify",
"detail":
"(false), enable/disable tracing for the given module and submodules"}],
"isIncomplete": true}