Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Full sort information by default.
authorpaulson
Tue, 17 Jul 2007 16:06:13 +0200
changeset 23833 3fe991a1f805
parent 23832 09ee9527ffce
child 23834 ad6ad61332fa
Full sort information by default. Race condition on successful proofs fixed.
src/HOL/Tools/res_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Jul 17 16:05:54 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Jul 17 16:06:13 2007 +0200
@@ -33,7 +33,7 @@
 (*Full proof reconstruction wanted*)
 val full = ref true;
 
-val recon_sorts = ref false;
+val recon_sorts = ref true;
 
 val modulus = ref 1;    (*keep every nth proof line*)
 
@@ -512,7 +512,9 @@
     TextIO.output (toParent, "Success.\n");
     TextIO.output (toParent, probfile ^ "\n");
     TextIO.flushOut toParent;
-    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
+    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+    (*Give the parent time to respond before possibly sending another signal*)
+    OS.Process.sleep (Time.fromMilliseconds 600)
   end;
 
 fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
isabelle