Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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 optsSource

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

checkOpts :: Flag CommandLineOptionsSource

Checks that the given options are consistent.



:: [String]

Pragma options.

-> CommandLineOptions

Command-line options which should be updated.

-> Either String PragmaOptions 

Parse options from an options pragma.

parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag optsSource

Parse options for a plugin.

defaultVerbosity :: VerbositySource

For batch usage.

standardOptions_ :: [OptDescr ()]Source

Used for printing usage info.

isLiterate :: FilePath -> BoolSource

This should probably go somewhere else.

mapFlag :: (String -> String) -> OptDescr a -> OptDescr aSource

Map a function over the long options. Also removes the short options. Will be used to add the plugin name to the plugin options.

usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> StringSource

The usage info message. The argument is the program name (probably agda).