src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17583 c272b91b619f
parent 17569 c1143a96f6d7
child 17690 8ba7c3cd24a8
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 22 14:02:14 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 22 14:09:48 2005 +0200
     1.3 @@ -301,9 +301,7 @@
     1.4  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
     1.5  	 TextIO.flushOut toParent;
     1.6  
     1.7 -	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
     1.8 -	(* Attempt to prevent several signals from turning up simultaneously *)
     1.9 -	 Posix.Process.sleep(Time.fromSeconds 1); ()
    1.10 +	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    1.11      end
    1.12      handle exn => (*FIXME: exn handler is too general!*)
    1.13       (File.write(File.tmp_path (Path.basic "proverString_handler")) 
    1.14 @@ -312,9 +310,7 @@
    1.15                       remove_linebreaks proofstr ^ "\n");
    1.16        TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
    1.17        TextIO.flushOut toParent;
    1.18 -      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.19 -      (* Attempt to prevent several signals from turning up simultaneously *)
    1.20 -      Posix.Process.sleep(Time.fromSeconds 1); ());
    1.21 +      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    1.22  
    1.23  val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
    1.24  
    1.25 @@ -383,10 +379,8 @@
    1.26         TextIO.output (toParent, reconstr^"\n");
    1.27         TextIO.output (toParent, goalstring^"\n");
    1.28         TextIO.flushOut toParent;
    1.29 -
    1.30         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.31 -      (* Attempt to prevent several signals from turning up simultaneously *)
    1.32 -       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
    1.33 +       all_tac
    1.34    end
    1.35    handle exn => (*FIXME: exn handler is too general!*)
    1.36     (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
    1.37 @@ -395,9 +389,7 @@
    1.38           (remove_linebreaks proofstr) ^"\n");
    1.39      TextIO.output (toParent, goalstring^"\n");
    1.40      TextIO.flushOut toParent;
    1.41 -    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.42 -    (* Attempt to prevent several signals from turning up simultaneously *)
    1.43 -    Posix.Process.sleep(Time.fromSeconds 1); all_tac)
    1.44 +    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
    1.45  
    1.46  (**********************************************************************************)
    1.47  (* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)
    1.48 @@ -699,10 +691,8 @@
    1.49        val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) 
    1.50  	 ("str is: "^str^" goalstr is: "^goalstring^"\n")	
    1.51        val (frees,recon_steps) = parse_step tokens 
    1.52 -      val isar_str = to_isar_proof (frees, recon_steps, goalstring)
    1.53 -      val foo = File.write (File.tmp_path (Path.basic "apply_res_2")) isar_str
    1.54    in 
    1.55 -     Pretty.writeln(Pretty.str isar_str)
    1.56 +      to_isar_proof (frees, recon_steps, goalstring)
    1.57    end 
    1.58  
    1.59  end;