[ upstream ] Add WithDefault handling to visibility (#207)

idris-community · Oct 25, 2023 · 526902b · 526902b
1 parent 7fa662a
commit 526902b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/Idris2 b/Idris2
diff --git a/src/Language/LSP/BrowseNamespace.idr b/src/Language/LSP/BrowseNamespace.idr
@@ -13,6 +13,7 @@ import Idris.Syntax
 import Language.LSP.Definition
 import Language.LSP.Message
 import Libraries.Data.NameMap
+import Libraries.Data.WithDefault
 import Parser.Source
 import Parser.Rule.Source
 import Server.Configuration
@@ -23,7 +24,7 @@ visible : Defs -> Name -> Core Bool
 visible defs n = do 
   Just def <- lookupCtxtExact n (gamma defs)
     | Nothing => pure False
-  pure $ visibility def /= Private
+  pure $ collapseDefault (visibility def) /= Private
 
 inNS : Namespace -> Name -> Bool
 inNS ns (NS xns (UN _)) = ns `isParentOf` xns

diff --git a/src/Language/LSP/Completion/Handler.idr b/src/Language/LSP/Completion/Handler.idr
@@ -20,6 +20,7 @@ import Language.LSP.Utils
 import Language.LSP.VirtualDocument
 import Libraries.Data.NameMap
 import Libraries.Data.UserNameMap
+import Libraries.Data.WithDefault
 import Server.Configuration
 import Server.Log
 import Server.Utils
@@ -110,7 +111,7 @@ completionNames = do
         case mdef of
           Nothing => pure Nothing
           Just def =>
-            let visible = (ns == currentNS defs) || (visibility def /= Private) in
+            let visible = (ns == currentNS defs) || (collapseDefault (visibility def) /= Private) in
             if visible
               then do
                 ty <- prettyType (const ()) def.type