From c342a8f9b53c7a8da71803733dcd65d9c0282304 Mon Sep 17 00:00:00 2001
From: marche
Date: Tue, 9 Dec 2003 09:48:05 +0000
Subject: commandes de coqide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5081 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/command_windows.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'ide/command_windows.ml')

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);
-- 
cgit v1.2.3