From 28d45c2413ad24c758fca5cfb00ec4ba20935f39 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 23 Nov 2017 11:38:55 +0100
Subject: 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.
---
 intf/vernacexpr.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index c7a9db1cbc..a90e5501a5 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -315,13 +315,8 @@ type cumulative_inductive_parsing_flag =
 (** {6 The type of vernacular expressions} *)
 
 type vernac_expr =
-  (* Control *)
-  | VernacLoad of verbose_flag * string
-  | VernacTime of vernac_expr located
-  | VernacRedirect of string * vernac_expr located
-  | VernacTimeout of int * vernac_expr
-  | VernacFail of vernac_expr
 
+  | VernacLoad of verbose_flag * string
   (* Syntax *)
   | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of bool * scope_name
@@ -482,6 +477,14 @@ and vernac_argument_status = {
   implicit_status : vernac_implicit_status;
 }
 
+type vernac_control =
+  | VernacExpr of vernac_expr
+   (* Control *)
+  | VernacTime of vernac_control located
+  | VernacRedirect of string * vernac_control located
+  | VernacTimeout of int * vernac_control
+  | VernacFail of vernac_control
+
 (* A vernac classifier provides information about the exectuion of a
    command:
 
-- 
cgit v1.2.3