isabelle: src/HOL/Tools/ATP/watcher.sig@3d80209e9a53 (annotated)

15789 4cb16144c81b added hearder lines and deleted some redundant material paulson parents: 15782 diff changeset	1	(* ID: $Id$
15642 028059faa963 * empty log message * quigley parents: diff changeset	2	Author: Claire Quigley
028059faa963 * empty log message * quigley parents: diff changeset	3	Copyright 2004 University of Cambridge
028059faa963 * empty log message * quigley parents: diff changeset	4	*)
028059faa963 * empty log message * quigley parents: diff changeset	5
028059faa963 * empty log message * quigley parents: diff changeset	6	(***************************************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	7	(* The watcher process starts a Spass process when it receives a *)
028059faa963 * empty log message * quigley parents: diff changeset	8	(* message from Isabelle *)
028059faa963 * empty log message * quigley parents: diff changeset	9	(* Signals Isabelle, puts output of child into pipe to Isabelle, *)
028059faa963 * empty log message * quigley parents: diff changeset	10	(* and removes dead processes. Also possible to kill all the vampire *)
028059faa963 * empty log message * quigley parents: diff changeset	11	(* processes currently running. *)
028059faa963 * empty log message * quigley parents: diff changeset	12	(***************************************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	13
028059faa963 * empty log message * quigley parents: diff changeset	14
028059faa963 * empty log message * quigley parents: diff changeset	15	signature WATCHER =
15789 4cb16144c81b added hearder lines and deleted some redundant material paulson parents: 15782 diff changeset	16	sig
15642 028059faa963 * empty log message * quigley parents: diff changeset	17
028059faa963 * empty log message * quigley parents: diff changeset	18	(*****************************************************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	19	(* Send request to Watcher for multiple spasses to be called for filenames in arg *)
028059faa963 * empty log message * quigley parents: diff changeset	20	(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
028059faa963 * empty log message * quigley parents: diff changeset	21	(*****************************************************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	22
15782 a1863ea9052b Corrected the problem with the ATP directory. quigley parents: 15658 diff changeset	23	val callResProvers : TextIO.outstream (string stringstring stringstringstringstringstring*string) list -> unit
15642 028059faa963 * empty log message * quigley parents: diff changeset	24
028059faa963 * empty log message * quigley parents: diff changeset	25
028059faa963 * empty log message * quigley parents: diff changeset	26
028059faa963 * empty log message * quigley parents: diff changeset	27	(************************************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	28	(* Send message to watcher to kill currently running resolution provers *)
028059faa963 * empty log message * quigley parents: diff changeset	29	(************************************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	30
028059faa963 * empty log message * quigley parents: diff changeset	31	val callSlayer : TextIO.outstream -> unit
028059faa963 * empty log message * quigley parents: diff changeset	32
028059faa963 * empty log message * quigley parents: diff changeset	33
028059faa963 * empty log message * quigley parents: diff changeset	34
028059faa963 * empty log message * quigley parents: diff changeset	35	(**********************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	36	(* Start a watcher and set up signal handlers *)
028059faa963 * empty log message * quigley parents: diff changeset	37	(**********************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	38
15919 b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file. quigley parents: 15789 diff changeset	39	val createWatcher : Thm.thm(ResClause.clause Thm.thm) Array.array * int -> TextIO.instream * TextIO.outstream * Posix.Process.pid
15642 028059faa963 * empty log message * quigley parents: diff changeset	40
028059faa963 * empty log message * quigley parents: diff changeset	41
028059faa963 * empty log message * quigley parents: diff changeset	42
028059faa963 * empty log message * quigley parents: diff changeset	43	(**********************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	44	(* Kill watcher process *)
028059faa963 * empty log message * quigley parents: diff changeset	45	(**********************************************************)
028059faa963 * empty log message * quigley parents: diff changeset	46
028059faa963 * empty log message * quigley parents: diff changeset	47	val killWatcher : (Posix.Process.pid) -> unit
028059faa963 * empty log message * quigley parents: diff changeset	48
028059faa963 * empty log message * quigley parents: diff changeset	49
028059faa963 * empty log message * quigley parents: diff changeset	50	end

author	wenzelm
	Mon, 29 Aug 2005 16:18:04 +0200
changeset 17184	3d80209e9a53
parent 15919	b30a35432f5a
permissions	-rw-r--r--