Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Reinstated plugins

...but for now they'll only work on my machine! I'll try to make this
portable asap...

darcs-hash:20070805212942-974a0-5e6a15ac4d5fd6385c51fb8fc99d8ec65b21b19f.gz
  • Loading branch information...
commit 7c68badf3c2880a8c675c9c9a3439776c6abf1f9 1 parent 6a1ca9d
eb authored
Showing with 5 additions and 7 deletions.
  1. +1 −1  Ivor/Plugin.lhs
  2. +2 −4 Ivor/Shell.lhs
  3. +2 −2 ivor.cabal
View
2  Ivor/Plugin.lhs
@@ -25,7 +25,7 @@
> load :: FilePath -> Context -> IO (Context, Maybe (Parser ViewTerm))
> load fn ctxt = do
-> mv <- Plugins.load fn [] [] "initialise" -- "/home/eb/.ghc/i386-linux-6.4.1/package.conf"] "initialise"
+> mv <- Plugins.load fn [] ["/home/eb/.ghc/i386-linux-6.4.1/package.conf"] "initialise"
> initialise <- case mv of
> LoadFailure msg -> fail $ "Plugin loading failed: " ++ (show msg)
> LoadSuccess _ v -> return v
View
6 Ivor/Shell.lhs
@@ -26,7 +26,7 @@
> import Ivor.Gadgets
> import Ivor.Primitives
> import qualified Ivor.Prefix
-> -- import Ivor.Plugin
+> import Ivor.Plugin
> import IO
> import System
@@ -262,14 +262,12 @@ function which doesn't need to be in the IO Monad.
> process (Failure err) st = return $ respondLn st err
> process (Success (Command (Load f))) st = do importFile f st
> process (Success (Command (Plugin f))) st = do
-> fail "Plugins currently unsupported"
-> {-
> (ctxt, exts) <- load f (context st)
> let st' = st { context = ctxt }
> let st'' = case exts of
> Nothing -> st'
> Just p -> extendParser st' p
-> return st'' -}
+> return st''
> process (Success (Command (Compile f))) st = do compile (context st) f
> putStrLn $ "Output " ++ f ++ ".hs"
> return st
View
4 ivor.cabal
@@ -6,7 +6,7 @@ License-file: LICENSE
Maintainer: eb@dcs.st-and.ac.uk
Homepage: http://www.dcs.st-and.ac.uk/~eb/Ivor/
Stability: experimental
-Build-depends: base, haskell98, parsec, mtl
+Build-depends: base, haskell98, parsec, mtl, plugins
Extensions: MultiParamTypeClasses, FunctionalDependencies,
ExistentialQuantification, OverlappingInstances
Synopsis: Theorem proving library based on dependent type theory
@@ -34,7 +34,7 @@ Category: Theorem provers
Exposed-modules:
Ivor.TT, Ivor.Shell, Ivor.Primitives,
Ivor.TermParser, Ivor.ViewTerm, Ivor.Equality,
- Ivor.Construction
+ Ivor.Plugin, Ivor.Construction
Other-modules: Ivor.Nobby, Ivor.TTCore, Ivor.State,
Ivor.Tactics, Ivor.Typecheck,
Ivor.Gadgets, Ivor.SC, Ivor.Bytecode,
Please sign in to comment.
Something went wrong with that request. Please try again.