{-# LANGUAGE DeriveGeneric #-}
module Options
( Options(..)
, getOptionsFromArgv
, usageMessage
, Config(..)
, initConfig
) where
import Data.Aeson.Types hiding ( Options
, defaultOptions
)
import GHC.Generics ( Generic )
import System.Console.GetOpt
import System.Environment ( getArgs )
import Text.Read ( readMaybe )
getOptionsFromArgv :: IO Options
getOptionsFromArgv = do
-- extract options for Agda from ARGV
(argvForALS, argvForAgda) <- extractAgdaOpts <$> getArgs
-- parse options for ALS
(opts , _ ) <- parseOpts argvForALS
-- save options for Agda back
return $ opts { optRawAgdaOptions = argvForAgda }
usageMessage :: String
usageMessage = usageInfo usage options ++ usageAboutAgdaOptions
--------------------------------------------------------------------------------
-- | Command-line arguments
data Options = Options
{ optViaTCP :: Maybe Int
, optRawAgdaOptions :: [String]
, optHelp :: Bool
}
defaultOptions :: Options
defaultOptions =
Options { optViaTCP = Nothing, optRawAgdaOptions = [], optHelp = False }
options :: [OptDescr (Options -> Options)]
options =
[ Option ['h']
["help"]
(NoArg (\opts -> opts { optHelp = True }))
"print this help message"
, Option
['p']
["port"]
(OptArg
(\port opts -> case port of
Just n -> opts { optViaTCP = readMaybe n }
Nothing -> opts { optViaTCP = Just 4096 }
)
"PORT"
)
"talk with the editor via TCP port (4096 as default)"
]
usage :: String
usage = "Agda Language Server v0.0.3.0 \nUsage: als [Options...]\n"
usageAboutAgdaOptions :: String
usageAboutAgdaOptions =
"\n\
\ +AGDA [Options for Agda ...] -AGDA\n\
\ To pass command line options to Agda, put them in between '+AGDA' and '-AGDA'\n\
\ For example:\n\
\ als -p=3000 +AGDA --cubical -AGDA\n\
\ If you are using agda-mode on VS Code, put them in the Settings at:\n\
\ agdaMode.connection.commandLineOptions\n\
\"
parseOpts :: [String] -> IO (Options, [String])
parseOpts argv = case getOpt Permute options argv of
(o, n, [] ) -> return (foldl (flip id) defaultOptions o, n)
(_, _, errs) -> ioError $ userError $ concat errs ++ usageInfo usage options
-- | Removes RTS options from a list of options (stolen from Agda)
stripRTS :: [String] -> [String]
stripRTS [] = []
stripRTS ("--RTS" : argv) = argv
stripRTS (arg : argv)
| is "+RTS" arg = stripRTS $ drop 1 $ dropWhile (not . is "-RTS") argv
| otherwise = arg : stripRTS argv
where is x arg = [x] == take 1 (words arg)
-- | Extract Agda options (+AGDA ... -AGDA) from a list of options
extractAgdaOpts :: [String] -> ([String], [String])
extractAgdaOpts argv =
let (before , argv') = break (== "+AGDA") argv
(forAgda, after) = break (== "-AGDA") argv'
forALS = before ++ dropWhile (== "-AGDA") after
forAgda' = dropWhile (== "+AGDA") forAgda
in (forALS, forAgda')
--------------------------------------------------------------------------------
newtype Config = Config { configRawAgdaOptions :: [String] }
deriving (Eq, Show, Generic)
instance FromJSON Config where
parseJSON (Object v) = Config <$> v .: "commandLineOptions"
-- We do not expect a non-Object value here.
-- We could use empty to fail, but typeMismatch
-- gives a much more informative error message.
parseJSON invalid =
prependFailure "parsing Config failed, " (typeMismatch "Object" invalid)
initConfig :: Config
initConfig = Config []