Remove the syntax [Vernac1. Vernac2. … Vernacn. ].

It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being.

The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ].

I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr.

6 files changed, 29 insertions, 21 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 335e04b91..3ffaca113 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -265,9 +265,8 @@ type module_binder = bool option * lident list * module_ast_inl
 
 type vernac_expr =
   (* Control *)
-  | VernacList of located_vernac_expr list
   | VernacLoad of verbose_flag * string
-  | VernacTime of vernac_expr
+  | VernacTime of vernac_list
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
   | VernacError of exn (* always fails *)
@@ -431,6 +430,8 @@ type vernac_expr =
   | VernacPolymorphic of bool * vernac_expr
   | VernacLocal of bool * vernac_expr
 
+and vernac_list = located_vernac_expr list
+
 and located_vernac_expr = Loc.t * vernac_expr
 
 (* A vernac classifier has to tell if a command:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 05e654925..3c3caa140 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -69,7 +69,7 @@ let default_command_entry =
 GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
-    [ [ IDENT "Time"; v = vernac -> VernacTime v
+    [ [ IDENT "Time"; l = vernac_list -> VernacTime l
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
       | IDENT "Fail"; v = vernac -> VernacFail v
 
@@ -104,10 +104,12 @@ GEXTEND Gram
       | g = gallina_ext; "." -> g
       | c = command; "." -> c
       | c = syntax; "." -> c
-      | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
       | c = subprf -> c
     ] ]
   ;
+  vernac_list:
+    [ [ c = located_vernac -> [c] ] ]
+  ;
   vernac_aux: LAST
     [ [ prfcom = default_command_entry -> prfcom ] ]
   ;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 6d7e3c38d..16759a3d8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -531,13 +531,9 @@ let rec pr_vernac = function
   | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s
 
   (* Control *)
-  | VernacList l ->
-      hov 2 (str"[" ++ spc() ++
-             prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l
-             ++ spc() ++ str"]")
   | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
   ++ spc()) else spc()  ++ qs s
-  | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
+  | VernacTime v -> str"Time" ++ spc() ++ pr_vernac_list v
   | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v
   | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v
   | VernacError _ -> str"No-parsing-rule for VernacError"
@@ -959,6 +955,11 @@ let rec pr_vernac = function
   | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i
   | VernacEndSubproof -> str "}"
 
+and pr_vernac_list l =
+      hov 2 (str"[" ++ spc() ++
+             prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l
+             ++ spc() ++ str"]")
+
 and pr_extend s cl =
   let pr_arg a =
     try pr_gen a
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 8ba01a7b2..05c8fdd0d 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -56,7 +56,7 @@ let undo_classifier = ref (fun _ -> assert false)
 let set_undo_classifier f = undo_classifier := f
 
 let rec classify_vernac e =
-  let static_classifier e = match e with
+  let rec static_classifier e = match e with
     (* PG compatibility *)
     | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
     | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
@@ -77,7 +77,7 @@ let rec classify_vernac e =
 	make_polymorphic (classify_vernac e)
       else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime e -> classify_vernac e
+    | VernacTime e -> classify_vernac_list e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep | VtSideff _
@@ -157,7 +157,6 @@ let rec classify_vernac e =
     | VernacRegister _
     | VernacComments _ -> VtSideff [], VtLater
     (* Who knows *)
-    | VernacList _
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
     | VernacEndSegment _ -> VtSideff [], VtNow
@@ -193,6 +192,13 @@ let rec classify_vernac e =
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
         with Not_found -> anomaly(str"No classifier for"++spc()++str s)
+  and classify_vernac_list = function
+    (* spiwack: It would be better to define a monoid on classifiers.
+       So that the classifier of the list would be the composition of
+       the classifier of the individual commands. Currently: special
+       case for singleton lists.*)
+    | [_,c] -> static_classifier c
+    | l -> VtUnknown,VtNow
   in
   let res = static_classifier e in
     if Flags.is_universe_polymorphism () then
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e887204c3..76d2b89c6 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,12 +27,13 @@ let rec is_navigation_vernac = function
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacTime c -> is_navigation_vernac c (* Time Back* is harmless *)
+  | VernacTime l ->
+    List.exists
+      (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
 
 and is_deep_navigation_vernac = function
   | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
-  | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
   | _ -> false
 
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
@@ -234,9 +235,6 @@ let rec vernac_com verbosely checknav (loc,com) =
 	    raise reraise
 	end
 
-    | VernacList l ->
-        List.iter (fun (_,v) -> interp v) l
-
     | v when !just_parsing -> ()
 
     | v -> Stm.interp verbosely (loc,v)
@@ -245,7 +243,7 @@ let rec vernac_com verbosely checknav (loc,com) =
       checknav loc com;
       if do_beautify () then pr_new_syntax loc (Some com);
       if !Flags.time then display_cmd_header loc com;
-      let com = if !Flags.time then VernacTime com else com in
+      let com = if !Flags.time then VernacTime [loc,com] else com in
       interp com
     with reraise ->
       let reraise = Errors.push reraise in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0dbc77b83..5864c54b6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1669,7 +1669,6 @@ let interp ?proof locality poly c =
   prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
   match c with
   (* Done later in this file *)
-  | VernacList _ -> assert false
   | VernacLoad _ -> assert false
   | VernacFail _ -> assert false
   | VernacTime _ -> assert false
@@ -1960,11 +1959,10 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         aux ?locality ?polymorphism isprogcmd v
     | VernacTime v ->
 	let tstart = System.get_time() in
-        aux ?locality ?polymorphism isprogcmd v;
+        aux_list ?locality ?polymorphism isprogcmd v;
 	let tend = System.get_time() in
 	let msg = if !Flags.time then "" else "Finished transaction in " in
         msg_info (str msg ++ System.fmt_time_difference tstart tend)
-    | VernacList l -> List.iter (aux false) (List.map snd l)
     | VernacLoad (_,fname) -> vernac_load (aux false) fname
     | c -> 
         check_vernac_supports_locality c locality;
@@ -1991,6 +1989,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             restore_timeout psh;
             Flags.program_mode := orig_program_mode;
             raise e
+  and aux_list ?locality ?polymorphism isprogcmd l =
+    List.iter (aux false) (List.map snd l)
   in
     if verbosely then Flags.verbosely (aux false) c
     else aux false c