[ git ] Merge pull request #40 from agda-web/raw-responses

Add a CLI option to let the server respond in JSON-interaction style

Author: banacorn

.gitmodules

@@ -4,4 +4,5 @@
 
 [submodule "wasm-submodules/agda"]
 	path = wasm-submodules/agda
-	url = [email protected]:agda-web/agda.git
+	url = https://github.com/agda-web/agda
+	branch = agda-web/release-v2.8.0

src/Agda.hs

@@ -88,10 +88,14 @@ import           GHC.Generics                   ( Generic )
 import           Language.LSP.Server            ( getConfig )
 import           Monad
 import           Options                        ( Config(configRawAgdaOptions)
-                                                , Options(optRawAgdaOptions)
+                                                , Options(optRawAgdaOptions, optRawResponses)
                                                 , versionNumber
                                                 )
 
+import qualified Agda.IR                       as IR
+import           Agda.Interaction.JSON          ( encode, encodeTCM )
+import           Agda.Interaction.JSONTop       ()
+
 getAgdaVersion :: String
 getAgdaVersion = versionWithCommitInfo
 
@@ -104,8 +108,14 @@ start = do
   result <- runAgda $ do
     -- decides how to output Response
     lift $ setInteractionOutputCallback $ \response -> do
-      reaction <- fromResponse response
-      sendResponse env reaction
+      resp <- if optRawResponses (envOptions env)
+        then do
+          value <- (pure . encodeTCM) response
+          resp' <- fmap IR.ResponseJSONRaw value
+          return resp'
+        else fromResponse response
+
+      sendResponse env resp
 
     -- keep reading command
     commands <- liftIO $ initialiseCommandQueue (readCommand env)

src/Agda/IR.hs

@@ -44,6 +44,8 @@ data Response
   | ResponseMimer Int (Maybe String)
   | -- priority: 3
     ResponseJumpToError FilePath Int
+  | -- raw form
+    ResponseJSONRaw Value
   | ResponseEnd
   deriving (Generic)
 

src/Options.hs

@@ -39,14 +39,15 @@ usageMessage = usageInfo usage options ++ usageAboutAgdaOptions
 data Options = Options
   { optViaTCP :: Maybe Int,
     optRawAgdaOptions :: [String],
+    optRawResponses :: Bool,
     optSetup :: Bool,
     optHelp :: Bool,
     optVersion :: Bool
   }
 
 defaultOptions :: Options
 defaultOptions =
-  Options {optViaTCP = Nothing, optRawAgdaOptions = [], optSetup = False, optHelp = False, optVersion = False}
+  Options {optViaTCP = Nothing, optRawAgdaOptions = [], optRawResponses = False, optSetup = False, optHelp = False, optVersion = False}
 
 options :: [OptDescr (Options -> Options)]
 options =
@@ -66,6 +67,11 @@ options =
           "PORT"
       )
       "talk with the editor via TCP port (4096 as default)",
+    Option
+      []
+      ["raw"]
+      (NoArg (\opts -> opts {optRawResponses = True}))
+      "return all responses in raw JSON format",
 #if MIN_VERSION_Agda(2,8,0)
     Option
       []