Idris.IdeSlave

Documentation

parseMessage :: String -> Either Err (SExp, Integer)

convSExp :: SExpable a => String -> a -> Integer -> String

data IdeSlaveCommand

Constructors

REPLCompletions String

Interpret String

TypeOf String

CaseSplit Int String

AddClause Int String

AddProofClause Int String

AddMissing Int String

MakeWithBlock Int String

ProofSearch Bool Int String [String] (Maybe Int)

^ Recursive?, line, name, hints, depth

MakeLemma Int String

LoadFile String (Maybe Int)

DocsFor String

Apropos String

GetOpts

SetOpt Opt Bool

Metavariables Int

^ the Int is the column count for pretty-printing

WhoCalls String

CallsWho String

TermNormalise [(Name, Bool)] Term

TermShowImplicits [(Name, Bool)] Term

TermNoImplicits [(Name, Bool)] Term

sexpToCommand :: SExp -> Maybe IdeSlaveCommand

data SExp

Constructors

SexpList [SExp]

StringAtom String

BoolAtom Bool

IntegerAtom Integer

SymbolAtom String

Instances

Eq SExp

Show SExp

SExpable SExp

class SExpable a where

Methods

toSExp :: a -> SExp

Instances

SExpable Bool

SExpable Int

SExpable Integer

SExpable String

SExpable Name

SExpable OutputAnnotation

SExpable NameOutput

SExpable FC

SExpable SExp

SExpable a => SExpable [a]

SExpable a => SExpable (Maybe a)

(SExpable a, SExpable b) => SExpable (a, b)

(SExpable a, SExpable b, SExpable c) => SExpable (a, b, c)

(SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d)

(SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) => SExpable (a, b, c, d, e)

data Opt

Constructors

ShowImpl

ErrContext

Instances

Show Opt

ideSlaveEpoch :: Int

getLen :: Handle -> IO (Either Err Int)

getNChar :: Handle -> Int -> String -> IO String