diff --git a/.gitignore b/.gitignore index 41f3983..14ce36d 100644 --- a/.gitignore +++ b/.gitignore @@ -21,3 +21,6 @@ node_modules/ cabal.sandbox.config cabal.project.local *~ + + +*.agdai \ No newline at end of file diff --git a/test/Test/LSP.hs b/test/Test/LSP.hs index 62c0f70..2a78683 100644 --- a/test/Test/LSP.hs +++ b/test/Test/LSP.hs @@ -6,6 +6,7 @@ import Agda import Control.Monad.IO.Class import qualified Data.Aeson as JSON import Language.LSP.Protocol.Message +import Language.LSP.Protocol.Types import Language.LSP.Test import Switchboard (agdaCustomMethod) import Test.Tasty @@ -24,14 +25,18 @@ demo alsPath = do runSession alsPath fullLatestClientCaps "test/data/" $ do doc <- openDoc "A.agda" "agda" - -- Use your favourite favourite combinators. - -- skipManyTill loggingNotification (count 1 publishDiagnosticsNotification) + -- hover + TResponseMessage _ _ rsp <- request SMethod_TextDocumentHover (HoverParams doc (Position 3 9) Nothing) + case rsp of + Right (InL (Hover (InL (MarkupContent _ content)) (Just (Range start end)))) -> liftIO $ do + content @?= "\n```agda-language-server\nAgda.Primitive.Set\n```\n" + start @?= Position 3 9 + end @?= Position 3 9 + _ -> liftIO $ assertFailure "Unexpected response" + -- agda-mode:load testCustomMethod "IOTCM \"test/data/A.agdaa\" NonInteractive Direct( Cmd_load \"test/data/A.agda\" [] )" --- Or use one of the helper functions --- getDocumentSymbols doc >>= liftIO . print - -- | Sends a custom method request to the server and expects a response of `CmdRes Nothing` testCustomMethod :: String -> Session () testCustomMethod cmd = do diff --git a/test/Test/SrcLoc.hs b/test/Test/SrcLoc.hs index af4c3e4..c3928b7 100644 --- a/test/Test/SrcLoc.hs +++ b/test/Test/SrcLoc.hs @@ -1,11 +1,11 @@ module Test.SrcLoc where -import Test.Tasty -import Test.Tasty.HUnit -import Data.List (sort) import Agda.Position -import Data.Text (Text) import qualified Data.IntMap as IntMap +import Data.List (sort) +import Data.Text (Text) +import Test.Tasty +import Test.Tasty.HUnit tests :: TestTree tests = testGroup "Source Location" [positionToOffsetTests, offsetToPositionTests] @@ -16,14 +16,14 @@ positionToOffsetTests :: TestTree positionToOffsetTests = testGroup "Position => Offset" - [ testCase "cached table" $ IntMap.toList (unToOffset table) @?= [(1, 4), (2, 9), (3, 12)] - , testCase "line 0" $ run [(0, 0), (0, 1), (0, 2), (0, 3)] @?= [0, 1, 2, 3] - , testCase "line 1" $ run [(1, 0), (1, 1), (1, 2), (1, 3), (1, 4)] @?= [4, 5, 6, 7, 8] - , testCase "line 2" $ run [(2, 0), (2, 1)] @?= [9, 10] - , testCase "line 3" $ run [(3, 0), (3, 1)] @?= [12, 13] + [ testCase "cached table" $ IntMap.toList (unToOffset table) @?= [(1, 4), (2, 9), (3, 12)], + testCase "line 0" $ run [(0, 0), (0, 1), (0, 2), (0, 3)] @?= [0, 1, 2, 3], + testCase "line 1" $ run [(1, 0), (1, 1), (1, 2), (1, 3), (1, 4)] @?= [4, 5, 6, 7, 8], + testCase "line 2" $ run [(2, 0), (2, 1)] @?= [9, 10], + testCase "line 3" $ run [(3, 0), (3, 1)] @?= [12, 13] ] where - text :: Text + text :: Text text = "012\n456\r\n90\r23" table :: ToOffset @@ -31,21 +31,21 @@ positionToOffsetTests = run :: [(Int, Int)] -> [Int] run = map (toOffset table) - + -------------------------------------------------------------------------------- offsetToPositionTests :: TestTree offsetToPositionTests = testGroup "Offset => Position" - [ testCase "cached table" $ IntMap.toList (unFromOffset table) @?= [(4, 1), (9, 2), (12, 3)] - , testCase "line 0" $ run [0, 1, 2, 3] @?= [(0, 0), (0, 1), (0, 2), (0, 3)] - , testCase "line 1" $ run [4, 5, 6, 7, 8] @?= [(1, 0), (1, 1), (1, 2), (1, 3), (1, 4)] - , testCase "line 2" $ run [9, 10] @?= [(2, 0), (2, 1)] - , testCase "line 3" $ run [12, 13] @?= [(3, 0), (3, 1)] + [ testCase "cached table" $ IntMap.toList (unFromOffset table) @?= [(4, 1), (9, 2), (12, 3)], + testCase "line 0" $ run [0, 1, 2, 3] @?= [(0, 0), (0, 1), (0, 2), (0, 3)], + testCase "line 1" $ run [4, 5, 6, 7, 8] @?= [(1, 0), (1, 1), (1, 2), (1, 3), (1, 4)], + testCase "line 2" $ run [9, 10] @?= [(2, 0), (2, 1)], + testCase "line 3" $ run [12, 13] @?= [(3, 0), (3, 1)] ] where - text :: Text + text :: Text text = "012\n456\r\n90\r23" table :: FromOffset @@ -53,4 +53,3 @@ offsetToPositionTests = run :: [Int] -> [(Int, Int)] run = map (fromOffset table) - \ No newline at end of file