Agda.Interaction.Options
- data CommandLineOptions = Options {
- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludeDirs :: [FilePath]
- optShowVersion :: Bool
- optShowHelp :: Bool
- optInteractive :: Bool
- optVerbose :: Trie String Int
- optProofIrrelevance :: Bool
- optAllowUnsolved :: Bool
- optShowImplicit :: Bool
- optRunTests :: Bool
- optCompile :: Bool
- optGenerateVimFile :: Bool
- optGenerateHTML :: Bool
- optHTMLDir :: FilePath
- optCSSFile :: Maybe FilePath
- optIgnoreInterfaces :: Bool
- optDisablePositivity :: Bool
- optCompileAlonzo :: Bool
- optCompileMAlonzo :: Bool
- optMAlonzoDir :: Maybe FilePath
- optTerminationCheck :: Bool
- optCompletenessCheck :: Bool
- optUnreachableCheck :: Bool
- optUniverseCheck :: Bool
- optSizedTypes :: Bool
- optUniversePolymorphism :: Bool
- optGhcFlags :: [String]
- type Flag opts = opts -> Either String opts
- checkOpts :: Flag CommandLineOptions
- parseStandardOptions :: String -> [String] -> Either String CommandLineOptions
- parsePragmaOptions :: [String] -> CommandLineOptions -> Either String CommandLineOptions
- parsePluginOptions :: String -> [String] -> opts -> [OptDescr (Flag opts)] -> Either String opts
- defaultOptions :: CommandLineOptions
- standardOptions_ :: [OptDescr ()]
- isLiterate :: FilePath -> Bool
- mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
- usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> String
- tests :: IO Bool
Documentation
data CommandLineOptions Source
Constructors
| Options | |
Fields
| |
Instances
type Flag opts = opts -> Either String optsSource
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
checkOpts :: Flag CommandLineOptionsSource
Checks that the given options are consistent.
parseStandardOptions :: String -> [String] -> Either String CommandLineOptionsSource
Parse the standard options.
parsePragmaOptions :: [String] -> CommandLineOptions -> Either String CommandLineOptionsSource
Parse options from an options pragma.
parsePluginOptions :: String -> [String] -> opts -> [OptDescr (Flag opts)] -> Either String optsSource
Parse options for a plugin.
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.