[ new ] Merge & use command-line options passed from agda-mode

Author: banacorn

src/Agda.hs

@@ -64,8 +64,11 @@ 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                        ( Options(optRawAgdaOptions) )
+import           Options                        ( Config(configRawAgdaOptions)
+                                                , Options(optRawAgdaOptions)
+                                                )
 
 getAgdaVersion :: String
 getAgdaVersion = versionWithCommitInfo
@@ -167,10 +170,16 @@ parseIOTCM raw = case listToMaybe $ reads raw of
 getCommandLineOptions
   :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions
 getCommandLineOptions = do
+  -- command line options from ARGV 
   argv   <- asks (optRawAgdaOptions . envOptions)
+  -- command line options from agda-mode
+  config <- asks (configRawAgdaOptions . envConfig)
+  -- concatenate both 
+  let merged = argv <> config
+
   result <- runExceptT $ do
     (bs, opts) <- ExceptT $ runOptM $ parseBackendOptions builtinBackends
-                                                          argv
+                                                          merged
                                                           defaultOptions
     return opts
   case result of

src/Monad.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts #-}
 module Monad where
 
 import           Agda.IR
@@ -21,6 +22,9 @@ import           Data.IORef                     ( IORef
                                                 , writeIORef
                                                 )
 import           Data.Maybe                     ( isJust )
+import           Language.LSP.Server            ( MonadLsp
+                                                , getConfig
+                                                )
 import qualified Language.LSP.Types            as LSP
 import           Options
 
@@ -29,19 +33,21 @@ import           Options
 data Env = Env
   { envOptions            :: Options
   , envDevMode            :: Bool
+  , envConfig             :: Config
   , envLogChan            :: Chan Text
   , envCommandController  :: CommandController
   , envResponseChan       :: Chan Response
   , envResponseController :: ResponseController
   }
 
-createInitEnv :: Options -> IO Env
+createInitEnv :: (MonadIO m, MonadLsp Config m) => Options -> m Env
 createInitEnv options =
   Env options (isJust (optViaTCP options))
-    <$> newChan
-    <*> CommandController.new
-    <*> newChan
-    <*> ResponseController.new
+    <$> getConfig
+    <*> liftIO newChan
+    <*> liftIO CommandController.new
+    <*> liftIO newChan
+    <*> liftIO ResponseController.new
 
 --------------------------------------------------------------------------------
 

src/Options.hs

@@ -30,9 +30,9 @@ usageMessage = usageInfo usage options ++ usageAboutAgdaOptions
 
 -- | Command-line arguments
 data Options = Options
-  { optViaTCP      :: Maybe Int
+  { optViaTCP         :: Maybe Int
   , optRawAgdaOptions :: [String]
-  , optHelp        :: Bool
+  , optHelp           :: Bool
   }
 
 defaultOptions :: Options
@@ -96,7 +96,7 @@ extractAgdaOpts argv =
 
 --------------------------------------------------------------------------------
 
-newtype Config = Config { commandLineOptions :: [String] }
+newtype Config = Config { configRawAgdaOptions :: [String] }
   deriving (Eq, Show, Generic)
 
 instance FromJSON Config where

src/Server.hs

@@ -36,34 +36,35 @@ import           Options
 --------------------------------------------------------------------------------
 
 run :: Options -> IO Int
-run alsOptions = do
-  env         <- createInitEnv alsOptions
-  switchboard <- Switchboard.new env
-  case optViaTCP alsOptions of
+run options = do
+  case optViaTCP options of
     Just port -> do
       void
         $ TCP.serve (TCP.Host "127.0.0.1") (show port)
         $ \(sock, _remoteAddr) -> do
-            writeChan (envLogChan env) "[Server] connection established"
+            -- writeChan (envLogChan env) "[Server] connection established"
             handle <- socketToHandle sock ReadWriteMode
-            _ <- runServerWithHandles handle handle (serverDefn env switchboard)
+            _      <- runServerWithHandles handle handle (serverDefn options)
             return ()
-      Switchboard.destroy switchboard
+      -- Switchboard.destroy switchboard
       return 0
     Nothing -> do
-      runServer (serverDefn env switchboard)
+      runServer (serverDefn options)
  where
-  serverDefn :: Env -> Switchboard -> ServerDefinition Config
-  serverDefn env switchboard = ServerDefinition
+  serverDefn :: Options -> ServerDefinition Config
+  serverDefn options = ServerDefinition
     { defaultConfig         = initConfig
     , onConfigurationChange = \old newRaw -> case JSON.fromJSON newRaw of
       JSON.Error s -> Left $ pack $ "Cannot parse server configuration: " <> s
       JSON.Success new -> Right new
     , doInitialize          = \ctxEnv _req -> do
+                                env <- runLspT ctxEnv (createInitEnv options)
+                                switchboard <- Switchboard.new env
                                 Switchboard.setupLanguageContextEnv switchboard ctxEnv
-                                pure $ Right ctxEnv
+                                pure $ Right (ctxEnv, env)
     , staticHandlers        = handlers
-    , interpretHandler = \ctxEnv -> Iso (runLspT ctxEnv . runServerM env) liftIO
+    , interpretHandler      = \(ctxEnv, env) ->
+                                Iso (runLspT ctxEnv . runServerM env) liftIO
     , options               = lspOptions
     }