Remove VernacError

11 files changed, 75 insertions, 60 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e787e48bf..e20704b7f 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -504,7 +504,6 @@ let rec tmpp v loc =
       xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
                     [tmpp e loc])
   | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
-  | VernacError _ -> xmlWithLoc loc "error" [] []
 
   (* Syntax *)
   | VernacSyntaxExtension (_, ((_, name), sml)) ->
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 25d3c705f..f018d59e6 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -71,7 +71,7 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation*int option
+  | PrintAbout of reference or_by_notation * goal_selector option
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
   | PrintStrategy of reference or_by_notation option
@@ -316,7 +316,6 @@ type vernac_expr =
   | VernacRedirect of string * vernac_expr located
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
-  | VernacError of exn (* always fails *)
 
   (* Syntax *)
   | VernacSyntaxExtension of
@@ -436,11 +435,11 @@ type vernac_expr =
   | VernacRemoveOption of Goptions.option_name * option_ref_value list
   | VernacMemOption of Goptions.option_name * option_ref_value list
   | VernacPrintOption of Goptions.option_name
-  | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr
+  | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr
   | VernacGlobalCheck of constr_expr
   | VernacDeclareReduction of string * Genredexpr.raw_red_expr
   | VernacPrint of printable
-  | VernacSearch of searchable * int option * search_restriction
+  | VernacSearch of searchable * goal_selector option * search_restriction
   | VernacLocate of locatable
   | VernacRegister of lident * register_kind
   | VernacComments of comment list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4fd316119..011565d86 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -40,7 +40,6 @@ let def_body = Gram.entry_create "vernac:def_body"
 let decl_notation = Gram.entry_create "vernac:decl_notation"
 let record_field = Gram.entry_create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
-let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
 let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
@@ -53,7 +52,7 @@ let make_bullet s =
   | _ -> assert false
 
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command;
+  GLOBAL: vernac gallina_ext noedit_mode subprf;
   vernac: FIRST
     [ [ IDENT "Time"; c = located_vernac -> VernacTime c
       | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
@@ -92,7 +91,7 @@ GEXTEND Gram
     [ [ prfcom = command_entry -> prfcom ] ]
   ;
   noedit_mode:
-    [ [ c = subgoal_command -> c None] ]
+    [ [ c = query_command -> c None] ]
   ;
 
   subprf:
@@ -102,15 +101,6 @@ GEXTEND Gram
     ] ]
   ;
 
-  subgoal_command:
-    [ [ c = query_command; "." ->
-                  begin function
-                    | Some (SelectNth g) -> c (Some g)
-                    | None -> c None
-                    | _ ->
-                        VernacError (UserError (None,str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
-                  end ] ]
-  ;
   located_vernac:
     [ [ v = vernac -> !@loc, v ] ]
   ;
@@ -918,29 +908,30 @@ GEXTEND Gram
 	  VernacRemoveOption ([table], v) ]] 
   ;
   query_command: (* TODO: rapprocher Eval et Check *)
-    [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr ->
+    [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." ->
           fun g -> VernacCheckMayEval (Some r, g, c)
-      | IDENT "Compute"; c = lconstr ->
+      | IDENT "Compute"; c = lconstr; "." ->
 	  fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c)
-      | IDENT "Check"; c = lconstr ->
+      | IDENT "Check"; c = lconstr; "." ->
 	 fun g -> VernacCheckMayEval (None, g, c)
       (* Searching the environment *)
-      | IDENT "About"; qid = smart_global ->
+      | IDENT "About"; qid = smart_global; "." ->
 	 fun g -> VernacPrint (PrintAbout (qid,g))
-      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules ->
+      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." ->
 	  fun g -> VernacSearch (SearchHead c,g, l)
-      | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
+      | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
 	  fun g -> VernacSearch (SearchPattern c,g, l)
-      | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
+      | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
 	  fun g -> VernacSearch (SearchRewrite c,g, l)
-      | IDENT "Search"; s = searchabout_query; l = searchabout_queries ->
+      | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." ->
 	  let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m)
       (* compatibility: SearchAbout *)
-      | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries ->
+      | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." ->
 	  fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m)
       (* compatibility: SearchAbout with "[ ... ]" *)
       | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
-	  l = in_or_out_modules -> fun g -> VernacSearch (SearchAbout sl,g, l)
+	l = in_or_out_modules; "." ->
+         fun g -> VernacSearch (SearchAbout sl,g, l)
       ] ]
   ;
   printable:
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ece0adb07..ca5d198c2 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -335,7 +335,7 @@ GEXTEND Gram
     |   IDENT "all"; ":" -> SelectAll ] ]
   ;
   tactic_mode:
-    [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ]
+    [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ]
   ;
   command:
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index cfc2e48d1..5af0e1d9b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -107,7 +107,7 @@ open Decl_kinds
         | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
   let pr_search a gopt b pr_p =
-    pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+    pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
     ++
       match a with
       | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -497,7 +497,7 @@ open Decl_kinds
     | PrintVisibility s ->
       keyword "Print Visibility" ++ pr_opt str s
     | PrintAbout (qid,gopt) ->
-       pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+       pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
        ++ keyword "About" ++ spc()  ++ pr_smart_global qid
     | PrintImplicit qid ->
       keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
@@ -619,8 +619,6 @@ open Decl_kinds
         return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v)
       | VernacFail v ->
         return (keyword "Fail" ++ spc() ++ pr_vernac_body v)
-      | VernacError _ ->
-        return (keyword "No-parsing-rule for VernacError")
 
     (* Syntax *)
       | VernacOpenCloseScope (_,(opening,sc)) ->
@@ -1140,7 +1138,8 @@ open Decl_kinds
                      spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
           | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
         in
-        let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
+        let pr_i = match io with None -> mt ()
+                               | Some i -> Proof_global.pr_goal_selector i ++ str ": " in
         return (pr_i ++ pr_mayeval r c)
       | VernacGlobalCheck c ->
         return (hov 2 (keyword "Type" ++ pr_constrarg c))
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e4cba6f07..61b776f24 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -671,16 +671,18 @@ let _ =
 let default_goal_selector = ref (Vernacexpr.SelectNth 1)
 let get_default_goal_selector () = !default_goal_selector
 
-let print_range_selector (i, j) =
-  if i = j then string_of_int i
-  else string_of_int i ^ "-" ^ string_of_int j
-
-let print_goal_selector = function
-  | Vernacexpr.SelectAll -> "all"
-  | Vernacexpr.SelectNth i -> string_of_int i
-  | Vernacexpr.SelectList l -> "[" ^
-      String.concat ", " (List.map print_range_selector l) ^ "]"
-  | Vernacexpr.SelectId id -> Id.to_string id
+let pr_range_selector (i, j) =
+  if i = j then int i
+  else int i ++ str "-" ++ int j
+
+let pr_goal_selector = function
+  | Vernacexpr.SelectAll -> str "all"
+  | Vernacexpr.SelectNth i -> int i
+  | Vernacexpr.SelectList l ->
+     str "["
+     ++ prlist_with_sep pr_comma pr_range_selector l
+     ++ str "]"
+  | Vernacexpr.SelectId id -> Id.print id
 
 let parse_goal_selector = function
   | "all" -> Vernacexpr.SelectAll
@@ -699,7 +701,10 @@ let _ =
                                   optdepr = false;
                                   optname = "default goal selector" ;
                                   optkey = ["Default";"Goal";"Selector"] ;
-                                  optread = begin fun () -> print_goal_selector !default_goal_selector end;
+                                  optread = begin fun () ->
+                                            string_of_ppcmds
+                                              (pr_goal_selector !default_goal_selector)
+                                            end;
                                   optwrite = begin fun n ->
                                     default_goal_selector := parse_goal_selector n
                                   end
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 3b2cc6b23..6bb6f5e2c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -198,6 +198,7 @@ end
 (*                                                        *)
 (**********************************************************)
 
+val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
 val get_default_goal_selector : unit -> Vernacexpr.goal_selector
 
 module V82 : sig
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index fb6adaec5..c4f392f20 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -202,8 +202,7 @@ let rec classify_vernac e =
     (* What are these? *)
     | VernacToplevelControl _
     | VernacRestoreState _
-    | VernacWriteState _
-    | VernacError _ -> VtUnknown, VtNow
+    | VernacWriteState _ -> VtUnknown, VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 81fda176e..7446c17d9 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -98,6 +98,14 @@ h: n <> newdef n
 h': newdef n <> n
 h: n <> newdef n
 h: n <> newdef n
+h: n <> newdef n
+h': newdef n <> n
+The command has indeed failed with message:
+No such goal.
+The command has indeed failed with message:
+Query commands only support the single numbered goal selector.
+The command has indeed failed with message:
+Query commands only support the single numbered goal selector.
 h: P n
 h': ~ P n
 h: P n
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 2a0f0b407..82096f29b 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro".  (* andb_prop *)
 Definition newdef := fun x:nat => x.
 
 Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
-  intros n h h'.
+  cut False.
+  intros _ n h h'.
   Search n.                             (* search hypothesis *)
   Search newdef.                        (* search hypothesis *)
   Search ( _ <> newdef _).              (* search hypothesis, pattern *)
   Search ( _ <> newdef _) -"h'".        (* search hypothesis, pattern *)
+
+  1:Search newdef.
+  2:Search newdef.
+
+  Fail 3:Search newdef.
+  Fail 1-2:Search newdef.
+  Fail all:Search newdef.
 Abort.
 
 Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 92b1a5956..52136a70e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1533,7 +1533,14 @@ let get_current_context_of_args = function
   | Some n -> get_goal_context n
   | None -> get_current_context ()
 
-let vernac_check_may_eval redexp glopt rc =
+let query_command_selector ~loc = function
+  | None -> None
+  | Some (SelectNth n) -> Some n
+  | _ -> user_err ~loc ~hdr:"query_command_selector"
+      (str "Query commands only support the single numbered goal selector.")
+
+let vernac_check_may_eval ~loc redexp glopt rc =
+  let glopt = query_command_selector ~loc glopt in
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma', c = interp_open_constr env sigma rc in
   let c = EConstr.Unsafe.to_constr c in
@@ -1595,9 +1602,10 @@ exception NoHyp
 (* Printing "About" information of a hypothesis of the current goal.
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ref_or_by_not glnumopt =
+let print_about_hyp_globs ~loc ref_or_by_not glopt =
   let open Context.Named.Declaration in
   try
+    let glnumopt = query_command_selector ~loc glopt in
     let gl,id =
       match glnumopt,ref_or_by_not with
       | None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *)
@@ -1605,8 +1613,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
       | Some n,AN (Ident (_loc,id)) ->  (* goal number given, catch if wong *)
 	 (try get_nth_goal n,id
 	  with
-	    Failure _ -> user_err ~hdr:"print_about_hyp_globs"
-                           (str "No such goal: " ++ int n ++ str "."))
+	    Failure _ -> user_err ~loc ~hdr:"print_about_hyp_globs"
+                          (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
     let hyps = pf_hyps gl in
     let decl = Context.Named.lookup id hyps in
@@ -1619,7 +1627,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
     | NoHyp | Not_found -> print_about ref_or_by_not
 
 	       
-let vernac_print = let open Feedback in function
+let vernac_print ~loc = let open Feedback in function
   | PrintTables -> msg_notice (print_tables ())
   | PrintFullContext-> msg_notice (print_full_context_typ ())
   | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
@@ -1664,7 +1672,7 @@ let vernac_print = let open Feedback in function
   | PrintVisibility s ->
       msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintAbout (ref_or_by_not,glnumopt) ->
-     msg_notice (print_about_hyp_globs ref_or_by_not glnumopt)
+     msg_notice (print_about_hyp_globs ~loc ref_or_by_not glnumopt)
   | PrintImplicit qid ->
     dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,t,r) ->
@@ -1729,7 +1737,8 @@ let _ =
       optread  = (fun () -> !search_output_name_only);
       optwrite = (:=) search_output_name_only }
 
-let vernac_search s gopt r =
+let vernac_search ~loc s gopt r =
+  let gopt = query_command_selector ~loc gopt in
   let r = interp_search_restriction r in
   let env,gopt =
     match gopt with | None ->
@@ -1935,9 +1944,6 @@ let interp ?proof ~loc locality poly c =
   | VernacBack _       -> anomaly (str "VernacBack not handled by Stm")
   | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm")
 
-  (* Horrible Hack that should die. *)
-  | VernacError e -> raise e
-
   (* This one is possible to handle here *)
   | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
 
@@ -2039,11 +2045,11 @@ let interp ?proof ~loc locality poly c =
   | VernacAddOption (key,v) -> vernac_add_option key v
   | VernacMemOption (key,v) -> vernac_mem_option key v
   | VernacPrintOption key -> vernac_print_option key
-  | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c
+  | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~loc r g c
   | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
   | VernacGlobalCheck c -> vernac_global_check c
-  | VernacPrint p -> vernac_print p
-  | VernacSearch (s,g,r) -> vernac_search s g r
+  | VernacPrint p -> vernac_print ~loc p
+  | VernacSearch (s,g,r) -> vernac_search ~loc s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")