Moving bullets (-, +, *) into stand-alone commands instead of being

part of a tactic.
WARNING: Coqide needs to be adapted.


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

6 files changed, 33 insertions, 26 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 756f1d5186..02d2663361 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -37,7 +37,6 @@ let check_command = Gram.entry_create "vernac:check_command"
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
 let noedit_mode = Gram.entry_create "vernac:noedit_command"
-let bullet = Gram.entry_create "vernac:bullet"
 let subprf = Gram.entry_create "vernac:subprf"
 
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
@@ -70,7 +69,7 @@ let default_command_entry =
 
 let no_hook _ _ = ()
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext tactic_mode noedit_mode bullet subprf subgoal_command;
+  GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
     [ [ IDENT "Time"; v = vernac -> VernacTime v
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
@@ -97,22 +96,20 @@ GEXTEND Gram
       | -> locality_flag := None ] ]
   ;
   noedit_mode:
-    [ [ c = subgoal_command -> c None None] ]
+    [ [ c = subgoal_command -> c None] ]
   ;
   tactic_mode:
   [ [ gln = OPT[n=natural; ":" -> n];
-      tac = subgoal_command -> tac gln None 
-    | b = bullet; tac = subgoal_command -> tac None (Some b)] ]
-  ;
-  bullet:
-  [ [ "-" -> Dash
-    | "*" -> Star
-    | "+" -> Plus ] ]
+      tac = subgoal_command -> tac gln 
+    | tac = subgoal_command -> tac None ] ]
   ;
 
   subprf:
   [ [
-      "{" -> VernacSubproof None
+      "-" -> VernacBullet Dash
+    | "*" -> VernacBullet Star
+    | "+" -> VernacBullet Plus
+    | "{" -> VernacSubproof None
     | "}" -> VernacEndSubproof
     ] ]
   ;
@@ -120,12 +117,12 @@ GEXTEND Gram
 
 
   subgoal_command: 
-    [ [ c = check_command; "." -> fun g _ -> c g
+    [ [ c = check_command; "." -> fun g -> c g
       | tac = Tactic.tactic;
         use_dft_tac = [ "." -> false | "..." -> true ] ->
-          (fun g b ->
+          (fun g ->
             let g = Option.default 1 g in
-            VernacSolve(g,b,tac,use_dft_tac)) ] ]
+            VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
   located_vernac:
     [ [ v = vernac -> loc, v ] ]
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e10d42b9d9..c858439e6a 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -754,14 +754,8 @@ let rec pr_vernac = function
       hov 2 (str"Include " ++
 	     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
   (* Solving *)
-  | VernacSolve (i,b,tac,deftac) ->
+  | VernacSolve (i,tac,deftac) ->
       (if i = 1 then mt() else int i ++ str ": ") ++
-      begin match b with
-      | None -> mt ()
-      | Some Dash -> str"-"
-      | Some Star -> str"*"
-      | Some Plus -> str"+"
-      end ++
       pr_raw_tactic tac
       ++ (try if deftac then str ".." else mt ()
       with UserError _|Loc.Exc_located _ -> mt())
@@ -979,6 +973,11 @@ let rec pr_vernac = function
       str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++
       str "with" ++ spc() ++pr_raw_tactic te
   | VernacProofMode s -> str ("Proof Mode "^s)
+  | VernacBullet b -> begin match b with
+      | Dash -> str"-"
+      | Star -> str"*"
+      | Plus -> str"+"
+  end ++ spc()
   | VernacSubproof None -> str "BeginSubproof"
   | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i
   | VernacEndSubproof -> str "EndSubproof"
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 8ed3ae62d3..27def8cc13 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -139,7 +139,7 @@ GEXTEND Gram
   GLOBAL: proof_mode ;
 
   proof_mode: LAST
-    [ [ c=G_vernac.subgoal_command -> c (Some 1) None ] ]
+    [ [ c=G_vernac.subgoal_command -> c (Some 1) ] ]
   ;
 END  
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 31a651279d..42ecb75bcb 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -208,6 +208,7 @@ let rec attribute_of_vernac_command = function
   | VernacProof _ -> []
 
   | VernacProofMode _ -> []
+  | VernacBullet _ -> [SolveCommand]
   | VernacSubproof _ -> [SolveCommand]
   | VernacEndSubproof -> [SolveCommand]
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 435d85233e..a04b167cbb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -645,12 +645,11 @@ let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
 
-let vernac_solve n bullet tcom b =
+let vernac_solve n tcom b =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode.";
   let p = Proof_global.give_me_the_proof () in
   Proof.transaction p begin fun () ->
-    Option.iter (Proof_global.Bullet.put p) bullet ;
     solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b;
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
@@ -1367,6 +1366,15 @@ let vernac_end_subproof () =
   let p = Proof_global.give_me_the_proof () in
   Proof.unfocus subproof_kind p ; print_subgoals ()
 
+
+let vernac_bullet (bullet:Proof_global.Bullet.t) =
+  let p = Proof_global.give_me_the_proof () in
+  Proof.transaction p 
+    (fun () -> Proof_global.Bullet.put p bullet);
+  (* Makes the focus visible in emacs by re-printing the goal. *)
+  if !Flags.print_emacs then print_subgoals ();;
+
+
 let vernac_show = function
   | ShowGoal goalref ->
       if !pcoq <> None then (Option.get !pcoq).show_goal goalref
@@ -1459,7 +1467,7 @@ let interp c = match c with
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
-  | VernacSolve (n,bullet,tac,b) -> vernac_solve n bullet tac b
+  | VernacSolve (n,tac,b) -> vernac_solve n tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
 
   (* Auxiliary file and library management *)
@@ -1519,6 +1527,7 @@ let interp c = match c with
   | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
+  | VernacBullet b -> vernac_bullet b
   | VernacSubproof n -> vernac_subproof n
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index b1ab3bdce0..f2e2c0ac70 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -284,7 +284,7 @@ type vernac_expr =
 
   (* Solving *)
 
-  | VernacSolve of int * bullet option * raw_tactic_expr * bool
+  | VernacSolve of int * raw_tactic_expr * bool
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
@@ -353,6 +353,7 @@ type vernac_expr =
   | VernacBacktrack of int*int*int
   | VernacFocus of int option
   | VernacUnfocus
+  | VernacBullet of bullet
   | VernacSubproof of int option
   | VernacEndSubproof
   | VernacShow of showable