Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered

Agda.Interaction.Options

Synopsis

Documentation

type OptionsPragma = [String]

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

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 CommandLineOptions

Checks that the given options are consistent.

parseStandardOptions :: [String] -> Either String CommandLineOptions

Parse the standard options.

parsePragmaOptions

Arguments

:: [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 opts

Parse options for a plugin.

standardOptions_ :: [OptDescr ()]

Used for printing usage info.

isLiterate :: FilePath -> Bool

This should probably go somewhere else.

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

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 -> String

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