diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-12-18 18:14:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-15 20:45:28 +0100 |
| commit | fa9df2efe5666789bf91bb7761567cd53e6c451f (patch) | |
| tree | dfabeded9b4060114e0f9d7f4d3760efc982ae0c /stm/stm.mli | |
| parent | 0df095ec0715f548180bbff70a6feb673c6726a6 (diff) | |
[stm] Break stm/toplevel dependency loop.
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index b8a2a3859..36341a5d5 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -184,7 +184,6 @@ val register_proof_block_delimiter : 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 val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t (* ready means that master has it at hand *) val state_ready_hook : (Stateid.t -> unit) Hook.t @@ -218,7 +217,3 @@ val show_script : ?proof:Proof_global.closed_proof -> unit -> unit (* Hooks to be set by other Coq components in order to break file cycles *) val process_error_hook : Future.fix_exn Hook.t -val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t -val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t -val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn) |