Agda.Main · Agda-2.8.0.2 · horizon-platform

valuerunAgda :: [Backend] -> IO ()

#

The main function

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

#

The main function without importing built-in backends

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

#

datadata FrontendType

#

Major mode of operation, not including the standard mode (checking the given main module).

Constructors

FrontEndInteraction InteractionFormat
--interaction or --interaction-json.
FrontEndRepl
--interactive.
FrontEndBuildLibrary
--build-library.

datadata InteractionFormat

#

Constructors

InteractionEmacs
--interaction.
InteractionJson
--interaction-json.

patternpattern FrontEndEmacs :: FrontendType

#

patternpattern FrontEndJson :: FrontendType

#

valuebuildLibraryInteractor :: Interactor ()

#

valueinteractionInteractor :: InteractionFormat -> Interactor ()

#

Emacs/JSON mode. Note that it ignores the "check" action because it calls typeCheck directly.

valuereplInteractor :: Maybe AbsolutePath -> Interactor ()

#

The (deprecated) repl mode.

valuedefaultInteractor :: AbsolutePath -> Interactor ()

#

The interactor to use when there are no frontends or backends specified.

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.