ivor-0.1.8: Theorem proving library based on dependent type theory Source code Contents Index

Ivor.Plugin Portability portable Stability experimental Maintainer eb@dcs.st-and.ac.uk

Description

Plugin loader

Synopsis

load :: FilePath -> Context -> IO (Context, Maybe (Parser ViewTerm), Maybe (ShellState -> IO ShellState), Maybe (IO [(String, String -> Context -> IO (String, Context))]))

Documentation

load :: FilePath -> Context -> IO (Context, Maybe (Parser ViewTerm), Maybe (ShellState -> IO ShellState), Maybe (IO [(String, String -> Context -> IO (String, Context))])) Source

Load the given plugin file (which should be a full path to a .o or .hs file) and update the Context. If it is a .hs file, it will be compiled if necessary. Plugins must contain the symbol plugin_context :: Monad m => Context -> m Context which updates the context. It may optionally contain symbols plugin_parser :: Parser ViewTerm which adds new parsing rules, plugin_shell :: ShellState -> IO ShellState which updates the shell plugin_commands :: IO [(String, String -> COntext -> IO (String, Context))] which adds new user defined commands (which may need to do some setting up themselves, hence the IO) Returns the new context and the extra parsing rules and commands, if any.

Produced by Haddock version 2.4.2