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

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

sexpToCommand :: SExp -> Maybe IdeModeCommand

toSExp :: SExpable a => a -> SExp

data SExp

Constructors

SexpList [SExp]

StringAtom String

BoolAtom Bool

IntegerAtom Integer

SymbolAtom String

Instances

Eq SExp

Defined in Idris.IdeMode

Methods

(==) :: SExp -> SExp -> Bool

(/=) :: SExp -> SExp -> Bool

Show SExp

Defined in Idris.IdeMode

Methods

showsPrec :: Int -> SExp -> ShowS

show :: SExp -> String

showList :: [SExp] -> ShowS

SExpable SExp

Defined in Idris.IdeMode

Methods

toSExp :: SExp -> SExp

class SExpable a

Minimal complete definition

toSExp

Instances

SExpable Bool

Defined in Idris.IdeMode

Methods

toSExp :: Bool -> SExp

SExpable Int

Defined in Idris.IdeMode

Methods

toSExp :: Int -> SExp

SExpable Integer

Defined in Idris.IdeMode

Methods

toSExp :: Integer -> SExp

SExpable String

Defined in Idris.IdeMode

Methods

toSExp :: String -> SExp

SExpable Name

Defined in Idris.IdeMode

Methods

toSExp :: Name -> SExp

SExpable OutputAnnotation

Defined in Idris.IdeMode

Methods

toSExp :: OutputAnnotation -> SExp

SExpable NameOutput

Defined in Idris.IdeMode

Methods

toSExp :: NameOutput -> SExp

SExpable FC

Defined in Idris.IdeMode

Methods

toSExp :: FC -> SExp

SExpable SExp

Defined in Idris.IdeMode

Methods

toSExp :: SExp -> SExp

SExpable a => SExpable [a]

Defined in Idris.IdeMode

Methods

toSExp :: [a] -> SExp

SExpable a => SExpable (Maybe a)

Defined in Idris.IdeMode

Methods

toSExp :: Maybe a -> SExp

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

Defined in Idris.IdeMode

Methods

toSExp :: (a, b) -> SExp

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

Defined in Idris.IdeMode

Methods

toSExp :: (a, b, c) -> SExp

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

Defined in Idris.IdeMode

Methods

toSExp :: (a, b, c, d) -> SExp

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

Defined in Idris.IdeMode

Methods

toSExp :: (a, b, c, d, e) -> SExp

data Opt

Constructors

ShowImpl

ErrContext

Instances

Show Opt

Defined in Idris.IdeMode

Methods

showsPrec :: Int -> Opt -> ShowS

show :: Opt -> String

showList :: [Opt] -> ShowS

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

sExpToString :: SExp -> String