src/HOL/Tools/watcher.ML
author paulson
Fri Aug 24 14:16:44 2007 +0200 (2007-08-24)
changeset 24425 ca97c6f3d9cd
parent 24386 7cbaf94aed08
child 24584 01e83ffa6c54
permissions -rw-r--r--
Returning both a "one-line" proof and a structured proof
paulson@23519
     1
(*  Title:      Watcher.ML
paulson@23519
     2
    ID:         $Id$
paulson@23519
     3
    Author:     Claire Quigley
paulson@23519
     4
    Copyright   2004  University of Cambridge
paulson@23519
     5
 *)
paulson@23519
     6
paulson@23519
     7
(*  The watcher process starts a resolution process when it receives a     *)
paulson@23519
     8
(*  message from Isabelle                                                  *)
paulson@23519
     9
(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
paulson@23519
    10
(*  and removes dead processes.  Also possible to kill all the resolution  *)
paulson@23519
    11
(*  processes currently running.                                           *)
paulson@23519
    12
paulson@23519
    13
signature WATCHER =
paulson@23519
    14
sig
paulson@23519
    15
paulson@23519
    16
(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
paulson@23519
    17
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
paulson@23519
    18
paulson@23519
    19
val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
paulson@23519
    20
paulson@23519
    21
(* Send message to watcher to kill resolution provers *)
paulson@23519
    22
val callSlayer : TextIO.outstream -> unit
paulson@23519
    23
paulson@23519
    24
(* Start a watcher and set up signal handlers*)
paulson@23519
    25
val createWatcher : 
paulson@23519
    26
	Proof.context * thm * string Vector.vector list ->
paulson@23519
    27
	TextIO.instream * TextIO.outstream * Posix.Process.pid
paulson@23519
    28
val killWatcher : Posix.Process.pid -> unit
paulson@23519
    29
val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
paulson@23519
    30
val command_sep : char
paulson@23519
    31
val setting_sep : char
paulson@23519
    32
val reapAll : unit -> unit
paulson@23519
    33
end
paulson@23519
    34
paulson@23519
    35
paulson@23519
    36
paulson@23519
    37
structure Watcher: WATCHER =
paulson@23519
    38
struct
paulson@23519
    39
paulson@23519
    40
(*Field separators, used to pack items onto a text line*)
paulson@23519
    41
val command_sep = #"\t"
paulson@23519
    42
and setting_sep = #"%";
paulson@23519
    43
paulson@23519
    44
val goals_being_watched = ref 0;
paulson@23519
    45
paulson@23519
    46
val trace_path = Path.basic "watcher_trace";
paulson@23519
    47
paulson@23519
    48
fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
paulson@23519
    49
              else ();
paulson@23519
    50
paulson@23519
    51
(*Representation of a watcher process*)
paulson@23519
    52
type proc = {pid : Posix.Process.pid,
paulson@23519
    53
             instr : TextIO.instream,
paulson@23519
    54
             outstr : TextIO.outstream};
paulson@23519
    55
paulson@23519
    56
(*Representation of a child (ATP) process*)
paulson@23519
    57
type cmdproc = {
paulson@23519
    58
        prover: string,       (* Name of the resolution prover used, e.g. "spass"*)
paulson@23519
    59
        file:  string,        (* The file containing the goal for the ATP to prove *)
paulson@23519
    60
        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
paulson@23519
    61
        instr : TextIO.instream,     (*Output of the child process *)
paulson@23519
    62
        outstr : TextIO.outstream};  (*Input to the child process *)
paulson@23519
    63
paulson@23519
    64
paulson@23519
    65
fun fdReader (name : string, fd : Posix.IO.file_desc) =
paulson@23519
    66
	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
paulson@23519
    67
paulson@23519
    68
fun fdWriter (name, fd) =
paulson@23519
    69
          Posix.IO.mkTextWriter {
paulson@23519
    70
	      appendMode = false,
paulson@23519
    71
              initBlkMode = true,
paulson@23519
    72
              name = name,
paulson@23519
    73
              chunkSize=4096,
paulson@23519
    74
              fd = fd};
paulson@23519
    75
paulson@23519
    76
fun openOutFD (name, fd) =
paulson@23519
    77
	  TextIO.mkOutstream (
paulson@23519
    78
	    TextIO.StreamIO.mkOutstream (
paulson@23519
    79
	      fdWriter (name, fd), IO.BLOCK_BUF));
paulson@23519
    80
paulson@23519
    81
fun openInFD (name, fd) =
paulson@23519
    82
	  TextIO.mkInstream (
paulson@23519
    83
	    TextIO.StreamIO.mkInstream (
paulson@23519
    84
	      fdReader (name, fd), ""));
paulson@23519
    85
paulson@23519
    86
paulson@23519
    87
(*  Send request to Watcher for a vampire to be called for filename in arg*)
paulson@23519
    88
fun callResProver (toWatcherStr,  arg) =
paulson@23519
    89
      (TextIO.output (toWatcherStr, arg^"\n");
paulson@23519
    90
       TextIO.flushOut toWatcherStr)
paulson@23519
    91
paulson@23519
    92
(*  Send request to Watcher for multiple provers to be called*)
paulson@23519
    93
fun callResProvers (toWatcherStr,  []) =
paulson@23519
    94
      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
paulson@23519
    95
  | callResProvers (toWatcherStr,
paulson@23519
    96
                    (prover,proverCmd,settings,probfile)  ::  args) =
paulson@23519
    97
      (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
paulson@23519
    98
       (*Uses a special character to separate items sent to watcher*)
paulson@23519
    99
       TextIO.output (toWatcherStr,
paulson@23519
   100
          space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
paulson@23519
   101
       inc goals_being_watched;
paulson@23519
   102
       TextIO.flushOut toWatcherStr;
paulson@23519
   103
       callResProvers (toWatcherStr,args))
paulson@23519
   104
paulson@23519
   105
paulson@23519
   106
(*Send message to watcher to kill currently running vampires. NOT USED and possibly
paulson@23519
   107
  buggy. Note that killWatcher kills the entire process group anyway.*)
paulson@23519
   108
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
paulson@23519
   109
                            TextIO.flushOut toWatcherStr)
paulson@23519
   110
paulson@23519
   111
paulson@23519
   112
(* Get commands from Isabelle*)
paulson@23519
   113
fun getCmds (toParentStr, fromParentStr, cmdList) =
paulson@23519
   114
  let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
paulson@23519
   115
  in
paulson@23519
   116
     trace("\nGot command from parent: " ^ thisLine);
paulson@23519
   117
     if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
paulson@23519
   118
     else if thisLine = "Kill children\n"
paulson@23519
   119
     then (TextIO.output (toParentStr,thisLine);
paulson@23519
   120
	   TextIO.flushOut toParentStr;
paulson@23519
   121
	   [("","Kill children",[],"")])
paulson@23519
   122
     else
paulson@23519
   123
       let val [prover,proverCmd,settingstr,probfile,_] =
paulson@23519
   124
                   String.tokens (fn c => c = command_sep) thisLine
paulson@23519
   125
           val settings = String.tokens (fn c => c = setting_sep) settingstr
paulson@23519
   126
       in
paulson@23519
   127
           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
paulson@23519
   128
                  "\n  problem file: " ^ probfile);
paulson@23519
   129
           getCmds (toParentStr, fromParentStr,
paulson@23519
   130
                    (prover, proverCmd, settings, probfile)::cmdList)
paulson@23519
   131
       end
paulson@23519
   132
       handle Bind =>
paulson@23519
   133
          (trace "\ngetCmds: command parsing failed!";
paulson@23519
   134
           getCmds (toParentStr, fromParentStr, cmdList))
paulson@23519
   135
  end
paulson@23519
   136
	
paulson@23519
   137
paulson@23519
   138
(*Get Io-descriptor for polling of an input stream*)
paulson@23519
   139
fun getInIoDesc someInstr =
paulson@23519
   140
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
paulson@23519
   141
        val _ = TextIO.output (TextIO.stdOut, buf)
paulson@23519
   142
        val ioDesc =
paulson@23519
   143
	    case rd
paulson@23519
   144
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
paulson@23519
   145
	       | _ => NONE
paulson@23519
   146
     in (* since getting the reader will have terminated the stream, we need
paulson@23519
   147
	 * to build a new stream. *)
paulson@23519
   148
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
paulson@23519
   149
	ioDesc
paulson@23519
   150
    end
paulson@23519
   151
paulson@23519
   152
fun pollChild fromStr =
paulson@23519
   153
   case getInIoDesc fromStr of
paulson@23519
   154
     SOME iod =>
paulson@23519
   155
       (case OS.IO.pollDesc iod of
paulson@23519
   156
	  SOME pd =>
paulson@23519
   157
	      let val pd' = OS.IO.pollIn pd in
paulson@23519
   158
		case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
paulson@23519
   159
		    [] => false
paulson@23519
   160
		  | pd''::_ => OS.IO.isIn pd''
paulson@23519
   161
	      end
paulson@23519
   162
	 | NONE => false)
paulson@23519
   163
   | NONE => false
paulson@23519
   164
paulson@23519
   165
paulson@23519
   166
(*************************************)
paulson@23519
   167
(*  Set up a Watcher Process         *)
paulson@23519
   168
(*************************************)
paulson@23519
   169
paulson@23519
   170
fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
paulson@23519
   171
paulson@23519
   172
val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;
paulson@23519
   173
paulson@23519
   174
fun killWatcher (toParentStr, procList) =
paulson@23519
   175
      (trace "\nWatcher timeout: Killing proof processes";
paulson@23519
   176
       TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
paulson@23519
   177
       TextIO.flushOut toParentStr;
paulson@23519
   178
       killChildren procList;
paulson@23519
   179
       Posix.Process.exit 0w0);
paulson@23519
   180
paulson@23519
   181
(* take an instream and poll its underlying reader for input *)
paulson@23519
   182
fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
paulson@23519
   183
  case OS.IO.pollDesc fromParentIOD of
paulson@23519
   184
     SOME pd =>
paulson@23519
   185
	(case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
paulson@23519
   186
	     [] => NONE
paulson@23519
   187
	   | pd''::_ => if OS.IO.isIn pd''
paulson@23519
   188
			then SOME (getCmds (toParentStr, fromParentStr, []))
paulson@23519
   189
			else NONE)
paulson@23519
   190
  | NONE => NONE;
paulson@23519
   191
paulson@23519
   192
(*get the number of the subgoal from the filename: the last digit string*)
paulson@23519
   193
fun number_from_filename s =
paulson@23519
   194
  let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s 
paulson@23519
   195
  in  valOf (Int.fromString (List.last numbers))  end
paulson@23519
   196
  handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
paulson@23519
   197
                    error ("Watcher could not read subgoal nunber! " ^ s));
paulson@23519
   198
paulson@23519
   199
(*Call ATP.  Settings should be a list of strings  ["-t 300", "-m 100000"],
paulson@23519
   200
  which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
paulson@23519
   201
  Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
paulson@23519
   202
  Vampire will reject the switches.*)
paulson@23519
   203
fun execCmds [] procList = procList
paulson@23519
   204
  | execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
paulson@23519
   205
      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
paulson@23519
   206
          val settings' = List.concat (map (String.tokens Char.isSpace) settings)
paulson@23519
   207
	  val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  =
paulson@23519
   208
	       Unix.execute(proverCmd, settings' @ [file])
paulson@23519
   209
	  val (instr, outstr) = Unix.streamsOf childhandle
paulson@23519
   210
	  val newProcList = {prover=prover, file=file, proc_handle=childhandle,
paulson@23519
   211
			     instr=instr, outstr=outstr} :: procList
paulson@23519
   212
	  val _ = trace ("\nFinished at " ^
paulson@23519
   213
			 Date.toString(Date.fromTimeLocal(Time.now())))
paulson@23519
   214
      in execCmds cmds newProcList end
paulson@23519
   215
paulson@23519
   216
fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
paulson@23519
   217
  let fun check [] = []  (* no children to check *)
paulson@23519
   218
	| check (child::children) =
paulson@23519
   219
	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
paulson@23519
   220
	       val _ = trace ("\nprobfile = " ^ file)
paulson@24386
   221
	       val i = number_from_filename file  (*subgoal number*)
paulson@24386
   222
	       val thm_names = List.nth(thm_names_list, i-1);
paulson@23519
   223
	       val ppid = Posix.ProcEnv.getppid()
paulson@23519
   224
	   in
paulson@23519
   225
	     if pollChild childIn
paulson@23519
   226
	     then (* check here for prover label on child*)
paulson@23519
   227
	       let val _ = trace ("\nInput available from child: " ^ file)
paulson@23519
   228
		   val childDone = (case prover of
paulson@23519
   229
		       "vampire" => ResReconstruct.checkVampProofFound
paulson@24386
   230
			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
paulson@23519
   231
		     | "E" => ResReconstruct.checkEProofFound
paulson@24386
   232
			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
paulson@23519
   233
		     | "spass" => ResReconstruct.checkSpassProofFound
paulson@24386
   234
			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
paulson@23519
   235
		     | _ => (trace ("\nBad prover! " ^ prover); true) )
paulson@23519
   236
		in
paulson@23519
   237
		 if childDone (*ATP has reported back (with success OR failure)*)
paulson@23519
   238
		 then (Unix.reap proc_handle;
paulson@23519
   239
		       if !Output.debugging then () else OS.FileSys.remove file;
paulson@23519
   240
		       check children)
paulson@23519
   241
		 else child :: check children
paulson@23519
   242
	      end
paulson@23519
   243
	    else (trace "\nNo child output";  child :: check children)
paulson@23519
   244
	   end
paulson@23519
   245
  in
paulson@23519
   246
    trace ("\nIn checkChildren, length of queue: " ^  Int.toString(length children));
paulson@23519
   247
    check children
paulson@23519
   248
  end;
paulson@23519
   249
paulson@23519
   250
paulson@23519
   251
fun setupWatcher (ctxt, th, thm_names_list) =
paulson@23519
   252
  let
paulson@23519
   253
    val checkc = checkChildren (ctxt, th, thm_names_list)
paulson@23519
   254
    val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
paulson@23519
   255
    val p2 = Posix.IO.pipe()
paulson@23519
   256
    (****** fork a watcher process and get it set up and going ******)
paulson@23519
   257
    fun startWatcher procList =
paulson@23519
   258
      case  Posix.Process.fork() of
paulson@23519
   259
         SOME pid => pid (* parent - i.e. main Isabelle process *)
paulson@23519
   260
       | NONE =>
paulson@23519
   261
          let            (* child - i.e. watcher  *)
paulson@23519
   262
	    val oldchildin = #infd p1
paulson@23519
   263
	    val fromParent = Posix.FileSys.wordToFD 0w0
paulson@23519
   264
	    val oldchildout = #outfd p2
paulson@23519
   265
	    val toParent = Posix.FileSys.wordToFD 0w1
paulson@23519
   266
	    val fromParentIOD = Posix.FileSys.fdToIOD fromParent
paulson@23519
   267
	    val fromParentStr = openInFD ("_exec_in_parent", fromParent)
paulson@23519
   268
	    val toParentStr = openOutFD ("_exec_out_parent", toParent)
paulson@23519
   269
	    val pid = Posix.ProcEnv.getpid()
paulson@23519
   270
	    val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
paulson@23519
   271
		     (*set process group id: allows killing all children*)
paulson@23519
   272
	    val () = trace "\nsubgoals forked to startWatcher"
paulson@23519
   273
	    val limit = ref 200;  (*don't let watcher run forever*)
paulson@23519
   274
	    (*Watcher Loop : Check running ATP processes for output*)
paulson@23519
   275
	    fun keepWatching procList =
paulson@23519
   276
	      (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
paulson@23519
   277
				"  length(procList) = " ^ Int.toString(length procList));
paulson@23519
   278
	       OS.Process.sleep (Time.fromMilliseconds 100);  limit := !limit - 1;
paulson@23519
   279
	       if !limit < 0 then killWatcher (toParentStr, procList)
paulson@23519
   280
	       else
paulson@23519
   281
	       case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
paulson@23519
   282
		  SOME [(_,"Kill children",_,_)] =>
paulson@23519
   283
		    (trace "\nReceived Kill command";
paulson@23519
   284
		     killChildren procList; keepWatching [])
paulson@23519
   285
		| SOME cmds => (*  deal with commands from Isabelle process *)
paulson@23519
   286
		      let val _ = trace("\nCommands from parent: " ^
paulson@23519
   287
					Int.toString(length cmds))
paulson@23519
   288
			  val newProcList' = checkc toParentStr (execCmds cmds procList)
paulson@23519
   289
		      in trace "\nCommands executed"; keepWatching newProcList' end
paulson@23519
   290
		| NONE => (* No new input from Isabelle *)
paulson@23519
   291
		    (trace "\nNothing from parent...";
paulson@23519
   292
		     keepWatching(checkc toParentStr procList)))
paulson@23519
   293
	     handle exn => (*FIXME: exn handler is too general!*)
paulson@23519
   294
	       (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
paulson@23519
   295
		keepWatching procList);
paulson@23519
   296
	  in
paulson@23519
   297
	    (*** Sort out pipes ********)
paulson@23519
   298
	    Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
paulson@23519
   299
	    Posix.IO.dup2{old = oldchildin, new = fromParent};
paulson@23519
   300
	    Posix.IO.close oldchildin;
paulson@23519
   301
	    Posix.IO.dup2{old = oldchildout, new = toParent};
paulson@23519
   302
	    Posix.IO.close oldchildout;
paulson@23519
   303
	    keepWatching (procList)
paulson@23519
   304
	  end;
paulson@23519
   305
paulson@23519
   306
    val _ = TextIO.flushOut TextIO.stdOut
paulson@23519
   307
    val pid = startWatcher []
paulson@23519
   308
    (* communication streams to watcher*)
paulson@23519
   309
    val instr = openInFD ("_exec_in", #infd p2)
paulson@23519
   310
    val outstr = openOutFD ("_exec_out", #outfd p1)
paulson@23519
   311
  in
paulson@23519
   312
   (* close the child-side fds*)
paulson@23519
   313
    Posix.IO.close (#outfd p2);  Posix.IO.close (#infd p1);
paulson@23519
   314
    (* set the fds close on exec *)
paulson@23519
   315
    Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@23519
   316
    Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@23519
   317
    {pid = pid, instr = instr, outstr = outstr}
paulson@23519
   318
  end;
paulson@23519
   319
paulson@23519
   320
paulson@23519
   321
paulson@23519
   322
(**********************************************************)
paulson@23519
   323
(* Start a watcher and set up signal handlers             *)
paulson@23519
   324
(**********************************************************)
paulson@23519
   325
paulson@23519
   326
(*Signal handler to tidy away zombie processes*)
paulson@23519
   327
fun reapAll() =
paulson@23519
   328
     (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
paulson@23519
   329
	  SOME _ => reapAll() | NONE => ())
paulson@23519
   330
     handle OS.SysErr _ => ()
paulson@23519
   331
paulson@23519
   332
(*FIXME: does the main process need something like this?
paulson@23519
   333
    IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
paulson@23519
   334
paulson@23519
   335
fun killWatcher pid =
paulson@23519
   336
  (goals_being_watched := 0;
paulson@23519
   337
   Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
paulson@23519
   338
   reapAll());
paulson@23519
   339
paulson@23519
   340
fun reapWatcher(pid, instr, outstr) = ignore
paulson@23519
   341
  (TextIO.closeIn instr; TextIO.closeOut outstr;
paulson@23519
   342
   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
paulson@23519
   343
  handle OS.SysErr _ => ()
paulson@23519
   344
paulson@23519
   345
fun string_of_subgoal th i =
paulson@23519
   346
    string_of_cterm (List.nth(cprems_of th, i-1))
paulson@23519
   347
    handle Subscript => "Subgoal number out of range!"
paulson@23519
   348
paulson@23519
   349
fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
paulson@23519
   350
paulson@23519
   351
fun read_proof probfile =
paulson@23519
   352
  let val p = ResReconstruct.txt_path probfile
paulson@23519
   353
      val _ = trace("\nReading proof from file " ^ Path.implode p)
paulson@23519
   354
      val msg = File.read p 
paulson@23519
   355
      val _ = trace("\nProof:\n" ^ msg)
paulson@23519
   356
  in  if !Output.debugging then () else File.rm p;  msg  end;
paulson@23519
   357
paulson@24386
   358
(*Non-successful outcomes*)
paulson@24386
   359
fun report i s = priority ("Subgoal " ^ Int.toString i ^ ": " ^ s);
paulson@24386
   360
paulson@24386
   361
(*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*)
paulson@24386
   362
fun report_success i s sgtx = 
paulson@24425
   363
  let val sgline = "Subgoal " ^ string_of_int i ^ ":"
paulson@24425
   364
      val outlines = 
paulson@24425
   365
	case split_lines s of
paulson@24425
   366
	    [] => ["Received bad string: " ^ s]
paulson@24425
   367
	  | line::lines => ["  Try this command:", (*Markup.enclose Markup.sendback*) line, ""]
paulson@24425
   368
	                   @ lines
paulson@24425
   369
  in priority (cat_lines (sgline::sgtx::outlines)) end;
paulson@24425
   370
  
paulson@23519
   371
fun createWatcher (ctxt, th, thm_names_list) =
paulson@23519
   372
 let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
paulson@23519
   373
     fun decr_watched() =
paulson@23519
   374
	  (goals_being_watched := !goals_being_watched - 1;
paulson@23519
   375
	   if !goals_being_watched = 0
paulson@23519
   376
	   then
paulson@23519
   377
	     (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
paulson@23519
   378
	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
paulson@23519
   379
	    else ())
paulson@23519
   380
     fun proofHandler _ =
paulson@23519
   381
       let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
paulson@23519
   382
           val outcome  = valOf (TextIO.inputLine childin)
paulson@23519
   383
                          handle Option => error "watcher: \"outcome\" line is missing"
paulson@23519
   384
	   val probfile = valOf (TextIO.inputLine childin)
paulson@23519
   385
                          handle Option => error "watcher: \"probfile\" line is missing"
paulson@24386
   386
	   val i = number_from_filename probfile
paulson@24386
   387
	   val text = "\n" ^ string_of_subgoal th i
paulson@23519
   388
       in
paulson@23519
   389
	 Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
paulson@23519
   390
		       "\"\nprobfile = " ^ probfile ^
paulson@23519
   391
		       "\nGoals being watched: "^  Int.toString (!goals_being_watched)));
paulson@23519
   392
	 if String.isPrefix "Invalid" outcome
paulson@24386
   393
	 then (report i ("Subgoal is not provable:" ^ text);
paulson@23519
   394
	       decr_watched())
paulson@23519
   395
	 else if String.isPrefix "Failure" outcome
paulson@24386
   396
	 then (report i ("Proof attempt failed:" ^ text);
paulson@23519
   397
	       decr_watched())
paulson@23519
   398
	(* print out a list of rules used from clasimpset*)
paulson@23519
   399
	 else if String.isPrefix "Success" outcome
paulson@24386
   400
	 then (report_success i (read_proof probfile) text;
paulson@23519
   401
	       decr_watched())
paulson@23519
   402
	  (* if proof translation failed *)
paulson@23519
   403
	 else if String.isPrefix "Translation failed" outcome
paulson@24386
   404
	 then (report i (outcome ^ text);
paulson@23519
   405
	       decr_watched())
paulson@24386
   406
	 else (report i "System error in proof handler";
paulson@23519
   407
	       decr_watched())
paulson@23519
   408
       end
paulson@23519
   409
 in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
paulson@23519
   410
    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
paulson@23519
   411
    (childin, childout, childpid)
paulson@23519
   412
  end
paulson@23519
   413
paulson@23519
   414
end (* structure Watcher *)