Declarative mode: fix escape and return.

The declarative mode should now work almost like in v8.3

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

3 files changed, 17 insertions, 22 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 549b1f146..c5fcabfc3 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -127,13 +127,6 @@ let daimon_tac gls =
   set_daimon_flag ();
   {it=[];sigma=sig_sig gls}
 
-let daimon _ pftree =
-  set_daimon_flag ();
-  {pftree with
-     ref=Some (Daimon,[])}
-
-let daimon_subtree =
-  fun _ -> Util.anomaly "Todo: Decl_proof_instr.daimon_subtree"
 
 (* marking closed blocks *)
 
@@ -164,16 +157,12 @@ let goto_current_focus_or_top pts =
 (* return *)
 
 let close_tactic_mode pts =
-    let pts1=
-      try goto_current_focus pts
-      with Not_found ->
-	error "\"return\" cannot be used outside of Declarative Proof Mode." in
-    let pts2 = daimon_subtree pts1 in
-      goto_current_focus pts2
+  try goto_current_focus pts
+  with Not_found ->
+    error "\"return\" cannot be used outside of Declarative Proof Mode."
 
 let return_from_tactic_mode () =
-  (* arnaud: la commande return ne fonctionne pas *)
-  Util.anomaly "Todo: Decl_proof_instr.return_from_tactic_mode"
+  close_tactic_mode (Proof_global.give_me_the_proof ())
 
 (* end proof/claim *)
 
@@ -1376,7 +1365,12 @@ let end_tac et2 gls =
 
 (* escape *)
 
-let escape_tac gls =  tcl_erase_info gls
+let escape_tac gls =
+  (* spiwack: sets an empty info stack to avoid interferences.
+     We could erase the info altogether, but that doesn't play
+     well with the Decl_mode.focus (used in post_processing). *)
+  let info={pm_stack=[]} in
+  tcl_change_info info gls
 
 (* General instruction engine *)
 
@@ -1440,8 +1434,11 @@ let rec postprocess pts instr =
       Phence i | Pthus i | Pthen i -> postprocess pts i
     | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> ()
-    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _
-    | Pescape -> Decl_mode.focus pts
+    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ ->
+      Decl_mode.focus pts
+    | Pescape ->
+      Decl_mode.focus pts;
+      Proof_global.set_proof_mode "Classic"
     | Pend (B_elim ET_Induction) ->
   	begin
 	  let pfterm = List.hd (Proof.partial_proof pts) in
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index b27939b3c..1205060ae 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -19,8 +19,6 @@ val register_automation_tac: tactic -> unit
 
 val automation_tac : tactic
 
-val daimon_subtree: Proof.proof -> Proof.proof
-
 val concl_refiner:
   Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr
 
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index a133089f8..aa187cc74 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -74,12 +74,12 @@ let vernac_decl_proof () =
     end
 
 (* spiwack: some bureaucracy is not performed here *)
-let vernac_return () = 
+let vernac_return () =
   Decl_proof_instr.return_from_tactic_mode () ;
   Proof_global.set_proof_mode "Declarative" ;
   Vernacentries.print_subgoals ()
 
-let vernac_proof_instr instr = 
+let vernac_proof_instr instr =
   Decl_proof_instr.proof_instr instr;
   Vernacentries.print_subgoals ()