Idris.Parser

Reexports

Definitions

record ParseOpts : Type

Totality: total
Visibility: public export
Constructor: 

MkParseOpts : Bool -> Bool -> ParseOpts

Projections:

.eqOK : ParseOpts -> Bool

.withOK : ParseOpts -> Bool

.eqOK : ParseOpts -> Bool

Visibility: public export

eqOK : ParseOpts -> Bool

Visibility: public export

.withOK : ParseOpts -> Bool

Visibility: public export

withOK : ParseOpts -> Bool

Visibility: public export

pdef : ParseOpts

Visibility: export

plhs : ParseOpts

Visibility: export

debugString : OriginDesc -> Rule PTerm

Visibility: export

expr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm

Visibility: export

singlelineStr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm

Visibility: export

multilineStr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm

Visibility: export

import_ : OriginDesc -> IndentInfo -> Rule Import

Visibility: export

progHdr : OriginDesc -> EmptyRule Module

Visibility: export

prog : OriginDesc -> EmptyRule Module

Visibility: export

data CmdArg : Type

Totality: total
Visibility: export
Constructors:

NoArg : CmdArg

  The command takes no arguments.

NameArg : CmdArg

  The command takes a name.

ExprArg : CmdArg

  The command takes an expression.

DocArg : CmdArg

  The command takes a documentation directive.

DeclsArg : CmdArg

  The command takes a list of declarations

NumberArg : CmdArg

  The command takes a number.

AutoNumberArg : CmdArg

  The command takes a number or auto.

OptionArg : CmdArg

  The command takes an option.

FileArg : CmdArg

  The command takes a file.

ModuleArg : CmdArg

  The command takes a module.

StringArg : CmdArg

  The command takes a string

OnOffArg : CmdArg

  The command takes a on or off.

NamedCmdArg : String -> CmdArg -> CmdArg

  The command takes an argument documenting its name

WithDefaultArg : String -> CmdArg -> CmdArg

  The command takes an argument documenting its default value

CSVArg : CmdArg -> CmdArg

  The command takes arguments separated by commas

Args : List CmdArg -> CmdArg

  The command takes multiple arguments.

Hint: 

Show CmdArg

knownCommands : List (String, String)

Visibility: public export

KnownCommand : String -> Type

Visibility: public export

data ParseCmd : Type

Totality: total
Visibility: export
Constructors:

ParseREPLCmd : (cmds : List String) -> {auto 0 _ : All KnownCommand cmds} -> ParseCmd

ParseKeywordCmd : (cmds : List String) -> {auto 0 _ : All KnownCommand cmds} -> ParseCmd

ParseIdentCmd : (cmd : String) -> {auto 0 _ : KnownCommand cmd} -> ParseCmd

CommandDefinition : Type

Visibility: public export

CommandTable : Type

Visibility: public export

parserCommandsForHelp : CommandTable

Visibility: export

help : List (List String, (CmdArg, String))

Visibility: export

aPTerm : Rule PTerm

Visibility: export

command : EmptyRule REPLCmd

Visibility: export