Fixes parsing of all: followed by a typechecking/evaluation command.

Exceptions raised during parsing are caught by the parser and result in weird
parsing behaviour. Instead I added a special case in vernac_expr which always
raises an error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16988 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 6 insertions, 6 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2f76df0e5..8bf65d044 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -263,6 +263,7 @@ type vernac_expr =
   | VernacTime of vernac_expr
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
+  | VernacError of exn (* always fails *)
 
   (* Syntax *)
   | VernacTacticNotation of
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 30c88a11c..81bd6a108 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -138,11 +138,7 @@ GEXTEND Gram
                     | Some (SelectNth g) -> c (Some g)
                     | None -> c None
                     | _ ->
-                        (* arnaud: the error is raised bizarely:
-                           "all:Check 0." doesn't do anything, then
-                           inputing anything that ends with a period
-                           (including " .") raises the error. *)
-                        error "Typing and evaluation commands, cannot be used with the \"all:\" selector."
+                        VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
                   end
       | tac = Tactic.tactic;
         use_dft_tac = [ "." -> false | "..." -> true ] ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5345d40e2..441e362b1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -538,6 +538,7 @@ let rec pr_vernac = function
   | VernacTime v -> str"Time" ++ spc() ++ pr_vernac 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"
 
   (* Syntax *)
   | VernacTacticNotation (n,r,e) ->
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml
index 3c19e887c..139dc67d7 100644
--- a/toplevel/vernac_classifier.ml
+++ b/toplevel/vernac_classifier.ml
@@ -83,7 +83,7 @@ let rec classify_vernac e =
     | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus _
     | VernacSubproof _ | VernacEndSubproof _ 
-    | VernacSolve _ 
+    | VernacSolve _ | VernacError _
     | VernacCheckGuard _
     | VernacUnfocused _
     | VernacSolveExistential _ -> VtProofStep, VtLater
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f3298c29b..7655d3032 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1592,6 +1592,8 @@ let interp ?proof locality c =
   | VernacTimeout _ -> assert false
   | VernacStm _ -> assert false
 
+  | VernacError e -> raise e
+
   (* Syntax *)
   | VernacTacticNotation (n,r,e) ->
       Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e)