Agda.Interaction.Options

optProgramName :: String
optInputFile :: Maybe FilePath
optIncludeDirs :: Either [FilePath] [AbsolutePath]	`Left` is used temporarily, before the paths have been made absolute. An empty `Left` list is interpreted as `[.]` (see Agda.TypeChecking.Monad.Options.makeIncludeDirsAbsolute).
optShowVersion :: Bool
optShowHelp :: Bool
optInteractive :: Bool
optRunTests :: Bool
optCompile :: Bool
optEpicCompile :: Bool
optCompileDir :: Maybe FilePath	In the absence of a path the project root is used.
optGenerateVimFile :: Bool
optGenerateHTML :: Bool
optHTMLDir :: FilePath
optCSSFile :: Maybe FilePath
optIgnoreInterfaces :: Bool
optForcing :: Bool
optGhcFlags :: [String]
optPragmaOptions :: PragmaOptions
optEpicFlags :: [String]

data PragmaOptions

Source

Options which can be set in a pragma.

Constructors

PragmaOptions

optShowImplicit :: Bool
optVerbose :: Verbosity
optProofIrrelevance :: Bool
optAllowUnsolved :: Bool
optDisablePositivity :: Bool
optTerminationCheck :: Bool
optTerminationDepth :: Int
optCompletenessCheck :: Bool
optUnreachableCheck :: Bool
optUniverseCheck :: Bool
optSizedTypes :: Bool
optInjectiveTypeConstructors :: Bool
optGuardingTypeConstructors :: Bool
optUniversePolymorphism :: Bool
optIrrelevantProjections :: Bool
optWithoutK :: Bool

type OptionsPragma = [String]

Source

The options from an OPTIONS pragma.

In the future it might be nice to switch to a more structured representation. Note that, currently, there is not a one-to-one correspondence between list elements and options.

type Flag opts = opts -> Either String opts

Source

The default output directory for HTML.

f :: Flag opts is an action on the option record that results from parsing an option. f opts produces either an error message or an updated options record

type Verbosity = Trie String Int

Source

checkOpts :: Flag CommandLineOptions

Source

Checks that the given options are consistent.

parseStandardOptions :: [String] -> Either String CommandLineOptions

Source

Parse the standard options.

parsePragmaOptions

Source

:: [String]	Pragma options.
-> CommandLineOptions	Command-line options which should be updated.
-> Either String PragmaOptions
Parse options from an options pragma.