src/HOL/Tools/ATP/watcher.ML
changeset 16548 aa36ae6b955e
parent 16520 7a9cda53bfa2
child 16561 2bc33f0cfe9a
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Jun 22 19:48:20 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Jun 22 20:26:31 2005 +0200
     1.3 @@ -810,7 +810,7 @@
     1.4                            
     1.5  
     1.6  fun spass_proofHandler (n) = (
     1.7 -                                 let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
     1.8 +                                 let  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
     1.9                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
    1.10                                        val _ =  TextIO.closeOut outfile
    1.11                                        val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
    1.12 @@ -883,25 +883,40 @@
    1.13                                                            else if ((substring (reconstr, 0,5)) = "Proof")
    1.14                                                                 then 
    1.15                                                                     (
    1.16 -                                                                     goals_being_watched := (!goals_being_watched) -1;
    1.17 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.18 -                                                                      Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    1.19 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
    1.20 -                                                                      if (!goals_being_watched = 0)
    1.21 -                                                                      then 
    1.22 +                                                                      goals_being_watched := (!goals_being_watched) -1;
    1.23 +                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.24 +                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    1.25 +                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.26 +                                                                       if (!goals_being_watched = 0)
    1.27 +                                                                       then 
    1.28                                                                            (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
    1.29                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    1.30                                                                                 val _ =  TextIO.closeOut outfile
    1.31 -                                                                           in
    1.32 +                                                                            in
    1.33                                                                                killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
    1.34 -                                                                           end )
    1.35 -                                                                      else
    1.36 -                                                                         ( )
    1.37 +                                                                            end )
    1.38 +                                                                       else
    1.39 +                                                                          ( )
    1.40                                                                        )
    1.41  
    1.42  
    1.43                                                                  else  (* add something here ?*)
    1.44 -                                                                   ()
    1.45 +                                                                   (
    1.46 +                                                                      goals_being_watched := (!goals_being_watched) -1;
    1.47 +                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.48 +                                                                       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
    1.49 +                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.50 +                                                                       if (!goals_being_watched = 0)
    1.51 +                                                                       then 
    1.52 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
    1.53 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    1.54 +                                                                               val _ =  TextIO.closeOut outfile
    1.55 +                                                                            in
    1.56 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
    1.57 +                                                                            end )
    1.58 +                                                                       else
    1.59 +                                                                          ( )
    1.60 +                                                                      )
    1.61                                                                       
    1.62                                                                             
    1.63