From e641ae4eae75d5a1029168adaf063b3979244d46 Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Fri, 26 Nov 2021 10:31:01 +0100
Subject: [PATCH] fix: prefix check in set_option completion

---
 src/Lean/Server/Completion.lean               | 11 ++-
 tests/lean/interactive/completionOption.lean  | 21 ++++-
 .../completionOption.lean.expected.out        | 86 +++++++++++++++++--
 3 files changed, 106 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index ac8f2e298c..7e0e274194 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -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.
diff --git a/tests/lean/interactive/completionOption.lean b/tests/lean/interactive/completionOption.lean
index 027619ef2d..0bf565314b 100644
--- a/tests/lean/interactive/completionOption.lean
+++ b/tests/lean/interactive/completionOption.lean
@@ -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
diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out
index 83e601bd1d..30248e5625 100644
--- a/tests/lean/interactive/completionOption.lean.expected.out
+++ b/tests/lean/interactive/completionOption.lean.expected.out
@@ -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}