commandes de coqide

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

1 files changed, 7 insertions, 2 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 444495ee12..0d1b9fa754 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -147,10 +147,15 @@ object(self)
     result#misc#set_can_focus true; (* false causes problems for selection *)
     result#set_editable false;
     let callback () =
-      let phrase = combo#entry#text ^ " " ^ entry#text ^" . " in
+      let com = combo#entry#text in
+      let phrase = 
+	if String.get com (String.length com - 1) = '.'
+	then com ^ " " else com ^ " " ^ entry#text ^" . " 
+      in
       try
 	ignore(Coq.interp phrase);
-	result#buffer#set_text (Ideutils.read_stdout ())
+	result#buffer#set_text 
+	  ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ())
       with e ->
 	let (s,loc) = Coq.process_exn e in
 	assert (Glib.Utf8.validate s);