| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Main
Description
Agda main module.
Synopsis
- runAgda :: [Backend] -> IO ()
- runAgda' :: [Backend] -> IO ()
- data MainMode
- getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
- type Interactor a = TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM a
- data FrontendType
- emacsModeInteractor :: Interactor ()
- jsonModeInteractor :: Interactor ()
- replInteractor :: Maybe AbsolutePath -> Interactor ()
- defaultInteractor :: AbsolutePath -> Interactor ()
- getInteractor :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m (Maybe (Interactor ()))
- runAgdaWithOptions :: Interactor a -> String -> CommandLineOptions -> TCM a
- printUsage :: [Backend] -> Help -> IO ()
- backendUsage :: Backend -> String
- printVersion :: [Backend] -> PrintAgdaVersion -> IO ()
- printAgdaDataDir :: IO ()
- printAgdaAppDir :: IO ()
- optionError :: String -> IO ()
- runTCMPrettyErrors :: TCM () -> IO ()
- helpForLocaleError :: TCErr -> IO ()
Documentation
Main execution mode
getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode Source #
Determine the main execution mode to run, based on the configured backends and command line options. | This is pure.
type Interactor a = TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM a Source #
data FrontendType Source #
Constructors
| FrontEndEmacs | |
| FrontEndJson | |
| FrontEndRepl |
emacsModeInteractor :: Interactor () Source #
jsonModeInteractor :: Interactor () Source #
replInteractor :: Maybe AbsolutePath -> Interactor () Source #
defaultInteractor :: AbsolutePath -> Interactor () Source #
getInteractor :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m (Maybe (Interactor ())) Source #
Arguments
| :: Interactor a | Backend interaction |
| -> String | program name |
| -> CommandLineOptions | parsed command line options |
| -> TCM a |
Run Agda with parsed command line options
printUsage :: [Backend] -> Help -> IO () Source #
Print usage information.
backendUsage :: Backend -> String Source #
printVersion :: [Backend] -> PrintAgdaVersion -> IO () Source #
Print version information.
printAgdaDataDir :: IO () Source #
printAgdaAppDir :: IO () Source #
optionError :: String -> IO () Source #
What to do for bad options.
runTCMPrettyErrors :: TCM () -> IO () Source #
Run a TCM action in IO; catch and pretty print errors.
helpForLocaleError :: TCErr -> IO () Source #
If the error is an IO error, and the error message suggests that the problem is related to locales or code pages, print out some extra information.