Started to fix the declarative proof mode (C-zar).

Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported).
However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc.

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

4 files changed, 55 insertions, 26 deletions

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 232edda0fd..af6aa4bf59 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -66,7 +66,7 @@ type command_mode =
   | Mode_none
 
 let mode_of_pftreestate pts =
-  (* spiwack: it was "top_goal_..." but this should be fine *)
+  (* spiwack: it used to be "top_goal_..." but this should be fine *)
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
   let goal = List.hd goals in
     if info.get (Goal.V82.extra sigma goal) = None then
@@ -96,10 +96,25 @@ let get_stack pts =
   let info = get_info sigma (List.hd goals) in
   info.pm_stack
 
+
+let proof_focus = Proof.new_focus_kind ()
+let proof_cond = Proof.no_cond proof_focus
+
+let focus p =
+  let inf = get_stack p in
+  Proof.focus proof_cond inf 1 p
+
+let unfocus = Proof.unfocus proof_focus
+
+let maximal_unfocus = Proof_global.maximal_unfocus proof_focus
+
 let get_top_stack pts =
-  let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
-  let info = get_info sigma gl in
-  info.pm_stack
+  try
+    Proof.get_at_focus proof_focus pts
+  with Proof.NoSuchFocus ->
+    let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
+    let info = get_info sigma gl in
+    info.pm_stack
 
 let get_last env =
   try
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 72c46c7e7d..4e636598f9 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -70,3 +70,9 @@ val get_stack : Proof.proof -> stack_info list
 val get_top_stack : Proof.proof -> stack_info list
 
 val get_last:  Environ.env -> identifier
+
+val focus : Proof.proof -> unit
+
+val unfocus : Proof.proof -> unit
+
+val maximal_unfocus : Proof.proof -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index cee4d7271d..549b1f1465 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -111,17 +111,15 @@ let assert_postpone id t =
 
 (* start a proof *)
 
-let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
 
 let start_proof_tac gls=
   let info={pm_stack=[]} in
   tcl_change_info info gls
 
 let go_to_proof_mode () =
-  Pfedit.by start_proof_tac  ;
+  Pfedit.by start_proof_tac;
   let p = Proof_global.give_me_the_proof () in
-  Proof.focus proof_cond 1 p
+  Decl_mode.focus p
 
 (* closing gaps *)
 
@@ -154,12 +152,14 @@ let mark_rule_as_done = function
 
 (* post-instruction focus management *)
 
+(* spiwack: This used to fail if there was no focusing command
+   above, but I don't think it ever happened. I hope it doesn't mess
+   things up*)
 let goto_current_focus pts = 
-  Proof.unfocus proof_focus pts
+  Decl_mode.maximal_unfocus pts
 
 let goto_current_focus_or_top pts =
-  try goto_current_focus pts
-  with Util.UserError _ -> ()
+  goto_current_focus pts
 
 (* return *)
 
@@ -172,6 +172,7 @@ let close_tactic_mode pts =
       goto_current_focus pts2
 
 let return_from_tactic_mode () =
+  (* arnaud: la commande return ne fonctionne pas *)
   Util.anomaly "Todo: Decl_proof_instr.return_from_tactic_mode"
 
 (* end proof/claim *)
@@ -180,7 +181,12 @@ let close_block bt pts =
     if Proof.no_focused_goal pts then
       goto_current_focus pts
     else
-      let stack =get_stack pts in
+      let stack =
+	if Proof.is_done pts then
+	  get_top_stack pts
+	else
+	  get_stack pts 
+      in
       match bt,stack with
 	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
 	  (goto_current_focus pts)
@@ -197,7 +203,7 @@ let close_block bt pts =
 	      | ET_Induction ->  error "\"end induction\" expected."
 	  end
       | _,_ -> anomaly "Lonely suppose on stack."
-  
+
 
 (* utility for suppose / suppose it is *)
 
@@ -577,8 +583,8 @@ let instr_claim _thus st gls0 =
   let ninfo1 = {pm_stack=
       (if _thus then Focus_claim else Claim)::info.pm_stack} in
     tclTHENS (assert_postpone id st.st_it)
-      [tcl_change_info ninfo1;
-       thus_tac] gls0
+      [thus_tac;
+       tcl_change_info ninfo1] gls0
 
 (* tactics for assume *)
 
@@ -1294,12 +1300,9 @@ let understand_my_constr c gls =
   let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc ->  map_glob_constr frob rc in
     Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
 
-let set_refine,my_refine =
-let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in
-((fun tac -> refine:= tac),
-(fun c gls -> 
-   let oc = understand_my_constr c gls in
-     !refine oc gls))
+let my_refine c gls =
+  let oc = understand_my_constr c gls in
+  Refine.refine oc gls
 
 (* end focus/claim *)
 
@@ -1438,12 +1441,16 @@ let rec postprocess pts instr =
     | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> ()
     | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _
-    | Pescape -> Proof.focus proof_cond 1 pts
+    | Pescape -> Decl_mode.focus pts
     | Pend (B_elim ET_Induction) ->
   	begin
 	  let pfterm = List.hd (Proof.partial_proof pts) in
 	  let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in
-	  let env =  Goal.V82.env sigma (List.hd gls) in
+	  let env =  try
+		       Goal.V82.env sigma (List.hd gls)
+	             with Failure "hd" ->
+		       Global.env ()
+	  in
 	    try
 	      Inductiveops.control_only_guard env pfterm;
 	      goto_current_focus_or_top pts
@@ -1469,7 +1476,10 @@ let do_instr raw_instr pts =
 	interp_proof_instr (get_its_info gl) sigma env glob_instr in
       Pfedit.by (tclTHEN (eval_instr instr) clean_tmp)
     else () end;
-  postprocess pts raw_instr.instr
+  postprocess pts raw_instr.instr;
+  (* spiwack: this should restore a compatible semantics with
+     v8.3 where we never stayed focused on 0 goal. *)
+  Decl_mode.maximal_unfocus pts
 
 let proof_instr raw_instr =
   let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index 0a2ab571ff..b27939b3ca 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -109,5 +109,3 @@ val init_tree:
      (int option * Declarations.recarg Rtree.t) array ->
      (Names.Idset.t * Decl_mode.split_tree) option) ->
     Decl_mode.split_tree
-
-val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit