Idris.Interaction.Command

Documentation

data IdrisCommand

Supported sub-commands for Idris 2.

Constructors

Load

TypeOf

Help

Instances

Eq IdrisCommand

Defined in Idris.Interaction.Command

Methods

(==) :: IdrisCommand -> IdrisCommand -> Bool

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

Show IdrisCommand

Defined in Idris.Interaction.Command

Methods

showsPrec :: Int -> IdrisCommand -> ShowS

show :: IdrisCommand -> String

showList :: [IdrisCommand] -> ShowS

Generic IdrisCommand

Defined in Idris.Interaction.Command

Associated Types

type Rep IdrisCommand :: Type -> Type

Methods

from :: IdrisCommand -> Rep IdrisCommand x

to :: Rep IdrisCommand x -> IdrisCommand

type Rep IdrisCommand

Defined in Idris.Interaction.Command

type Rep IdrisCommand = D1 ('MetaData "IdrisCommand" "Idris.Interaction.Command" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "Load" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TypeOf" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Help" 'PrefixI 'False) (U1 :: Type -> Type)))

supportedCommands :: HashMap ByteString IdrisCommand

Map of supported Idris 2 sub-commands. We use it instead of parser.

matchSupported :: ByteString -> Maybe IdrisCommand

Check user input to identify IdrisCommand.

chooseCommand :: ExternalInterpreterSettings -> InterpreterRequest -> Either () IdrisCommand -> ByteString -> IO (IO (ExitCode, String, String))

Choose an action based on either IdrisCommand or raw input.

textResponse :: String -> IO (ExitCode, String, String)

Helper to wrap given text as stdout.

withResource :: ExternalInterpreterSettings -> InterpreterRequest -> (FilePath -> IO (ExitCode, String, String)) -> IO (IO (ExitCode, String, String))

Wrapper around temp directory that will try to identify whether associated file exists. And if file exists given action will be performed.

runProcess :: ExternalInterpreterSettings -> String -> FilePath -> IO (ExitCode, String, String)

Wrapper around CLI execution.

validateCmd :: ByteString -> ByteString

We are trying to filter out some potentially dangerous operations such as :x.