better reporting
authorpaulson
Fri Jan 27 18:28:55 2006 +0100 (2006-01-27)
changeset 187965629fea8b4c6
parent 18795 303793f49b0f
child 18797 8559cc115673
better reporting
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Jan 27 16:05:23 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Jan 27 18:28:55 2006 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4                      (prover, proverCmd, settings, probfile)::cmdList) 
     1.5         end
     1.6         handle Bind => 
     1.7 -          (trace "getCmds: command parsing failed!";
     1.8 +          (trace "\ngetCmds: command parsing failed!";
     1.9             getCmds (toParentStr, fromParentStr, cmdList))
    1.10    end
    1.11  	    
    1.12 @@ -353,37 +353,39 @@
    1.13  	     (Output.debug ("\nReaping a watcher, childpid = " ^ string_of_pid childpid);
    1.14  	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
    1.15  	    else ())
    1.16 -     val _ = Output.debug ("subgoals forked to createWatcher: "^ prems_string_of th);
    1.17 -     fun proofHandler n = 
    1.18 -       let val outcome = TextIO.inputLine childin
    1.19 +     fun proofHandler _ = 
    1.20 +       let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
    1.21 +           val outcome = TextIO.inputLine childin
    1.22  	   val probfile = TextIO.inputLine childin
    1.23  	   val sgno = number_from_filename probfile
    1.24  	   val text = string_of_subgoal th sgno
    1.25 -	   val _ = Output.debug ("In signal handler. outcome = \"" ^ outcome ^ 
    1.26 -		        "\"\nprobfile = " ^ probfile ^
    1.27 -		        "\nGoals being watched: "^  Int.toString (!goals_being_watched))
    1.28 +	   fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s);
    1.29         in 
    1.30 +	 Output.debug ("In signal handler. outcome = \"" ^ outcome ^ 
    1.31 +		       "\"\nprobfile = " ^ probfile ^
    1.32 +		       "\nGoals being watched: "^  Int.toString (!goals_being_watched));
    1.33  	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
    1.34  	 then (priority (Recon_Transfer.apply_res_thm outcome);
    1.35  	       decr_watched())
    1.36  	 else if String.isPrefix "Invalid" outcome
    1.37 -	 then (priority ("Subgoal is not provable:\n" ^ text);
    1.38 +	 then (report ("Subgoal is not provable:\n" ^ text);
    1.39  	       decr_watched())
    1.40  	 else if String.isPrefix "Failure" outcome
    1.41 -	 then (priority ("Proof attempt failed:\n" ^ text);
    1.42 +	 then (report ("Proof attempt failed:\n" ^ text);
    1.43  	       decr_watched()) 
    1.44  	(* print out a list of rules used from clasimpset*)
    1.45  	 else if String.isPrefix "Success" outcome
    1.46 -	 then (priority (outcome ^ text);
    1.47 +	 then (report (outcome ^ text);
    1.48  	       decr_watched())
    1.49  	  (* if proof translation failed *)
    1.50  	 else if String.isPrefix "Translation failed" outcome
    1.51 -	 then (priority (outcome ^ text);
    1.52 +	 then (report (outcome ^ text);
    1.53  	       decr_watched())
    1.54 -	 else (priority "System error in proof handler";
    1.55 +	 else (report "System error in proof handler";
    1.56  	       decr_watched())
    1.57         end
    1.58 - in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
    1.59 + in Output.debug ("subgoals forked to createWatcher: "^ prems_string_of th);
    1.60 +    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
    1.61      (childin, childout, childpid)
    1.62    end
    1.63