# HG changeset patch
# User paulson
# Date 1187713661 -7200
# Node ID 7cbaf94aed08c04385288f83e18386955a959e21
# Parent  ab62948281a9627f3f076f87f748b5e961e7b359
"sendback" to PG for one-line proof reconstructions

diff -r ab62948281a9 -r 7cbaf94aed08 src/HOL/Tools/watcher.ML
--- a/src/HOL/Tools/watcher.ML	Tue Aug 21 18:27:14 2007 +0200
+++ b/src/HOL/Tools/watcher.ML	Tue Aug 21 18:27:41 2007 +0200
@@ -218,8 +218,8 @@
 	| check (child::children) =
 	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
 	       val _ = trace ("\nprobfile = " ^ file)
-	       val sgno = number_from_filename file  (*subgoal number*)
-	       val thm_names = List.nth(thm_names_list, sgno-1);
+	       val i = number_from_filename file  (*subgoal number*)
+	       val thm_names = List.nth(thm_names_list, i-1);
 	       val ppid = Posix.ProcEnv.getppid()
 	   in
 	     if pollChild childIn
@@ -227,11 +227,11 @@
 	       let val _ = trace ("\nInput available from child: " ^ file)
 		   val childDone = (case prover of
 		       "vampire" => ResReconstruct.checkVampProofFound
-			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
+			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
 		     | "E" => ResReconstruct.checkEProofFound
-			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
+			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
 		     | "spass" => ResReconstruct.checkSpassProofFound
-			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
+			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
 		     | _ => (trace ("\nBad prover! " ^ prover); true) )
 		in
 		 if childDone (*ATP has reported back (with success OR failure)*)
@@ -355,6 +355,17 @@
       val _ = trace("\nProof:\n" ^ msg)
   in  if !Output.debugging then () else File.rm p;  msg  end;
 
+(*Non-successful outcomes*)
+fun report i s = priority ("Subgoal " ^ Int.toString i ^ ": " ^ s);
+
+(*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*)
+fun report_success i s sgtx = 
+  let val lines = String.tokens (fn c => c = #"\n") s
+  in  if length lines > 1 then report i (s ^ sgtx)  (*multiple commands: do the old way*)
+      else priority (cat_lines ["Subgoal " ^ string_of_int i ^ ":", sgtx,
+                                "  Try this command:", Markup.enclose Markup.sendback s])
+  end;
+
 fun createWatcher (ctxt, th, thm_names_list) =
  let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
      fun decr_watched() =
@@ -370,28 +381,27 @@
                           handle Option => error "watcher: \"outcome\" line is missing"
 	   val probfile = valOf (TextIO.inputLine childin)
                           handle Option => error "watcher: \"probfile\" line is missing"
-	   val sgno = number_from_filename probfile
-	   val text = string_of_subgoal th sgno
-	   fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s);
+	   val i = number_from_filename probfile
+	   val text = "\n" ^ string_of_subgoal th i
        in
 	 Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
 		       "\"\nprobfile = " ^ probfile ^
 		       "\nGoals being watched: "^  Int.toString (!goals_being_watched)));
 	 if String.isPrefix "Invalid" outcome
-	 then (report ("Subgoal is not provable:\n" ^ text);
+	 then (report i ("Subgoal is not provable:" ^ text);
 	       decr_watched())
 	 else if String.isPrefix "Failure" outcome
-	 then (report ("Proof attempt failed:\n" ^ text);
+	 then (report i ("Proof attempt failed:" ^ text);
 	       decr_watched())
 	(* print out a list of rules used from clasimpset*)
 	 else if String.isPrefix "Success" outcome
-	 then (report (read_proof probfile ^ "\n" ^ text);
+	 then (report_success i (read_proof probfile) text;
 	       decr_watched())
 	  (* if proof translation failed *)
 	 else if String.isPrefix "Translation failed" outcome
-	 then (report (outcome ^ text);
+	 then (report i (outcome ^ text);
 	       decr_watched())
-	 else (report "System error in proof handler";
+	 else (report i "System error in proof handler";
 	       decr_watched())
        end
  in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));