Moving VernacSolve to an EXTEND-based definition.

9 files changed, 80 insertions, 66 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5501ca7c7f..36b855ec3b 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -31,7 +31,6 @@ type goal_selector =
   | SelectNth of int
   | SelectId of Id.t
   | SelectAll
-  | SelectAllParallel
 
 type goal_identifier = string
 type scope_name = string
@@ -363,7 +362,6 @@ type vernac_expr =
 
   (* Solving *)
 
-  | VernacSolve of goal_selector * int option * raw_tactic_expr * bool
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 35a9fede1b..79392195fb 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
 open Util
 open Pp
 open Compat
@@ -38,7 +40,14 @@ let reference_to_id = function
         str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
-let selector = Gram.entry_create "vernac:selector"
+
+let new_entry name =
+  let e = Gram.entry_create name in
+  let entry = Entry.create name in
+  let () = Pcoq.set_grammar entry e in
+  e
+
+let selector = new_entry "vernac:selector"
 
 (* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
     proof editing and changes nothing else). Then sets it as the default proof mode. *)
@@ -290,16 +299,73 @@ GEXTEND Gram
   selector:
     [ [ n=natural; ":" -> Vernacexpr.SelectNth n
       | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id
-      | IDENT "all" ; ":" -> Vernacexpr.SelectAll
-      | IDENT "par" ; ":" -> Vernacexpr.SelectAllParallel ] ]
+      | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ]
   ;
   tactic_mode:
-    [ [ g = OPT selector;
-        tac = G_vernac.subgoal_command -> tac g
-      | g = OPT selector; info = OPT [IDENT "Info";n=natural -> n];
-        tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] ->
-        let g = Option.default (Proof_global.get_default_goal_selector ()) g in
-        Vernacexpr.VernacSolve (g, info, tac, use_dft_tac)
-    ] ]
+    [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ]
   ;
   END
+
+open Stdarg
+open Constrarg
+open Vernacexpr
+open Vernac_classifier
+
+let print_info_trace = ref None
+
+let _ = let open Goptions in declare_int_option {
+  optsync = true;
+  optdepr = false;
+  optname = "print info trace";
+  optkey = ["Info" ; "Level"];
+  optread = (fun () -> !print_info_trace);
+  optwrite = fun n -> print_info_trace := n;
+}
+
+let vernac_solve n info tcom b =
+  let status = Proof_global.with_current_proof (fun etac p ->
+    let with_end_tac = if b then Some etac else None in
+    let global = match n with SelectAll -> true | _ -> false in
+    let info = Option.append info !print_info_trace in
+    let (p,status) =
+      Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+    in
+    (* in case a strict subtree was completed,
+       go back to the top of the prooftree *)
+    let p = Proof.maximal_unfocus Vernacentries.command_focus p in
+    p,status) in
+    if not status then Pp.feedback Feedback.AddedAxiom
+
+let pr_ltac_selector = function
+| SelectNth i -> int i ++ str ":"
+| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+| SelectAll -> str "all" ++ str ":"
+
+VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
+| [ selector(s) ] -> [ s ]
+END
+
+let pr_ltac_info n = str "Info" ++ spc () ++ int n
+
+VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info
+| [ "Info" natural(n) ] -> [ n ]
+END
+
+let pr_ltac_use_default b = if b then str ".." else mt ()
+
+VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default
+| [ "." ] -> [ false ]
+| [ "..." ] -> [ true ]
+END
+
+VERNAC tactic_mode EXTEND VernacSolve
+| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    [ classify_as_proofstep ] -> [
+    let g = Option.default (Proof_global.get_default_goal_selector ()) g in
+    vernac_solve g n t def
+  ]
+| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    [ VtProofStep true, VtLater ] -> [
+    vernac_solve SelectAll n t def
+  ]
+END
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a101540aba..887a14d2bf 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -979,24 +979,6 @@ module Make
                      prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
           )
         (* Solving *)
-      | VernacSolve (i,info,tac,deftac) ->
-        let pr_goal_selector = function
-          | SelectNth i -> int i ++ str":"
-          | SelectId id -> pr_id id ++ str":"
-          | SelectAll -> str"all" ++ str":"
-          | SelectAllParallel -> str"par"
-        in
-        let pr_info =
-          match info with
-            | None -> mt ()
-            | Some i -> str"Info"++spc()++int i++spc()
-        in
-        return (
-          (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
-          pr_info ++
-          pr_raw_tactic tac
-          ++ (if deftac then str ".." else mt ())
-        )
         | VernacSolveExistential (i,c) ->
           return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 0fdcaa5875..608ee2c700 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -104,7 +104,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match gi with
       | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
       | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
-      | Vernacexpr.SelectAll | Vernacexpr.SelectAllParallel -> tac
+      | Vernacexpr.SelectAll -> tac
     in
     let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
     let () =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d19dc5ba0f..647dbe1115 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -664,7 +664,6 @@ let print_goal_selector = function
   | Vernacexpr.SelectAll -> "all"
   | Vernacexpr.SelectNth i -> string_of_int i
   | Vernacexpr.SelectId id -> Id.to_string id
-  | Vernacexpr.SelectAllParallel -> "par"
 
 let parse_goal_selector = function
   | "all" -> Vernacexpr.SelectAll
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 3c4b8cb71e..a459cd65f8 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -671,7 +671,7 @@ let rec tmpp v loc =
 
   (* Solving *)
 
-  | (VernacSolve _ | VernacSolveExistential _) as x ->
+  | (VernacSolveExistential _) as x ->
       xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
 
   (* Auxiliary file and library management *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f9f08f7afb..97d6e1fb71 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -102,12 +102,10 @@ let rec classify_vernac e =
     | VernacCheckMayEval _ ->
         VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
-    | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
     | VernacProof _ 
     | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
     | VernacSubproof _ | VernacEndSubproof
-    | VernacSolve _ 
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ -> VtProofStep false, VtLater
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fd125b335c..8ba5eb3f7d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -826,35 +826,6 @@ let vernac_declare_class id =
 let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
-
-let print_info_trace = ref None
-
-let _ = let open Goptions in declare_int_option {
-  optsync = true;
-  optdepr = false;
-  optname = "print info trace";
-  optkey = ["Info" ; "Level"];
-  optread = (fun () -> !print_info_trace);
-  optwrite = fun n -> print_info_trace := n;
-}
-
-let vernac_solve n info tcom b =
-  if not (refining ()) then
-    error "Unknown command of the non proof-editing mode.";
-  let status = Proof_global.with_current_proof (fun etac p ->
-    let with_end_tac = if b then Some etac else None in
-    let global = match n with SelectAll -> true | _ -> false in
-    let info = Option.append info !print_info_trace in
-    let (p,status) =
-      solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
-    in
-    (* in case a strict subtree was completed,
-       go back to the top of the prooftree *)
-    let p = Proof.maximal_unfocus command_focus p in
-    p,status) in
-    if not status then Pp.feedback Feedback.AddedAxiom
- 
-
   (* A command which should be a tactic. It has been
      added by Christine to patch an error in the design of the proof
      machine, and enables to instantiate existential variables when
@@ -892,7 +863,6 @@ let vernac_set_used_variables e =
       fst (solve SelectAll None tac p), ()
   end
 
-
 (*****************************)
 (* Auxiliary file management *)
 
@@ -1909,7 +1879,6 @@ let interp ?proof ~loc locality poly c =
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
-  | VernacSolve (n,info,tac,b) -> vernac_solve n info tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
 
   (* Auxiliary file and library management *)
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 451ccdb4d4..4a59b1299b 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -59,3 +59,5 @@ val vernac_end_proof :
   ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
 
 val with_fail : bool -> (unit -> unit) -> unit
+
+val command_focus : unit Proof.focus_kind