From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 ide/command_windows.ml | 34 ++++++++++++----------------------
 1 file changed, 12 insertions(+), 22 deletions(-)

(limited to 'ide/command_windows.ml')

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 1df83803..939238d3 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command_windows.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-class command_window () =
+class command_window coqtop current =
 (*  let window = GWindow.window
 		 ~allow_grow:true ~allow_shrink:true
 		 ~width:500 ~height:250
@@ -76,14 +74,10 @@ object(self)
     notebook#goto_page (notebook#page_num frame#coerce);
     let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
     let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
-    let combo = GEdit.combo ~popdown_strings:Coq_commands.state_preserving
-		  ~enable_arrow_keys:true
-		  ~allow_empty:false
-		  ~value_in_list:false (* true is not ok with disable_activate...*)
+    let (combo,_) = GEdit.combo_box_entry_text ~strings:Coq_commands.state_preserving
 		  ~packing:hbox#pack
 		  ()
     in
-    combo#disable_activate ();
     let on_activate c () =
       if List.mem combo#entry#text Coq_commands.state_preserving then c ()
       else prerr_endline "Not a state preserving command"
@@ -97,6 +91,7 @@ object(self)
 	~packing:(vbox#pack ~fill:true ~expand:true) () in
     let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in
     let result = GText.view ~packing:r_bin#add () in
+    result#misc#modify_font !current.Preferences.text_font;
     result#misc#set_can_focus true; (* false causes problems for selection *)
     result#set_editable false;
     let callback () =
@@ -106,11 +101,14 @@ object(self)
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
       try
-	ignore(Coq.interp false phrase);
-	result#buffer#set_text
-	  ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ())
+        result#buffer#set_text
+          (match Coq.interp !coqtop ~raw:true phrase with
+             | Interface.Fail (l,str) ->
+                 ("Error while interpreting "^phrase^":\n"^str)
+             | Interface.Good results ->
+                 ("Result for command " ^ phrase ^ ":\n" ^ results))
       with e ->
-	let (s,loc) = Coq.process_exn e in
+	let s = Printexc.to_string e in
 	assert (Glib.Utf8.validate s);
 	result#buffer#set_text s
     in
@@ -137,14 +135,6 @@ object(self)
     self#frame#misc#show ()
 
   initializer
-    ignore (new_page_menu#connect#clicked self#new_command);
+    ignore (new_page_menu#connect#clicked ~callback:self#new_command);
    (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*)
 end
-
-let command_window = ref None
-
-let main () = command_window := Some (new command_window ())
-
-let command_window () = match !command_window with
-  | None -> failwith "No command window."
-  | Some c -> c
-- 
cgit v1.2.3