| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Idris.IdeMode
- parseMessage :: String -> Either Err (SExp, Integer)
- convSExp :: SExpable a => String -> a -> Integer -> String
- data WhatDocs
- data IdeModeCommand
- = REPLCompletions String
- | Interpret String
- | TypeOf String
- | CaseSplit Int String
- | AddClause Int String
- | AddProofClause Int String
- | AddMissing Int String
- | MakeWithBlock Int String
- | MakeCaseBlock Int String
- | ProofSearch Bool Int String [String] (Maybe Int)
- | MakeLemma Int String
- | LoadFile String (Maybe Int)
- | DocsFor String WhatDocs
- | Apropos String
- | GetOpts
- | SetOpt Opt Bool
- | Metavariables Int
- | WhoCalls String
- | CallsWho String
- | BrowseNS String
- | TermNormalise [(Name, Bool)] Term
- | TermShowImplicits [(Name, Bool)] Term
- | TermNoImplicits [(Name, Bool)] Term
- | TermElab [(Name, Bool)] Term
- | PrintDef String
- | ErrString Err
- | ErrPPrint Err
- | GetIdrisVersion
- sexpToCommand :: SExp -> Maybe IdeModeCommand
- data SExp
- class SExpable a where
- data Opt
- ideModeEpoch :: Int
- getLen :: Handle -> IO (Either Err Int)
- getNChar :: Handle -> Int -> String -> IO String
- sExpToString :: SExp -> String
Documentation
data IdeModeCommand Source
Constructors
| REPLCompletions String | |
| Interpret String | |
| TypeOf String | |
| CaseSplit Int String | |
| AddClause Int String | |
| AddProofClause Int String | |
| AddMissing Int String | |
| MakeWithBlock Int String | |
| MakeCaseBlock Int String | |
| ProofSearch Bool Int String [String] (Maybe Int) | ^ Recursive?, line, name, hints, depth |
| MakeLemma Int String | |
| LoadFile String (Maybe Int) | |
| DocsFor String WhatDocs | |
| Apropos String | |
| GetOpts | |
| SetOpt Opt Bool | |
| Metavariables Int | ^ the Int is the column count for pretty-printing |
| WhoCalls String | |
| CallsWho String | |
| BrowseNS String | |
| TermNormalise [(Name, Bool)] Term | |
| TermShowImplicits [(Name, Bool)] Term | |
| TermNoImplicits [(Name, Bool)] Term | |
| TermElab [(Name, Bool)] Term | |
| PrintDef String | |
| ErrString Err | |
| ErrPPrint Err | |
| GetIdrisVersion |
Constructors
| SexpList [SExp] | |
| StringAtom String | |
| BoolAtom Bool | |
| IntegerAtom Integer | |
| SymbolAtom String |
Instances
| SExpable Bool Source | |
| SExpable Int Source | |
| SExpable Integer Source | |
| SExpable String Source | |
| SExpable Name Source | |
| SExpable OutputAnnotation Source | |
| SExpable NameOutput Source | |
| SExpable FC Source | |
| SExpable SExp Source | |
| SExpable a => SExpable [a] Source | |
| SExpable a => SExpable (Maybe a) Source | |
| (SExpable a, SExpable b) => SExpable (a, b) Source | |
| (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) Source | |
| (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) Source | |
| (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) => SExpable (a, b, c, d, e) Source |
The version of the IDE mode command set. Increment this when you change it so clients can adapt.
sExpToString :: SExp -> String Source