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

Methods

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

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

Show SExp

Methods

showsPrec :: Int -> SExp -> ShowS

show :: SExp -> String

showList :: [SExp] -> ShowS

SExpable SExp

Methods

toSExp :: SExp -> SExp

class SExpable a where

Minimal complete definition

toSExp

Methods

toSExp :: a -> SExp

Instances

SExpable Bool

Methods

toSExp :: Bool -> SExp

SExpable Int

Methods

toSExp :: Int -> SExp

SExpable Integer

Methods

toSExp :: Integer -> SExp

SExpable String

Methods

toSExp :: String -> SExp

SExpable Name

Methods

toSExp :: Name -> SExp

SExpable OutputAnnotation

Methods

toSExp :: OutputAnnotation -> SExp

SExpable NameOutput

Methods

toSExp :: NameOutput -> SExp

SExpable FC

Methods

toSExp :: FC -> SExp

SExpable SExp

Methods

toSExp :: SExp -> SExp

SExpable a => SExpable [a]

Methods

toSExp :: [a] -> SExp

SExpable a => SExpable (Maybe a)

Methods

toSExp :: Maybe a -> SExp

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

Methods

toSExp :: (a, b) -> SExp

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

Methods

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

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

Methods

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

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

Methods

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

data Opt

Constructors

ShowImpl

ErrContext

Instances

Show Opt

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