diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-03 18:36:10 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-03 18:36:16 +0100 |
| commit | c3b35b153f5f0023934e8d09007a68fd4a2a6b55 (patch) | |
| tree | ec0248109be75287dc764dfce787531b36525b80 /stm/stm.mli | |
| parent | c4f270f573360e39bd91e3ffff8d37775b2871d7 (diff) | |
STM: code refactoring
This is mainly shuffling code around and removing internal
refs that are not needed anymore.
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 2e133f1eb..48e1ca4e4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -72,13 +72,6 @@ val get_current_state : unit -> Stateid.t (* Misc *) val init : unit -> unit -val slave_main_loop : unit -> unit -val slave_init_stdout : unit -> unit -val tacslave_main_loop : unit -> unit -val tacslave_init_stdout : unit -> unit -val queryslave_main_loop : unit -> unit -val queryslave_init_stdout : unit -> unit - val print_ast : Stateid.t -> Xml_datatype.xml (* Filename *) @@ -87,6 +80,12 @@ val set_compilation_hints : string -> unit (* Reorders the task queue putting forward what is in the perspective *) val set_perspective : Stateid.t list -> unit +(** workers **************************************************************** **) + +module ProofTask : AsyncTaskQueue.Task +module TacTask : AsyncTaskQueue.Task +module QueryTask : AsyncTaskQueue.Task + (** read-eval-print loop compatible interface ****************************** **) (* Adds a new line to the document. It replaces the core of Vernac.interp. |