Idris.IdeMode

Documentation

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

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

data WhatDocs

Constructors

Overview

Full

data IdeModeCommand

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 WhatDocs

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

TermElab [(Name, Bool)] Term

PrintDef String

ErrString Err

ErrPPrint Err

GetIdrisVersion

sexpToCommand :: SExp -> Maybe IdeModeCommand

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

ideModeEpoch :: Int

The version of the IDE mode command set. Increment this when you change it so clients can adapt.

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

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