Fix goal display when backtracking

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

2 files changed, 8 insertions, 3 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index d5450220e..7e742b55d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -720,6 +720,7 @@ object(self)
 
   method show_goals_full =
     if not full_goal_done then
+      proof_view#buffer#set_text "";
       begin
         let menu_callback = if !current.contextual_menus_on_goal then
           (fun s () -> ignore (self#insert_this_phrase_on_success
@@ -978,6 +979,7 @@ object(self)
   (* backtrack Coq to the phrase preceding iterator [i] *)
   method backtrack_to_no_lock i =
     prerr_endline "Backtracking_to iter starts now.";
+    full_goal_done <- false;
     (* pop Coq commands until we reach iterator [i] *)
     let rec n_step n =
       if Stack.is_empty cmd_stack then n else
@@ -1030,6 +1032,7 @@ object(self)
       else self#backtrack_to point
 
   method undo_last_step =
+    full_goal_done <- false;
     if Mutex.try_lock coq_may_stop then
       (push_info "Undoing last step...";
        (try
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index d578122a0..9dce5c1cc 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -404,9 +404,10 @@ let concl_next_tac sigma concl =
   ])
 
 let current_goals () =
-  let pfts =
-    Proof_global.give_me_the_proof ()
-  in
+  try 
+    let pfts =
+      Proof_global.give_me_the_proof ()
+    in
   let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in
   if all_goals = [] then
     begin
@@ -441,6 +442,7 @@ let current_goals () =
       in
       Goals (List.map process_goal all_goals)
     end
+  with Proof_global.NoCurrentProof -> Message "" (* quick hack to have a clean message screen *)
 
 let id_of_name = function
   | Names.Anonymous -> id_of_string "x"