idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.REPL

Synopsis

Documentation

repl Source

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 () Source

Run the REPL server

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

Run a command on the server on localhost

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

Run the IdeMode

runIdeModeCommand Source

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 () Source

Show a term for IDEMode with the specified implicitness

mkPrompt :: [FilePath] -> [Char] Source

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

lit :: FilePath -> Bool Source

Determine whether a file uses literate syntax

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

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

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

runMain :: Idris () -> IO () Source

getIdrisUserDataDir :: Idris FilePath Source

Get the platform-specific, user-specific Idris dir

getInitScript :: Idris FilePath Source

Locate the platform-specific location for the init script

initScript :: Idris () Source

Run the initialisation script

getPkgMkDoc Source

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 Source

Arguments

:: Opt

the option to extract

-> Maybe String

the package file to test

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