src/HOL/Tools/ATP/watcher.ML
changeset 15702 2677db44c795
parent 15684 5ec4d21889d6
child 15774 9df37a0e935d
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Apr 12 13:38:08 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Apr 13 09:48:41 2005 +0200
     1.3 @@ -19,27 +19,12 @@
     1.4  use "modUnix";*)
     1.5  (*use "/homes/clq20/Jia_Code/TransStartIsar";*)
     1.6  
     1.7 -use "~~/src/HOL/Tools/ATP/VampireCommunication.ML";
     1.8 -use "~~/src/HOL/Tools/ATP/SpassCommunication.ML";
     1.9 -
    1.10 -
    1.11 -use "~~/src/HOL/Tools/ATP/modUnix.ML";
    1.12 -
    1.13  
    1.14  structure Watcher: WATCHER =
    1.15    struct
    1.16  
    1.17 -fun fst (a,b) = a;
    1.18 -fun snd (a,b) = b;
    1.19 -
    1.20  val goals_being_watched = ref 0;
    1.21  
    1.22 -fun remove y [] = []
    1.23 -|   remove y (x::xs) = (if y = x 
    1.24 -                       then 
    1.25 -                           remove y xs 
    1.26 -                       else ((x::(remove y  xs))))
    1.27 -
    1.28  
    1.29  
    1.30  fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
    1.31 @@ -230,7 +215,7 @@
    1.32  
    1.33  fun getInIoDesc someInstr = 
    1.34      let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
    1.35 -        val _ = print (TextIO.stdOut, buf)
    1.36 +        val _ = TextIO.output (TextIO.stdOut, buf)
    1.37          val ioDesc = 
    1.38  	    case rd
    1.39  	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
    1.40 @@ -584,7 +569,7 @@
    1.41                             val childout = snd streams
    1.42                             val childpid = fst mychild
    1.43                             
    1.44 -                           fun vampire_proofHandler (n:int) =
    1.45 +                           fun vampire_proofHandler (n) =
    1.46                             (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.47                             getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )                   
    1.48                            
    1.49 @@ -636,7 +621,7 @@
    1.50                                                        end )
    1.51  *)
    1.52  
    1.53 -fun spass_proofHandler (n:int) = (
    1.54 +fun spass_proofHandler (n) = (
    1.55                                   let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
    1.56                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
    1.57                                        val _ =  TextIO.closeOut outfile
    1.58 @@ -715,8 +700,8 @@
    1.59  
    1.60                          
    1.61                         in 
    1.62 -                          Signal.signal (Posix.Signal.usr1, Signal.SIG_HANDLE vampire_proofHandler);
    1.63 -                          Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE spass_proofHandler);
    1.64 +                          IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
    1.65 +                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
    1.66                            (childin, childout, childpid)
    1.67  
    1.68                         end