From 6acb5e84d4ce8b3f3b3b24b576c7100e62c2ca20 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Tue, 14 Oct 2025 16:18:32 +0800 Subject: [PATCH 1/2] Change submodule upstream url to use https --- .gitmodules | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index dc10f3e..a0d74ae 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,4 +4,5 @@ [submodule "wasm-submodules/agda"] path = wasm-submodules/agda - url = git@github.com:agda-web/agda.git + url = https://github.com/agda-web/agda + branch = agda-web/release-v2.8.0 From 1c76bbf9dde0f1a328578f27d8af2ae843175475 Mon Sep 17 00:00:00 2001 From: Andy Pan Date: Wed, 15 Oct 2025 03:56:43 +0800 Subject: [PATCH 2/2] Add an option to let LSP respond as if in JSON interaction mode --- src/Agda.hs | 16 +++++++++++++--- src/Agda/IR.hs | 2 ++ src/Options.hs | 8 +++++++- wasm-submodules/agda | 2 +- 4 files changed, 23 insertions(+), 5 deletions(-) diff --git a/src/Agda.hs b/src/Agda.hs index 197eb9e..53f7330 100644 --- a/src/Agda.hs +++ b/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) diff --git a/src/Agda/IR.hs b/src/Agda/IR.hs index e450a76..ab40fa6 100644 --- a/src/Agda/IR.hs +++ b/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) diff --git a/src/Options.hs b/src/Options.hs index ef8af48..27742d5 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -39,6 +39,7 @@ usageMessage = usageInfo usage options ++ usageAboutAgdaOptions data Options = Options { optViaTCP :: Maybe Int, optRawAgdaOptions :: [String], + optRawResponses :: Bool, optSetup :: Bool, optHelp :: Bool, optVersion :: Bool @@ -46,7 +47,7 @@ data Options = Options 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 [] diff --git a/wasm-submodules/agda b/wasm-submodules/agda index e2f8c69..702c924 160000 --- a/wasm-submodules/agda +++ b/wasm-submodules/agda @@ -1 +1 @@ -Subproject commit e2f8c69414fa115328280ecc4de1d2b7a23be7fa +Subproject commit 702c924fdab93aa8992adca84e72a91c490f7b1b