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