@@ -3,6 +3,7 @@ module Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler) where
33import qualified Agda.Syntax.Abstract as A
44import Agda.Syntax.Common.Pretty (prettyShow )
55import Agda.Utils.Maybe (fromMaybe , mapMaybe )
6+ import Agda.Utils.Monad (forMaybeM )
67import Control.Monad (forM )
78import Control.Monad.Trans (lift )
89import Data.Map (Map )
@@ -15,33 +16,62 @@ import Monad (ServerM)
1516import Server.Model.AgdaFile (AgdaFile , agdaFileSymbols , defNameRange , symbolByName , symbolsByParent )
1617import Server.Model.Handler (requestHandlerWithAgdaFile )
1718import Server.Model.Monad (MonadAgdaFile (askAgdaFile ), useAgdaFile )
18- import Server.Model.Symbol (SymbolInfo (symbolName ), lspSymbolKind , symbolShortName , symbolType )
19+ import Server.Model.Symbol (SymbolInfo (symbolName ), SymbolKind ( .. ), lspSymbolKind , symbolKind , symbolShortName , symbolType )
1920
2021documentSymbolHandler :: LSP. Handlers ServerM
2122documentSymbolHandler = requestHandlerWithAgdaFile LSP. SMethod_TextDocumentDocumentSymbol $ \ req responder -> do
2223 file <- askAgdaFile
2324 let symbols = symbolsByParent file
2425 let topLevelNames = fromMaybe [] $ Map. lookup Nothing symbols
2526 let topLevelSymbols = mapMaybe (symbolByName file) topLevelNames
26- topLevelDocumentSymbols <- lift $ forM topLevelSymbols $ symbolToDocumentSymbol file symbols
27+ topLevelDocumentSymbols <- lift $ forMaybeM topLevelSymbols $ symbolToDocumentSymbol file symbols
2728 responder $ Right $ LSP. InR $ LSP. InL topLevelDocumentSymbols
2829
29- symbolToDocumentSymbol :: AgdaFile -> Map (Maybe A. QName ) [A. QName ] -> SymbolInfo -> ServerM LSP. DocumentSymbol
30- symbolToDocumentSymbol file symbolsByParent symbol = do
31- let name = symbolName symbol
32- let range = defNameRange file name
33- let childrenNames = fromMaybe [] $ Map. lookup (Just name) symbolsByParent
34- let childrenSymbols = mapMaybe (symbolByName file) childrenNames
35- childrenDocumentSymbols <-
36- forM childrenSymbols $
37- symbolToDocumentSymbol file symbolsByParent
38- return $
39- LSP. DocumentSymbol
40- (symbolShortName symbol)
41- (Text. pack <$> symbolType symbol)
42- (lspSymbolKind symbol)
43- Nothing
44- Nothing
45- range
46- range
47- (Just childrenDocumentSymbols)
30+ symbolToDocumentSymbol ::
31+ AgdaFile ->
32+ Map (Maybe A. QName ) [A. QName ] ->
33+ SymbolInfo ->
34+ ServerM (Maybe LSP. DocumentSymbol )
35+ symbolToDocumentSymbol file symbolsByParent symbol =
36+ if symbolIsDocumentSymbol symbol
37+ then do
38+ let name = symbolName symbol
39+ let range = defNameRange file name
40+ let childrenNames = fromMaybe [] $ Map. lookup (Just name) symbolsByParent
41+ let childrenSymbols = mapMaybe (symbolByName file) childrenNames
42+ childrenDocumentSymbols <-
43+ forMaybeM childrenSymbols $
44+ symbolToDocumentSymbol file symbolsByParent
45+ return $
46+ Just $
47+ LSP. DocumentSymbol
48+ (symbolShortName symbol)
49+ (Text. pack <$> symbolType symbol)
50+ (lspSymbolKind symbol)
51+ Nothing
52+ Nothing
53+ range
54+ range
55+ (Just childrenDocumentSymbols)
56+ else return Nothing
57+
58+ -- | We only want to report "important" symbols as document symbols. For
59+ -- example, top level module definitions should be document symbols, but local
60+ -- variables should not.
61+ symbolIsDocumentSymbol :: SymbolInfo -> Bool
62+ symbolIsDocumentSymbol symbol = case symbolKind symbol of
63+ Con -> True
64+ CoCon -> True
65+ Field -> True
66+ PatternSyn -> True
67+ GeneralizeVar -> True
68+ Macro -> True
69+ Data -> True
70+ Record -> True
71+ Fun -> True
72+ Axiom -> True
73+ Prim -> True
74+ Module -> True
75+ Param -> False
76+ Local -> False
77+ Unknown -> False
0 commit comments