Nettoyage de l'interface de Pfedit

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

7 files changed, 62 insertions, 48 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2f755b4e37..93426fde9b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -372,3 +372,11 @@ let build_scheme lnamedepindsort =
   declare 0 lrecnames; 
   if is_verbose() then pPNL(recursive_message lrecnames)
 
+let start_proof_com s stre com =
+  let env = Global.env () in
+  Pfedit.start_proof s stre env (interp_type Evd.empty env com)
+
+let get_current_context () =
+  try Pfedit.get_current_goal_context ()
+  with e when Logic.catchable_exception e -> 
+    (Evd.empty, Global.env())
diff --git a/toplevel/command.mli b/toplevel/command.mli
index cd4cb930d5..1cc9d5a754 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -38,3 +38,4 @@ val build_corecursive :  (identifier * Coqast.t * Coqast.t) list -> unit
 
 val build_scheme : (identifier * bool * identifier * Coqast.t) list -> unit
 
+val start_proof_com : string -> strength -> Coqast.t -> unit
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8b1fc69f3f..079ad7ed16 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -310,7 +310,7 @@ let explain_refiner_cannot_unify m n =
      'sTR"with"; 'bRK(1,1) ; pn >]
 
 let explain_refiner_cannot_generalize ty =
-  [< 'sTR "cannot find a generalisation of the goal with type : "; 
+  [< 'sTR "Cannot find a well-typed generalisation of the goal with type : "; 
      prterm ty >]
 
 let explain_refiner_not_well_typed c =
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 6d2ebf57ac..fcc7da2c2c 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -162,10 +162,13 @@ let valid_buffer_loc ib dloc (b,e) =
 (* A buffer to store the current command read on stdin. It is
  * initialized when a vernac command is immediately followed by "\n",
  * or after a Drop. *)
+let make_prompt () =
+  if Pfedit.refining () then
+    (Pfedit.get_current_proof_name ())^" < "
+  else "Coq < "
 
 let top_buffer =
-  let pr() = 
-    (Pfedit.proof_prompt())^(emacs_str (String.make 1 (Char.chr 249)))
+  let pr() = (make_prompt())^(emacs_str (String.make 1 (Char.chr 249)))
   in
   { prompt = pr;
     str = "";
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e3adda7f0d..bad51033bf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -125,9 +125,7 @@ and raw_compile_module verbosely only_spec mname file =
   Library.open_module mname;
   let lfname = read_vernac_file verbosely file in
   let base = Filename.chop_suffix lfname ".v" in
-  if Pfedit.refining () then
-    errorlabstrm "Vernac.raw_compile_module"
-      [< 'sTR"proof editing in progress" ; (Pfedit.msg_proofs false) >];
+  Pfedit.check_no_pending_proofs ();
   if only_spec then
     failwith ".vi not yet implemented"
   else 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1a45b8540b..f21768913e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -101,11 +101,6 @@ let show_top_evars () =
   let sigma = project gls in 
   mSG (pr_evars_int 1 (Evd.non_instantiated sigma))
 
-(* Focus commands *)
-let reset_top_of_tree () = 
-  let pts = get_pftreestate () in 
-  if not (is_top_pftreestate pts) then Pfedit.mutate top_of_tree
-
 (* Locate commands *)
  
 let locate_file f =
@@ -125,9 +120,9 @@ let print_loadpath () =
   mSGNL [< 'sTR"Load Path:"; 'fNL; 'sTR"  ";
            hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >]
 
-let goal_of_args = function
-  | [VARG_NUMBER n] -> Some n
-  | [] -> None
+let get_goal_context_of_args = function
+  | [VARG_NUMBER n] -> get_goal_context n
+  | [] -> get_current_goal_context ()
   | _ -> bad_vernac_args "goal_of_args"
 
 let isfinite = function 
@@ -218,24 +213,29 @@ let _ =
 
 (* Managing states *)
 
+let abort_refine f x =
+  if Pfedit.refining() then abort_goals ();
+  f x
+  (* used to be: error "Must save or abort current goal first" *)
+
 let _ =
   add "WriteState"
     (function 
        | [VARG_STRING file] ->
-	   (fun () -> Pfedit.abort_refine States.extern_state file)
+	   (fun () -> abort_refine States.extern_state file)
        | [VARG_IDENTIFIER id] ->
 	   let file = string_of_id id in
-	   (fun () -> Pfedit.abort_refine States.extern_state file)
+	   (fun () -> abort_refine States.extern_state file)
        | _ -> bad_vernac_args "SaveState")
 
 let _ =
   add "RestoreState"
     (function 
        | [VARG_STRING file] ->
-	   (fun () -> Pfedit.abort_refine States.intern_state file)
+	   (fun () -> abort_refine States.intern_state file)
        | [VARG_IDENTIFIER id] ->
 	   let file = string_of_id id in
-	   (fun () -> Pfedit.abort_refine States.intern_state file)
+	   (fun () -> abort_refine States.intern_state file)
        | _ -> bad_vernac_args "LoadState")
 
 (* Resetting *)
@@ -244,13 +244,13 @@ let _ =
   add "ResetName"
     (function 
        | [VARG_IDENTIFIER id] -> 
-	   (fun () -> Pfedit.abort_refine Lib.reset_name id)
+	   (fun () -> abort_refine Lib.reset_name id)
        | _ -> bad_vernac_args "ResetName")
 
 let _ =
   add "ResetInitial"
     (function 
-       | [] -> (fun () -> Pfedit.abort_refine Lib.reset_initial ())
+       | [] -> (fun () -> abort_refine Lib.reset_initial ())
        | _  -> bad_vernac_args "ResetInitial")
 
 (***
@@ -328,10 +328,7 @@ let _ =
     (function 
        | [VARG_IDENTIFIER id] ->
 	   (fun () ->
-              if refining () then 
-		errorlabstrm "vernacentries : EndSection"
-		  [< 'sTR"proof editing in progress" ; (msg_proofs false) ;
-                     'sTR"Use \"Abort All\" first or complete proof(s)." >];
+	      check_no_pending_proofs ();
               Discharge.close_section (not (is_silent())) (string_of_id id))
        | _ -> bad_vernac_args "EndSection")
 
@@ -343,7 +340,7 @@ let _ =
        | [VARG_CONSTR com] ->
 	   (fun () ->
               if not (refining()) then begin
-              	start_proof "Unnamed_thm" NeverDischarge com;
+              	start_proof_com "Unnamed_thm" NeverDischarge com;
 		if not (is_silent()) then show_open_subgoals ()
               end else 
 		error "repeated Goal not permitted in refining mode")
@@ -357,13 +354,21 @@ let _ =
 	   (fun () -> 
 	      let s = string_of_id id in
 	      abort_goal s; message ("Goal "^s^" aborted"))
-       | [] -> (fun () -> abort_cur_goal (); message "Current goal aborted")
+       | [] -> (fun () -> 
+		  abort_current_goal ();
+		  message "Current goal aborted")
        | _  -> bad_vernac_args "ABORT")
 
 let _ =
   add "ABORTALL"
     (function 
-       | [] -> (fun () -> abort_goals())
+       | [] -> (fun () ->
+		  if refining() then begin
+		    abort_goals ();
+		    message "Current goals aborted"
+		  end else
+		    error "No proof-editing in progress")
+
        | _  -> bad_vernac_args "ABORTALL")
 
 let _ =
@@ -375,15 +380,15 @@ let _ =
 let _ =
   add "SUSPEND"
     (function 
-       | [] -> (fun () -> set_proof None)
+       | [] -> (fun () -> set_current_proof None)
        | _  -> bad_vernac_args "SUSPEND")
 
 let _ =
   add "RESUME"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   (fun () -> set_proof (Some(string_of_id id)))
-       | [] -> (fun () -> resume_last ())
+	   (fun () -> set_current_proof (Some(string_of_id id)))
+       | [] -> (fun () -> resume_last_proof ())
        | _  -> bad_vernac_args "RESUME")
 
 let _ =
@@ -509,11 +514,11 @@ let _ =
        | [VARG_NUMBER n] ->
 	   (fun () -> (Pfedit.traverse n;show_node()))
        | [VARG_STRING"top"] ->
-           (fun () -> (mutate top_of_tree;show_node()))
+           (fun () -> (Pfedit.reset_top_of_tree ();show_node()))
        | [VARG_STRING"next"] ->
-           (fun () -> (mutate next_unproven;show_node()))
+           (fun () -> (Pfedit.traverse_next_unproven ();show_node()))
        | [VARG_STRING"prev"] ->
-           (fun () -> (mutate prev_unproven;show_node()))
+           (fun () -> (Pfedit.traverse_prev_unproven ();show_node()))
        | _ -> bad_vernac_args "Go")
 
 let _ =
@@ -608,7 +613,7 @@ let _ =
   add "ShowProofs"
     (function [] ->
        (fun () ->
-	  let l = Pfedit.list_proofs() in 
+	  let l = Pfedit.get_all_proof_names() in 
 	  mSGNL (prlist_with_sep pr_spc pr_str l))
        | _  -> bad_vernac_args "ShowProofs")
 
@@ -660,7 +665,7 @@ let _ =
 let _ =
   add "StartProof"
     (function 
-       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR c] ->
+       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
 	   let stre = match kind with
 	     | "THEOREM" -> NeverDischarge
              | "LEMMA" -> NeverDischarge
@@ -673,7 +678,7 @@ let _ =
            in 
 	   fun () ->
              begin
-               start_proof (string_of_id s) stre c;
+               start_proof_com (string_of_id s) stre com;
                if (not(is_silent())) then show_open_subgoals()
              end
        | _ -> bad_vernac_args "StartProof")
@@ -682,7 +687,7 @@ let _ =
   add "TheoremProof"
     (function 
        | [VARG_STRING kind; VARG_IDENTIFIER s; 
-	  VARG_CONSTR c; VARG_VARGLIST coml] ->
+	  VARG_CONSTR com; VARG_VARGLIST coml] ->
 	   let calls = List.map
 			 (function 
 			    | (VCALL(na,l)) -> (na,l)
@@ -703,7 +708,7 @@ let _ =
               try
             	States.with_heavy_rollback
 		  (fun () ->
-                     start_proof (string_of_id s) stre c;
+                     start_proof_com (string_of_id s) stre com;
                      if not (is_silent()) then show_open_subgoals();
                      List.iter Vernacinterp.call calls;
                      if not (is_silent()) then show_script();
@@ -714,8 +719,8 @@ let _ =
                   mSGNL [< 'sTR"Error: checking of theorem " ; print_id s ;
                            'sPC ; 'sTR"failed" ;
                            'sTR"... converting to Axiom" >];
-                  del_proof (string_of_id s);
-                  parameter_def_var (string_of_id s) c
+                  abort_goal (string_of_id s);
+                  parameter_def_var (string_of_id s) com
            	end else 
 		  errorlabstrm "vernacentries__TheoremProof"
                     [< 'sTR"checking of theorem " ; print_id s ; 'sPC ;
@@ -809,7 +814,7 @@ let _ =
   add "Eval"
     (function
        | VARG_TACTIC_ARG (Redexp redexp) :: VARG_CONSTR c :: g ->
-           let (evmap,sign) = get_evmap_sign (goal_of_args g) in
+           let (evmap,sign) = get_goal_context_of_args g in
            let redfun = print_eval (reduction_of_redexp redexp) sign in 
 	   fun () -> mSG (redfun (judgment_of_com evmap sign c))
        | _ -> bad_vernac_args "Eval")
@@ -818,7 +823,7 @@ let _ =
   add "Check"
     (function 
        | VARG_STRING kind :: VARG_CONSTR c :: g ->
-	   let (evmap, sign) = get_evmap_sign (goal_of_args g) in
+	   let (evmap, sign) = get_goal_context_of_args g in
 	   let prfun = match kind with
 	     | "CHECK" -> print_val
              | "PRINTTYPE" -> print_type
@@ -862,7 +867,7 @@ let _ =
 let _ =
   add "UNSETUNDO"
     (function 
-       | [] -> (fun () -> unset_undo ())
+       | [] -> (fun () -> reset_undo ())
        | _  -> bad_vernac_args "UNSETUNDO")
 
 let _ =
@@ -1407,7 +1412,7 @@ let _ =
   vinterp_add "EXISTENTIAL"
     (function 
        | [VARG_NUMBER n; VARG_CONSTR c] -> 
-           (fun () -> mutate (instantiate_pf_com n c))
+           (fun () -> instantiate_nth_evar_com n c)
        |  _  -> assert false)
 
 (* The second is a stupid macro that should be replaced by ``Exact
@@ -1449,5 +1454,5 @@ let _ =
           (* in case a strict subtree was completed, 
               go back to the top of the prooftree *) 
 	  if subtree_solved () then 
-	    (rev_mutate top_of_tree; print_subgoals()) 
+	    (reset_top_of_tree (); print_subgoals()) 
        ))
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index ea27b4aa67..1f55e4a3ec 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -96,9 +96,8 @@ let rec cvt_varg ast =
     | Node(_,"AST",[a]) -> VARG_AST a
     | Node(_,"ASTLIST",al) -> VARG_ASTLIST al
     | Node(_,"TACTIC_ARG",[targ]) ->
-      let (evc,env)=Pfedit.get_evmap_sign None
-      in
-        VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None) targ)
+      let (evc,env)= Pfedit.get_current_goal_context () in
+      VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None) targ)
     | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d
     | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg",
                         [< 'sTR "Unrecognizable ast node of vernac arg:";