# HG changeset patch
# User paulson
# Date 1113378521 -7200
# Node ID 2677db44c795746ada1e687958150390fc933410
# Parent  63f6614f95dcc20ed3eb99c18232359b3963de21
new signalling primmitives for sml/nj compatibility

diff -r 63f6614f95dc -r 2677db44c795 src/HOL/Tools/ATP/recon_order_clauses.ML
--- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 12 13:38:08 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Wed Apr 13 09:48:41 2005 +0200
@@ -1,5 +1,3 @@
-
-
 (*----------------------------------------------*)
 (* Reorder clauses for use in binary resolution *)
 (*----------------------------------------------*)
@@ -7,9 +5,6 @@
 fun drop n [] = []
 |   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
 
-fun remove n [] = []
-|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
-
 fun remove_nth n [] = []
 |   remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
 
diff -r 63f6614f95dc -r 2677db44c795 src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Tue Apr 12 13:38:08 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Wed Apr 13 09:48:41 2005 +0200
@@ -19,27 +19,12 @@
 use "modUnix";*)
 (*use "/homes/clq20/Jia_Code/TransStartIsar";*)
 
-use "~~/src/HOL/Tools/ATP/VampireCommunication.ML";
-use "~~/src/HOL/Tools/ATP/SpassCommunication.ML";
-
-
-use "~~/src/HOL/Tools/ATP/modUnix.ML";
-
 
 structure Watcher: WATCHER =
   struct
 
-fun fst (a,b) = a;
-fun snd (a,b) = b;
-
 val goals_being_watched = ref 0;
 
-fun remove y [] = []
-|   remove y (x::xs) = (if y = x 
-                       then 
-                           remove y xs 
-                       else ((x::(remove y  xs))))
-
 
 
 fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
@@ -230,7 +215,7 @@
 
 fun getInIoDesc someInstr = 
     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
-        val _ = print (TextIO.stdOut, buf)
+        val _ = TextIO.output (TextIO.stdOut, buf)
         val ioDesc = 
 	    case rd
 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
@@ -584,7 +569,7 @@
                            val childout = snd streams
                            val childpid = fst mychild
                            
-                           fun vampire_proofHandler (n:int) =
+                           fun vampire_proofHandler (n) =
                            (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
                            getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )                   
                           
@@ -636,7 +621,7 @@
                                                       end )
 *)
 
-fun spass_proofHandler (n:int) = (
+fun spass_proofHandler (n) = (
                                  let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
                                       val _ = TextIO.output (outfile, ("In signal handler now\n"))
                                       val _ =  TextIO.closeOut outfile
@@ -715,8 +700,8 @@
 
                         
                        in 
-                          Signal.signal (Posix.Signal.usr1, Signal.SIG_HANDLE vampire_proofHandler);
-                          Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE spass_proofHandler);
+                          IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
+                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
                           (childin, childout, childpid)
 
                        end
diff -r 63f6614f95dc -r 2677db44c795 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Apr 12 13:38:08 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Apr 13 09:48:41 2005 +0200
@@ -179,3 +179,14 @@
   val mkTextWriter = mkWriter 
   end;
 end;
+
+(** This extension of the Poly/ML Signal structure is only necessary
+    because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.**)
+
+structure IsaSignal =
+struct
+open Signal
+val usr1 = Posix.Signal.usr1 
+val usr2 = Posix.Signal.usr2 
+end;
+
diff -r 63f6614f95dc -r 2677db44c795 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Tue Apr 12 13:38:08 2005 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Apr 13 09:48:41 2005 +0200
@@ -127,6 +127,35 @@
 
 end;
 
+(** Signal handling: emulation of the Poly/ML Signal structure. Note that types 
+    Posix.Signal.signal and Signals.signal differ **)
+
+structure IsaSignal =
+struct
+
+datatype sig_handle = SIG_DFL | SIG_IGN | SIG_HANDLE of Signals.signal -> unit;
+
+(*From the SML/NJ documentation:
+"HANDLER(f) installs a handler for a signal. When signal is delivered to the process, the execution state of the current thread will be bundled up as a continuation k, then f(signal,n,k) will be called. The number n is the number of times signal has been signalled since the last time f was invoked for it."*)
+
+fun toAction SIG_DFL = Signals.DEFAULT
+  | toAction SIG_IGN = Signals.IGNORE
+  | toAction (SIG_HANDLE iu) = 
+      Signals.HANDLER (fn (signo,_,cont) => (iu signo; cont));
+  
+(*The types are correct, but I'm not sure about the semantics!*)
+fun fromAction Signals.DEFAULT = SIG_DFL
+  | fromAction Signals.IGNORE = SIG_IGN
+  | fromAction (Signals.HANDLER f) = 
+      SIG_HANDLE (fn signo => SMLofNJ.Cont.callcc (fn k => (f (signo,0,k); ())));
+    
+(*Poly/ML version has type  int * sig_handle -> sig_handle*)
+fun signal (signo, sh) = fromAction (Signals.setHandler (signo, toAction sh));
+
+val usr1 = UnixSignals.sigUSR1
+val usr2 = UnixSignals.sigUSR2
+
+end;
 
 
 (** OS related **)