- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"

  n'étaient pas gérés, merci à Julien). 
- Correction pb blocage CoqIDE quand le browser n'est pas déja lancé
  (utilisation pour cela de Sys.command au lieu de Unix.open_process_full).
- MAJ CHANGES et COMPATIBILITY.


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

3 files changed, 11 insertions, 13 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index ca28d1948..f45bd9f5c 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -376,8 +376,9 @@ let compute_reset_info = function
   | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
       ResetAtStatement (reset_mark id, ref false)
 
-  | VernacEndProof _ | VernacEndSegment _ -> NoReset
-  | _ -> match Lib.has_top_frozen_state () with
+  | VernacEndProof _ | VernacExactProof _ | VernacEndSegment _ -> NoReset
+  | com -> if is_vernac_tactic_command com then NoReset else
+      match Lib.has_top_frozen_state () with
       | Some sp -> ResetAtRegisteredObject (ResetToState sp, ref true)
       | None -> NoReset
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index dd807443b..29b34d28a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -533,7 +533,7 @@ let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast =
 	  } in
   begin
     match snd ast with
-      | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
+      | VernacEndProof _ | VernacExactProof _ -> update_on_end_of_proof ()
       | VernacEndSegment (_,id) -> update_on_end_of_segment id
       | _ -> ()
   end;
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 6a4833ec8..3442910d3 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -289,10 +289,8 @@ let run_command f c =
   let buffe = String.make 127 ' ' in
   let n = ref 0 in
   let ne = ref 0 in
-
-  while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; 
-    !n+ !ne <> 0
-  do 
+  while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0
+  do
     let r = try_convert (String.sub buff 0 !n) in 
     f r;
     Buffer.add_string result r;
@@ -304,10 +302,10 @@ let run_command f c =
 
 let browse f url =
   let com = Flags.subst_command_placeholder !current.cmd_browse url in
-  let (s,_res) = run_command f com in
-  if s = Unix.WEXITED 127 then
-    prerr_endline
-      ("Could not execute\n  \""^com^"\"\ncheck your preferences for setting a valid browser command")
+  let s = Sys.command com in
+  if s = 127 then
+    f ("Could not execute\n\""^com^
+       "\"\ncheck your preferences for setting a valid browser command\n")
 
 let url_for_keyword =
   let ht = Hashtbl.create 97 in
@@ -332,8 +330,7 @@ let url_for_keyword =
 
 let browse_keyword f text = 
   try let u = url_for_keyword text in browse f (!current.doc_url ^ u) 
-  with Not_found ->
-    prerr_endline ("No documentation found for "^text)
+  with Not_found -> f ("No documentation found for "^text)
 
 
 let underscore = Glib.Utf8.to_unichar "_" (ref 0)