diff --git a/Idris2 b/Idris2 index dc1b538..ea093ff 160000 --- a/Idris2 +++ b/Idris2 @@ -1 +1 @@ -Subproject commit dc1b5387b8d54132a6707c4c62d7777748271db4 +Subproject commit ea093ffaed7b003d28e35cb3b1114ac4bce4603d diff --git a/src/Language/LSP/BrowseNamespace.idr b/src/Language/LSP/BrowseNamespace.idr index 2d9563d..e610e4c 100644 --- 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 index 6e4227e..725a5e1 100644 --- 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