From 417f0d8373c6999e3ec77144685286cda30172c7 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 3 Jun 2005 13:14:27 +0000
Subject: whelp + correction bug affichage de coqide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7102 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq_commands.ml |  3 +++
 ide/coqide.ml       | 12 +++++++++++-
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 0e16a18d46..4dde601113 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -211,6 +211,9 @@ let state_preserving = [
   "Test Printing Let";
   "Test Printing Synth";
   "Test Printing Wildcard";
+
+  "Whelp Hint";
+  "Whelp Locate";
 ]
 
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 63e6c1178b..c838cd6687 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -970,9 +970,11 @@ object(self)
       end
     with e ->
       (if show_error then
+	 let msg = read_stdout () in 
+	 self#insert_message (if show_output then msg else "");
 	 let (s,loc) = Coq.process_exn e in
 	 assert (Glib.Utf8.validate s);
-	 self#set_message s;
+	 self#insert_message s;
 	 message_view#misc#draw None;
 	 if localize then 
 	   (match Util.option_app Util.unloc loc with 
@@ -2770,6 +2772,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		   ~term 
 		   ())
   in
+  let _ = 
+    queries_factory#add_item "_Whelp Locate" 
+      ~callback:(fun () -> let term = get_current_word () in
+		 (Command_windows.command_window ())#new_command
+		 ~command:"Whelp Locate"
+		   ~term 
+		   ())
+  in
 
   (* Externals *)
   let externals_menu =  factory#add_submenu "_Compile" in
-- 
cgit v1.2.3