src/HOL/Tools/ATP/watcher.sig
author quigley
Wed Apr 06 12:01:37 2005 +0200 (2005-04-06 ago)
changeset 15658 2edb384bf61f
parent 15642 028059faa963
child 15782 a1863ea9052b
permissions -rw-r--r--
watcher.ML and watcher.sig changed. Debug files now write to tmp.
     1 
     2 (*  Title:      Watcher.ML
     3     Author:     Claire Quigley
     4     Copyright   2004  University of Cambridge
     5 *)
     6 
     7 (***************************************************************************)
     8 (*  The watcher process starts a Spass process when it receives a        *)
     9 (*  message from Isabelle                                                  *)
    10 (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    11 (*  and removes dead processes.  Also possible to kill all the vampire     *)
    12 (*  processes currently running.                                           *)
    13 (***************************************************************************)
    14 
    15 
    16 signature WATCHER =
    17   sig
    18 
    19 (*****************************************************************************************)
    20 (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    21 (*  callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list             *)
    22 (*****************************************************************************************)
    23 
    24 val callResProvers : TextIO.outstream *(string* string*string *string*string*string) list -> unit
    25 
    26 
    27 
    28 (************************************************************************)
    29 (* Send message to watcher to kill currently running resolution provers *)
    30 (************************************************************************)
    31 
    32 val callSlayer : TextIO.outstream -> unit
    33 
    34 
    35 
    36 (**********************************************************)
    37 (* Start a watcher and set up signal handlers             *)
    38 (**********************************************************)
    39 
    40 val createWatcher : unit -> TextIO.instream * TextIO.outstream * Posix.Process.pid
    41 
    42 
    43 
    44 (**********************************************************)
    45 (* Kill watcher process                                   *)
    46 (**********************************************************)
    47 
    48 val killWatcher : (Posix.Process.pid) -> unit
    49 
    50 
    51 end