src/HOL/Tools/res_reconstruct.ML
changeset 23833 3fe991a1f805
parent 23519 a4ffa756d8eb
child 24182 a39c5e7de6a7
equal deleted inserted replaced
23832:09ee9527ffce 23833:3fe991a1f805
    31               else ();
    31               else ();
    32 
    32 
    33 (*Full proof reconstruction wanted*)
    33 (*Full proof reconstruction wanted*)
    34 val full = ref true;
    34 val full = ref true;
    35 
    35 
    36 val recon_sorts = ref false;
    36 val recon_sorts = ref true;
    37 
    37 
    38 val modulus = ref 1;    (*keep every nth proof line*)
    38 val modulus = ref 1;    (*keep every nth proof line*)
    39 
    39 
    40 (**** PARSING OF TSTP FORMAT ****)
    40 (**** PARSING OF TSTP FORMAT ****)
    41 
    41 
   510     (*We write the proof to a file because sending very long lines may fail...*)
   510     (*We write the proof to a file because sending very long lines may fail...*)
   511     File.write (txt_path probfile) msg;
   511     File.write (txt_path probfile) msg;
   512     TextIO.output (toParent, "Success.\n");
   512     TextIO.output (toParent, "Success.\n");
   513     TextIO.output (toParent, probfile ^ "\n");
   513     TextIO.output (toParent, probfile ^ "\n");
   514     TextIO.flushOut toParent;
   514     TextIO.flushOut toParent;
   515     Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
   515     Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
       
   516     (*Give the parent time to respond before possibly sending another signal*)
       
   517     OS.Process.sleep (Time.fromMilliseconds 600)
   516   end;
   518   end;
   517 
   519 
   518 fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
   520 fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
   519   let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
   521   let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
   520   in
   522   in