The main function
ModuleAgda-2.8.0.2Haskell2010
Agda.Main
Agda main module.
Synopsis
- value runAgda
- value runAgda'
- type Interactor
- data FrontendType
- data InteractionFormat
- pattern FrontEndEmacs
- pattern FrontEndJson
- value buildLibraryInteractor
- value interactionInteractor
- value replInteractor
- value defaultInteractor
- value getInteractor
- value runAgdaWithOptions
- value printUsage
- value backendUsage
- value printVersion
- value printAgdaDataDir
- value printAgdaAppDir
- value optionError
- value runTCMPrettyErrors
- value helpForLocaleError
- PackageAgda-2.8.0.2
- Exports21
- LanguageHaskell2010
- LicenceMIT
- SourceMain.hs
The main function without importing built-in backends
Major mode of operation, not including the standard mode (checking the given main module).
Constructors
FrontEndInteraction InteractionFormat--interactionor--interaction-json.FrontEndRepl--interactive.FrontEndBuildLibrary--build-library.
Constructors
InteractionEmacs--interaction.InteractionJson--interaction-json.
Emacs/JSON mode. Note that it ignores the "check" action because it calls typeCheck directly.
The (deprecated) repl mode.
The interactor to use when there are no frontends or backends specified.
value
runAgdaWithOptions :: Interactor aBackend interaction
-> Stringprogram name
-> CommandLineOptionsparsed command line options
-> TCM a
Run Agda with parsed command line options
Print usage information.
Print version information.
What to do for bad options.
Run a TCM action in IO; catch and pretty print errors.
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.