From 61209f27eb26dcb04a7d5428b9f2ab7f65f73ac8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 26 Nov 2014 18:42:40 +0100 Subject: STM: put hooks in key events to let plugins customize the feedback The default hook value is the one used by CoqIDE --- stm/stm.mli | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) (limited to 'stm/stm.mli') diff --git a/stm/stm.mli b/stm/stm.mli index 48e1ca4e4..88fdf316d 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -17,7 +17,8 @@ open Feedback The [ontop] parameter is just for asserting the GUI is on sync, but will eventually call edit_at on the fly if needed. The sentence [s] is parsed in the state [ontop]. - If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) + If [newtip] is provided, then the returned state id is guaranteed to be + [newtip] *) val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) -> bool -> edit_id -> string -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] @@ -86,6 +87,29 @@ module ProofTask : AsyncTaskQueue.Task module TacTask : AsyncTaskQueue.Task module QueryTask : AsyncTaskQueue.Task +(** customization ********************************************************** **) + +(* From the master (or worker, but beware that to install the hook + * into a worker one has to build the wroker toplevel to do so and + * the alternative toploop for the worker can be selected by changing + * the name of the Task(s) above) *) + +val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t +val parse_error_hook : + (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t +val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t + +(* Messages from the workers to the master *) +val forward_feedback_hook : + (Stateid.t -> Feedback.route_id -> Feedback.feedback_content -> unit) Hook.t + +type state = { + system : States.state; + proof : Proof_global.state; + shallow : bool +} +val state_of_id : Stateid.t -> state option + (** read-eval-print loop compatible interface ****************************** **) (* Adds a new line to the document. It replaces the core of Vernac.interp. -- cgit v1.2.3