License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.IdeMode

Description

Synopsis

parseMessage :: String -> Either Err (SExp, Integer)
convSExp :: SExpable a => String -> a -> Integer -> String
data WhatDocs
- = Overview
- | Full
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
toSExp :: SExpable a => a -> SExp
data SExp
- = SexpList [SExp]
- | StringAtom String
- | BoolAtom Bool
- | IntegerAtom Integer
- | SymbolAtom String
class SExpable a
data Opt
- = ShowImpl
- | ErrContext
ideModeEpoch :: Int
getLen :: Handle -> IO (Either Err Int)
getNChar :: Handle -> Int -> String -> IO String
sExpToString :: SExp -> String

Documentation

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

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

data WhatDocs Source #

Constructors

Overview
Full

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

sexpToCommand :: SExp -> Maybe IdeModeCommand Source #

toSExp :: SExpable a => a -> SExp Source #

data SExp Source #

Constructors

SexpList [SExp]
StringAtom String
BoolAtom Bool
IntegerAtom Integer
SymbolAtom String

Instances

Eq SExp Source #
Instance details Defined in Idris.IdeMode Methods (==) :: SExp -> SExp -> Bool # (/=) :: SExp -> SExp -> Bool #
Show SExp Source #
Instance details Defined in Idris.IdeMode Methods showsPrec :: Int -> SExp -> ShowS # show :: SExp -> String # showList :: [SExp] -> ShowS #
SExpable SExp Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: SExp -> SExp Source #

class SExpable a Source #

Minimal complete definition

toSExp

Instances

SExpable Bool Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: Bool -> SExp Source #
SExpable Int Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: Int -> SExp Source #
SExpable Integer Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: Integer -> SExp Source #
SExpable String Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: String -> SExp Source #
SExpable Name Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: Name -> SExp Source #
SExpable OutputAnnotation Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: OutputAnnotation -> SExp Source #
SExpable NameOutput Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: NameOutput -> SExp Source #
SExpable FC Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: FC -> SExp Source #
SExpable SExp Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: SExp -> SExp Source #
SExpable a => SExpable [a] Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: [a] -> SExp Source #
SExpable a => SExpable (Maybe a) Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: Maybe a -> SExp Source #
(SExpable a, SExpable b) => SExpable (a, b) Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: (a, b) -> SExp Source #
(SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: (a, b, c) -> SExp Source #
(SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: (a, b, c, d) -> SExp Source #
(SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) => SExpable (a, b, c, d, e) Source #
Instance details Defined in Idris.IdeMode Methods toSExp :: (a, b, c, d, e) -> SExp Source #

data Opt Source #

Constructors

ShowImpl
ErrContext

Instances

Show Opt Source #
Instance details Defined in Idris.IdeMode Methods showsPrec :: Int -> Opt -> ShowS # show :: Opt -> String # showList :: [Opt] -> ShowS #

ideModeEpoch :: Int Source #

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

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

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

sExpToString :: SExp -> String Source #