Agda.Main · Agda-2.7.0.1 · horizon-platform

valuerunAgda :: [Backend] -> IO ()

#

The main function

valuerunAgda' :: [Backend] -> IO ()

#

The main function without importing built-in backends

datadata MainMode

#

Main execution mode

Constructors

MainModeRun (Interactor ())
MainModePrintHelp Help
MainModePrintVersion PrintAgdaVersion
MainModePrintAgdaDataDir
MainModePrintAgdaAppDir

valuegetMainMode

#

Determine the main execution mode to run, based on the configured backends and command line options. | This is pure.

typetype Interactor a = TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM a

#

datadata FrontendType

#

FrontEndEmacs FrontEndJson FrontEndRepl

valueemacsModeInteractor :: Interactor ()

#

valuejsonModeInteractor :: Interactor ()

#

valuereplInteractor :: Maybe AbsolutePath -> Interactor ()

#

valuedefaultInteractor :: AbsolutePath -> Interactor ()

#

valuegetInteractor

#

valuerunAgdaWithOptions

:: Interactor a
Backend interaction
-> String
program name
-> CommandLineOptions
parsed command line options
-> TCM a

#

Run Agda with parsed command line options

valueprintUsage :: [Backend] -> Help -> IO ()

#

Print usage information.

valuebackendUsage :: Backend -> String

#

valueprintVersion :: [Backend] -> PrintAgdaVersion -> IO ()

#

Print version information.

valueprintAgdaDataDir :: IO ()

#

valueprintAgdaAppDir :: IO ()

#

valueoptionError :: String -> IO ()

#

What to do for bad options.

valuerunTCMPrettyErrors :: TCM () -> IO ()

#

Run a TCM action in IO; catch and pretty print errors.

valuehelpForLocaleError :: TCErr -> IO ()

#

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.