diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-23 11:38:55 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-20 16:52:43 +0100 |
| commit | 28d45c2413ad24c758fca5cfb00ec4ba20935f39 (patch) | |
| tree | 50f60424aac3c9e898bb9f9192416c58f44aa7b6 /stm/stm.mli | |
| parent | e2d1c676b23a335b4fb8a528c99dfca2b82a1a39 (diff) | |
Separate vernac controls and regular commands.
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index ef95be0e4..587b75642 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -39,7 +39,7 @@ val new_doc : stm_init_options -> doc * Stateid.t (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> - Vernacexpr.vernac_expr Loc.located + Vernacexpr.vernac_control Loc.located (* Reminder: A parsable [pa] is constructed using [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) @@ -53,7 +53,7 @@ exception End_of_input If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> Vernacexpr.vernac_expr Loc.located -> + bool -> Vernacexpr.vernac_control Loc.located -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* [query at ?report_with cmd] Executes [cmd] at a given state [at], @@ -111,7 +111,7 @@ val get_current_state : doc:doc -> Stateid.t val get_ldir : doc:doc -> Names.DirPath.t (* This returns the node at that position *) -val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option +val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option (* Filename *) val set_compilation_hints : string -> unit @@ -174,7 +174,7 @@ type static_block_declaration = { type document_node = { indentation : int; - ast : Vernacexpr.vernac_expr; + ast : Vernacexpr.vernac_control; id : Stateid.t; } @@ -189,7 +189,7 @@ type static_block_detection = type recovery_action = { base_state : Stateid.t; goals_to_admit : Goal.goal list; - recovery_command : Vernacexpr.vernac_expr option; + recovery_command : Vernacexpr.vernac_control option; } type dynamic_block_error_recovery = |