From 420f5bb315f7cf9b8ef628c0aea0049b43ae2402 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Feb 2022 13:33:27 -0800
Subject: [PATCH] fix: hide internal namespaces from autocompletion

closes #993
---
 src/Lean/Server/Completion.lean                       |  2 +-
 tests/lean/interactive/internalNamesIssue.lean        | 11 +++++++++++
 .../interactive/internalNamesIssue.lean.expected.out  |  6 ++++++
 3 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/interactive/internalNamesIssue.lean
 create mode 100644 tests/lean/interactive/internalNamesIssue.lean.expected.out

diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index fc23abef4d..2ef3e3fbba 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -206,7 +206,7 @@ def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M
     else
       addNamespaceCompletionItem (ns.replacePrefix ns' Name.anonymous)
   env.getNamespaceSet |>.forM fun ns => do
-    unless env.contains ns do -- Ignore namespaces that are also declaration names
+    unless ns.isInternal || env.contains ns do -- Ignore internal and namespaces that are also declaration names
       for openDecl in ctx.openDecls do
         match openDecl with
         | OpenDecl.simple ns' except =>
diff --git a/tests/lean/interactive/internalNamesIssue.lean b/tests/lean/interactive/internalNamesIssue.lean
new file mode 100644
index 0000000000..c5017978c9
--- /dev/null
+++ b/tests/lean/interactive/internalNamesIssue.lean
@@ -0,0 +1,11 @@
+namespace Foo
+
+def foo (x : Nat) := x + x + x
+
+def bla (x : Nat) : Nat :=
+  if x > foo (10 + 10) then 1 else x * x * x
+
+end Foo
+
+#check Foo.
+         --^ textDocument/completion
diff --git a/tests/lean/interactive/internalNamesIssue.lean.expected.out b/tests/lean/interactive/internalNamesIssue.lean.expected.out
new file mode 100644
index 0000000000..2a72302a74
--- /dev/null
+++ b/tests/lean/interactive/internalNamesIssue.lean.expected.out
@@ -0,0 +1,6 @@
+{"textDocument": {"uri": "file://internalNamesIssue.lean"},
+ "position": {"line": 9, "character": 11}}
+{"items":
+ [{"label": "bla", "kind": 3, "detail": "Nat → Nat"},
+  {"label": "foo", "kind": 3, "detail": "Nat → Nat"}],
+ "isIncomplete": true}