Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .gitmodules
Original file line number Diff line number Diff line change
Expand Up @@ -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
16 changes: 13 additions & 3 deletions src/Agda.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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)
Expand Down
2 changes: 2 additions & 0 deletions src/Agda/IR.hs
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,8 @@ data Response
| ResponseMimer Int (Maybe String)
| -- priority: 3
ResponseJumpToError FilePath Int
| -- raw form
ResponseJSONRaw Value
| ResponseEnd
deriving (Generic)

Expand Down
8 changes: 7 additions & 1 deletion src/Options.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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
[]
Expand Down
2 changes: 1 addition & 1 deletion wasm-submodules/agda
Submodule agda updated 2988 files