fix: hide internal namespaces from autocompletion

closes #993

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 =>

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

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}