# HG changeset patch # User paulson # Date 1138382935 -3600 # Node ID 5629fea8b4c668097d1ed1548772030bd9e911d2 # Parent 303793f49b0f520419df4a281ddaa353af8f33f3 better reporting diff -r 303793f49b0f -r 5629fea8b4c6 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Fri Jan 27 16:05:23 2006 +0100 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Jan 27 18:28:55 2006 +0100 @@ -127,7 +127,7 @@ (prover, proverCmd, settings, probfile)::cmdList) end handle Bind => - (trace "getCmds: command parsing failed!"; + (trace "\ngetCmds: command parsing failed!"; getCmds (toParentStr, fromParentStr, cmdList)) end @@ -353,37 +353,39 @@ (Output.debug ("\nReaping a watcher, childpid = " ^ string_of_pid childpid); killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) ) else ()) - val _ = Output.debug ("subgoals forked to createWatcher: "^ prems_string_of th); - fun proofHandler n = - let val outcome = TextIO.inputLine childin + fun proofHandler _ = + let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid) + val outcome = TextIO.inputLine childin val probfile = TextIO.inputLine childin val sgno = number_from_filename probfile val text = string_of_subgoal th sgno - val _ = Output.debug ("In signal handler. outcome = \"" ^ outcome ^ - "\"\nprobfile = " ^ probfile ^ - "\nGoals being watched: "^ Int.toString (!goals_being_watched)) + fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s); in + Output.debug ("In signal handler. outcome = \"" ^ outcome ^ + "\"\nprobfile = " ^ probfile ^ + "\nGoals being watched: "^ Int.toString (!goals_being_watched)); if String.isPrefix "[" outcome (*indicates a proof reconstruction*) then (priority (Recon_Transfer.apply_res_thm outcome); decr_watched()) else if String.isPrefix "Invalid" outcome - then (priority ("Subgoal is not provable:\n" ^ text); + then (report ("Subgoal is not provable:\n" ^ text); decr_watched()) else if String.isPrefix "Failure" outcome - then (priority ("Proof attempt failed:\n" ^ text); + then (report ("Proof attempt failed:\n" ^ text); decr_watched()) (* print out a list of rules used from clasimpset*) else if String.isPrefix "Success" outcome - then (priority (outcome ^ text); + then (report (outcome ^ text); decr_watched()) (* if proof translation failed *) else if String.isPrefix "Translation failed" outcome - then (priority (outcome ^ text); + then (report (outcome ^ text); decr_watched()) - else (priority "System error in proof handler"; + else (report "System error in proof handler"; decr_watched()) end - in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler); + in Output.debug ("subgoals forked to createWatcher: "^ prems_string_of th); + IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler); (childin, childout, childpid) end