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 /vernac/vernacprop.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 'vernac/vernacprop.mli')
| -rw-r--r-- | vernac/vernacprop.mli | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index fbdba6bac..eb7c7055a 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -11,9 +11,16 @@ open Vernacexpr -val is_navigation_vernac : vernac_expr -> bool -val is_deep_navigation_vernac : vernac_expr -> bool -val is_reset : vernac_expr -> bool -val is_query : vernac_expr -> bool -val is_debug : vernac_expr -> bool -val is_undo : vernac_expr -> bool +(* Return the vernacular command below control (Time, Timeout, Redirect, Fail). + Beware that Fail can change many properties of the underlying command, since + a success of Fail means the command was backtracked over. *) +val under_control : vernac_control -> vernac_expr + +val has_Fail : vernac_control -> bool + +val is_navigation_vernac : vernac_control -> bool +val is_deep_navigation_vernac : vernac_control -> bool +val is_reset : vernac_control -> bool +val is_query : vernac_control -> bool +val is_debug : vernac_control -> bool +val is_undo : vernac_control -> bool |