Safe Haskell | None |
---|
- repl :: IState -> [FilePath] -> InputT Idris ()
- startServer :: PortID -> IState -> [FilePath] -> Idris ()
- processNetCmd :: IState -> IState -> Handle -> FilePath -> String -> IO (IState, FilePath)
- runClient :: PortID -> String -> IO ()
- initIdeslaveSocket :: IO Handle
- ideslaveStart :: Bool -> IState -> [FilePath] -> Idris ()
- ideslave :: Handle -> IState -> [FilePath] -> Idris ()
- runIdeSlaveCommand :: Handle -> Integer -> IState -> FilePath -> [FilePath] -> IdeSlaveCommand -> Idris ()
- ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
- splitName :: String -> Either String Name
- ideslaveProcess :: FilePath -> Command -> Idris ()
- mkPrompt :: [FilePath] -> [Char]
- lit :: FilePath -> Bool
- processInput :: String -> IState -> [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 -> String
- showTotalN :: IState -> Name -> String
- displayHelp :: [Char]
- pprintDef :: Name -> Idris [Doc OutputAnnotation]
- helphead :: [([[Char]], CmdArg, [Char])]
- replSettings :: Maybe FilePath -> Settings Idris
- idris :: [Opt] -> IO (Maybe IState)
- loadInputs :: [FilePath] -> Maybe Int -> Idris ()
- idrisMain :: [Opt] -> Idris ()
- runMain :: Idris () -> IO ()
- execScript :: String -> Idris ()
- getIdrisUserDataDir :: Idris FilePath
- getInitScript :: Idris FilePath
- initScript :: Idris ()
- 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 :: Opt -> Maybe String
- getPkgTest :: Opt -> Maybe String
- getCodegen :: Opt -> Maybe Codegen
- getExecScript :: Opt -> Maybe String
- 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]
Documentation
Run the REPL
startServer :: PortID -> IState -> [FilePath] -> Idris ()Source
Run the REPL seDver
processNetCmd :: IState -> IState -> Handle -> FilePath -> String -> IO (IState, FilePath)Source
initIdeslaveSocket :: IO HandleSource
ideslaveStart :: Bool -> IState -> [FilePath] -> Idris ()Source
Run the IdeSlave
:: 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 |
-> IdeSlaveCommand | ^ The command to process |
-> Idris () |
Run IDESlave commands
ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()Source
Show a term for IDESlave with the specified implicitness
ideslaveProcess :: FilePath -> Command -> Idris ()Source
mkPrompt :: [FilePath] -> [Char]Source
The prompt consists of the currently loaded modules, or Idris if there are none
processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])Source
resolveProof :: Name -> Idris NameSource
removeProof :: Name -> Idris ()Source
insertScript :: String -> [String] -> [String]Source
showTotalN :: IState -> Name -> StringSource
displayHelp :: [Char]Source
replSettings :: Maybe FilePath -> Settings IdrisSource
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 ()Source
execScript :: String -> Idris ()Source
getIdrisUserDataDir :: Idris FilePathSource
Get the platform-specific, user-specific Idris dir
getInitScript :: Idris FilePathSource
Locate the platform-specific location for the init script
initScript :: Idris ()Source
Run the initialisation script
getIBCSubDir :: Opt -> Maybe StringSource
getImportDir :: Opt -> Maybe StringSource
getPkgClean :: Opt -> Maybe StringSource
getPkgREPL :: Opt -> Maybe StringSource
getPkgCheck :: Opt -> Maybe StringSource
:: 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
:: Opt | the option to extract |
-> Maybe String | the package file to test |
getCodegen :: Opt -> Maybe CodegenSource
getExecScript :: Opt -> Maybe StringSource
getEvalExpr :: Opt -> Maybe StringSource
getOutputTy :: Opt -> Maybe OutputTypeSource
getLanguageExt :: Opt -> Maybe LanguageExtSource
getOptLevel :: Opt -> Maybe IntSource
getOptimisation :: Opt -> Maybe (Idris ())Source