Idris.REPL

Documentation

repl

Arguments

:: IState

The initial state

-> [FilePath]

The loaded modules

-> FilePath

The file to edit (with :e)

-> InputT Idris ()

Run the REPL

startServer :: PortID -> IState -> [FilePath] -> Idris ()

Run the REPL server

processNetCmd :: IState -> IState -> Handle -> FilePath -> String -> IO (IState, FilePath)

runClient :: PortID -> String -> IO ()

Run a command on the server on localhost

initIdemodeSocket :: IO Handle

idemodeStart :: Bool -> IState -> [FilePath] -> Idris ()

Run the IdeMode

idemode :: Handle -> IState -> [FilePath] -> Idris ()

runIdeModeCommand

Arguments

:: Handle

^ The handle for communication

-> Integer

^ The continuation ID for the client

-> IState

^ The original IState

-> FilePath

^ The current open file

-> [FilePath]

^ The currently loaded modules

-> IdeModeCommand

^ The command to process

-> Idris ()

Run IDEMode commands

ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

Show a term for IDEMode with the specified implicitness

splitName :: String -> Either String Name

idemodeProcess :: FilePath -> Command -> Idris ()

mkPrompt :: [FilePath] -> [Char]

The prompt consists of the currently loaded modules, or Idris if there are none

lit :: FilePath -> Bool

Determine whether a file uses literate syntax

processInput :: String -> IState -> [FilePath] -> FilePath -> Idris (Maybe [FilePath])

resolveProof :: Name -> Idris Name

removeProof :: Name -> Idris ()

edit :: FilePath -> IState -> Idris ()

proofs :: IState -> Idris ()

insertScript :: String -> [String] -> [String]

process :: FilePath -> Command -> Idris ()

showTotal :: Totality -> IState -> Doc OutputAnnotation

showTotalN :: IState -> Name -> Doc OutputAnnotation

displayHelp :: [Char]

pprintDef :: Name -> Idris [Doc OutputAnnotation]

helphead :: [([[Char]], CmdArg, [Char])]

replSettings :: Maybe FilePath -> Settings Idris

idris :: [Opt] -> IO (Maybe IState)

Invoke as if from command line. It is an error if there are unresolved totality problems.

loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]

idrisMain :: [Opt] -> Idris ()

runMain :: Idris () -> IO ()

execScript :: String -> Idris ()

getIdrisUserDataDir :: Idris FilePath

Get the platform-specific, user-specific Idris dir

getInitScript :: Idris FilePath

Locate the platform-specific location for the init script

initScript :: Idris ()

Run the initialisation script

getFile :: Opt -> Maybe String

getBC :: Opt -> Maybe String

getOutput :: Opt -> Maybe String

getIBCSubDir :: Opt -> Maybe String

getImportDir :: Opt -> Maybe String

getPkgDir :: Opt -> Maybe String

getPkg :: Opt -> Maybe (Bool, String)

getPkgClean :: Opt -> Maybe String

getPkgREPL :: Opt -> Maybe String

getPkgCheck :: Opt -> Maybe String

getPkgMkDoc

Arguments

:: Opt

Opt to extract

-> Maybe String

Result

Returns None if given an Opt which is not PkgMkDoc Otherwise returns Just x, where x is the contents of PkgMkDoc

getPkgTest

Arguments

:: Opt

the option to extract

-> Maybe String

the package file to test

getCodegen :: Opt -> Maybe Codegen

getConsoleWidth :: Opt -> Maybe ConsoleWidth

getExecScript :: Opt -> Maybe String

getPkgIndex :: Opt -> Maybe FilePath

getEvalExpr :: Opt -> Maybe String

getOutputTy :: Opt -> Maybe OutputType

getLanguageExt :: Opt -> Maybe LanguageExt

getTriple :: Opt -> Maybe String

getCPU :: Opt -> Maybe String

getOptLevel :: Opt -> Maybe Int

getOptimisation :: Opt -> Maybe (Idris ())

getColour :: Opt -> Maybe Bool

getClient :: Opt -> Maybe String

getPort :: [Opt] -> PortID

opt :: (Opt -> Maybe a) -> [Opt] -> [a]

ver :: [Char]

defaultPort :: PortID

banner :: [Char]

warranty :: [Char]