[ test ] Primitive testing for hover

Author: banacorn

.gitignore

@@ -21,3 +21,6 @@ node_modules/
 cabal.sandbox.config
 cabal.project.local
 *~
+
+
+*.agdai

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

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,41 +16,40 @@ 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
     table = makeToOffset text
 
     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
     table = makeFromOffset text
 
     run :: [Int] -> [(Int, Int)]
     run = map (fromOffset table)
-