Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Remove Takusen, deal with bug in 7.4

Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
  • Loading branch information...
commit 2062d1355cbc1cc4161e476ceb5337659a1bc6f9 1 parent ec43fb5
Edward Z. Yang authored
Showing with 18 additions and 15 deletions.
  1. +11 −12 ClassicalFOLFFI.hs
  2. +1 −0  CoqTop.hs
  3. +4 −1 haskell.c
  4. +2 −2 logitext.cabal
23 ClassicalFOLFFI.hs
View
@@ -10,9 +10,10 @@ import qualified Data.ByteString.Lazy as L
import Foreign.Marshal.Utils
import Foreign
import Foreign.C.String
-import Foreign.C.UTF8 -- XXX Ughh, why is this in Takusen
import Control.Exception
+import Control.Monad
import System.IO
+import qualified Data.ByteString.UTF8 as U
import GHC.Conc
data UrwebContext
@@ -20,24 +21,22 @@ data UrwebContext
catchToNull m =
m `catch` (\(e :: SomeException) -> hPutStrLn stderr (show e) >> return nullPtr)
+-- incoming string doesn't have to be Haskell managed
+-- outgoing string is on Urweb allocated memory, and
+-- is the unique outgoing one
+wrapper f = \ctx cs -> catchToNull (peekUTF8String cs >>= startString >>= lazyByteStringToUrWebCString ctx)
+
initFFI :: IO ()
initFFI = evaluate theCoq >> return ()
startFFI :: Ptr UrwebContext -> CString -> IO CString
-startFFI ctx cs = catchToNull $ do
- s <- peekUTF8String cs
- r <- startString s
- lazyByteStringToUrWebCString ctx r
+startFFI = wrapper startString
parseUniverseFFI :: Ptr UrwebContext -> CString -> IO CString
-parseUniverseFFI ctx cs = catchToNull $ do
- s <- peekUTF8String cs
- r <- parseUniverseString s
- lazyByteStringToUrWebCString ctx r
+parseUniverseFFI = wrapper parseUniverseString
+
+peekUTF8String = liftM U.toString . S.packCString
--- incoming string doesn't have to be Haskell managed
--- outgoing string is on Urweb allocated memory, and
--- is the unique outgoing one
refineFFI :: Ptr UrwebContext -> CString -> IO CString
refineFFI ctx s = catchToNull $ do
-- bs must not escape from this function
1  CoqTop.hs
View
@@ -31,6 +31,7 @@ coqtopProcess theory err = CreateProcess
, std_out = CreatePipe
, std_err = UseHandle err
, close_fds = False
+ , create_group = False
}
onlyOnce :: IO () -> IO (IO ())
5 haskell.c
View
@@ -16,7 +16,10 @@ uw_Basis_string uw_Haskell_parseUniverse(uw_context ctx, uw_Basis_string i) {
}
uw_Basis_unit uw_Haskell_init(uw_context ctx) {
- hs_init(NULL, NULL);
+ int my_argc = 1;
+ char *my_argv[] = { "<unknown>", NULL };
+ char **my_argv2 = (char**)my_argv; // silly types...
+ hs_init(&my_argc, &my_argv2);
// XXX big ugly hack. If you remove it the event manager crashes
// for some odd reason
ensureIOManagerIsRunning();
4 logitext.cabal
View
@@ -52,7 +52,7 @@ Library
split >= 0.1,
xml >= 1.3,
base >= 3,
- process >= 1.0,
+ process >= 1.1,
bytestring >= 0.9,
transformers >= 0.2,
parsec >= 3.1,
@@ -64,7 +64,7 @@ Library
text >= 0.11,
syb >= 0.3,
mtl >= 2.0,
- Takusen >= 0.8
+ utf8-string >= 0.3
-- Modules not exported by this package.
-- Other-modules:
Please sign in to comment.
Something went wrong with that request. Please try again.