Safe Haskell	None
Language	Haskell98

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

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

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

Run a command on the server on localhost

initIdemodeSocket :: IO Handle Source

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

Run the IdeMode

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

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

splitName :: String -> Either String Name Source

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

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

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

resolveProof :: Name -> Idris Name Source

removeProof :: Name -> Idris () Source

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

proofs :: IState -> Idris () Source

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

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

showTotal :: Totality -> IState -> String Source

showTotalN :: IState -> Name -> String Source

displayHelp :: [Char] Source

pprintDef :: Name -> Idris [Doc OutputAnnotation] Source

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

replSettings :: Maybe FilePath -> Settings Idris Source

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

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

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

idrisMain :: [Opt] -> Idris () Source

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

execScript :: String -> Idris () 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

getFile :: Opt -> Maybe String Source

getBC :: Opt -> Maybe String Source

getOutput :: Opt -> Maybe String Source

getIBCSubDir :: Opt -> Maybe String Source

getImportDir :: Opt -> Maybe String Source

getPkgDir :: Opt -> Maybe String Source

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

getPkgClean :: Opt -> Maybe String Source

getPkgREPL :: Opt -> Maybe String Source

getPkgCheck :: Opt -> Maybe String Source

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

getCodegen :: Opt -> Maybe Codegen Source

getConsoleWidth :: Opt -> Maybe ConsoleWidth Source

getExecScript :: Opt -> Maybe String Source

getPkgIndex :: Opt -> Maybe FilePath Source

getEvalExpr :: Opt -> Maybe String Source

getOutputTy :: Opt -> Maybe OutputType Source

getLanguageExt :: Opt -> Maybe LanguageExt Source

getTriple :: Opt -> Maybe String Source

getCPU :: Opt -> Maybe String Source

getOptLevel :: Opt -> Maybe Int Source

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

getColour :: Opt -> Maybe Bool Source

getClient :: Opt -> Maybe String Source

getPort :: [Opt] -> PortID Source

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

ver :: [Char] Source

defaultPort :: PortID Source

banner :: [Char] Source

warranty :: [Char] Source