Remove all response converter, just use output of JSON backend

Author: andy0130tw

agda-language-server.cabal

@@ -48,25 +48,12 @@ flag Agda-2-8-0
 library
   exposed-modules:
       Agda
-      Agda.Convert
       Agda.IR
       Agda.Parser
       Agda.Position
       Control.Concurrent.SizedChan
       Monad
       Options
-      Render
-      Render.Class
-      Render.Common
-      Render.Concrete
-      Render.Interaction
-      Render.Internal
-      Render.Literal
-      Render.Name
-      Render.Position
-      Render.RichText
-      Render.TypeChecking
-      Render.Utils
       Server
       Server.CommandController
       Server.Handler
@@ -81,7 +68,7 @@ library
       OverloadedStrings
       PatternSynonyms
       TypeOperators
-  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Werror=incomplete-patterns -fno-warn-orphans
+  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Werror=incomplete-patterns -fno-warn-orphans -Wunused-imports -fsplit-sections
   build-depends:
       Agda
     , aeson
@@ -127,7 +114,7 @@ executable als
       OverloadedStrings
       PatternSynonyms
       TypeOperators
-  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans
+  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans -Wunused-imports -fsplit-sections
   build-depends:
       Agda
     , aeson
@@ -172,25 +159,12 @@ test-suite als-test
       Test.SrcLoc
       Test.WASM
       Agda
-      Agda.Convert
       Agda.IR
       Agda.Parser
       Agda.Position
       Control.Concurrent.SizedChan
       Monad
       Options
-      Render
-      Render.Class
-      Render.Common
-      Render.Concrete
-      Render.Interaction
-      Render.Internal
-      Render.Literal
-      Render.Name
-      Render.Position
-      Render.RichText
-      Render.TypeChecking
-      Render.Utils
       Server
       Server.CommandController
       Server.Handler
@@ -205,7 +179,7 @@ test-suite als-test
       OverloadedStrings
       PatternSynonyms
       TypeOperators
-  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans
+  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans -Wunused-imports -fsplit-sections
   build-depends:
       Agda
     , aeson

app/Main.hs

@@ -5,12 +5,10 @@ import Control.Monad (when)
 import Options
 import Server (run)
 -- import Simple (run)
-import System.Console.GetOpt
 import System.Directory (doesDirectoryExist)
 import System.Environment
 import System.FilePath ((</>))
 import System.IO
-import Text.Read (readMaybe)
 
 #if MIN_VERSION_Agda(2,8,0)
 import Agda.Setup (setup)

hie.yaml

@@ -1,13 +1,2 @@
 cradle:
-  stack:
-    - path: "./src"
-      component: "agda-language-server:lib"
-
-    - path: "./app/Main.hs"
-      component: "agda-language-server:exe:als"
-
-    - path: "./app/Paths_agda_language_server.hs"
-      component: "agda-language-server:exe:als"
-
-    - path: "./test"
-      component: "agda-language-server:test:als-test"
+  cabal:

src/Agda.hs

@@ -16,15 +16,13 @@ import           Prelude                        hiding ( null )
 
 import           Agda.Compiler.Backend          ( parseBackendOptions )
 import           Agda.Compiler.Builtin          ( builtinBackends )
-import           Agda.Convert                   ( fromResponse )
 import           Agda.Interaction.Base          ( Command
                                                 , Command'(Command, Done, Error)
 #if MIN_VERSION_Agda(2,7,0)
 #else
                                                 , CommandM
 #endif
                                                 , CommandState(optionsOnReload)
-                                                , IOTCM
                                                 , initCommandState
                                                 , parseIOTCM
                                                 )
@@ -61,7 +59,6 @@ import           Agda.TypeChecking.Monad.Base   ( TCM )
 import qualified Agda.TypeChecking.Monad.Benchmark
                                                as Bench
 import           Agda.TypeChecking.Monad.State  ( setInteractionOutputCallback )
-import           Agda.Utils.FileName            ( absolute )
 import           Agda.Utils.Impossible          ( CatchImpossible
                                                   ( catchImpossible
                                                   )
@@ -82,18 +79,16 @@ import           Data.Aeson                     ( FromJSON
                                                 , fromJSON
                                                 )
 import qualified Data.Aeson                    as JSON
-import           Data.Maybe                     ( listToMaybe )
 import           Data.Text                      ( pack )
 import           GHC.Generics                   ( Generic )
-import           Language.LSP.Server            ( getConfig )
 import           Monad
 import           Options                        ( Config(configRawAgdaOptions)
-                                                , Options(optRawAgdaOptions, optRawResponses)
+                                                , Options(optRawAgdaOptions)
                                                 , versionNumber
                                                 )
 
 import qualified Agda.IR                       as IR
-import           Agda.Interaction.JSON          ( encode, encodeTCM )
+import           Agda.Interaction.JSON          ( encodeTCM )
 import           Agda.Interaction.JSONTop       ()
 
 getAgdaVersion :: String
@@ -108,13 +103,8 @@ start = do
   result <- runAgda $ do
     -- decides how to output Response
     lift $ setInteractionOutputCallback $ \response -> do
-      resp <- if optRawResponses (envOptions env)
-        then do
-          value <- (pure . encodeTCM) response
-          resp' <- fmap IR.ResponseJSONRaw value
-          return resp'
-        else fromResponse response
-
+      value <- (pure . encodeTCM) response
+      resp <- fmap IR.ResponseJSONRaw value
       sendResponse env resp
 
     -- keep reading command