coqide: fenetre de cmmandes . undo correct

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

1 files changed, 118 insertions, 0 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
new file mode 100644
index 0000000000..f442eac2b8
--- /dev/null
+++ b/ide/command_windows.ml
@@ -0,0 +1,118 @@
+let decompose_tab w = 
+  let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in
+  let l = vbox#children in
+  match l with 
+    | [img;lbl] -> 
+	let img = new GMisc.image 
+		    ((Gobject.try_cast img#as_widget "GtkImage"):
+		       Gtk.image Gtk.obj) 
+	in
+	let lbl = GMisc.label_cast lbl in
+	vbox,img,lbl
+    | _ -> assert false
+
+
+class command_window () = 
+  let window = GWindow.window 
+		 ~allow_grow:true ~allow_shrink:true 
+		 ~width:320 ~height:200
+		 ~title:"CoqIde Commands" ~show:false ()
+  in
+  let accel_group = GtkData.AccelGroup.create () in
+  let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in
+  let menubar = GMenu.menu_bar ~packing:vbox#pack () in
+  let factory = new GMenu.factory menubar
+  in
+  let accel_group = factory#accel_group in
+
+  let notebook = GPack.notebook ~scrollable:true 
+		   ~packing:(vbox#pack 
+			       ~expand:true
+			       ~fill:true
+			    ) 
+		   ()
+  in
+  let hide_menu = factory#add_item "_Hide Window" 
+		    ~callback:window#misc#hide
+  in
+  let new_page_menu = factory#add_item "_New Page" in
+  let kill_page_menu = 
+    factory#add_item "_Kill Page" 
+      ~callback:
+      (fun () -> notebook#remove_page notebook#current_page)
+  in
+object(self)
+  val window = window
+  val menubar = menubar
+  val new_page_menu = new_page_menu
+  val notebook = notebook
+  method window = window
+  method new_command ?command ?term () =
+    let frame = GBin.frame 
+		  ~shadow_type:`ETCHED_OUT
+		  ~packing:notebook#append_page
+		  ()
+    in
+    notebook#next_page ();
+    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
+		  ~use_arrows:`ALWAYS
+		  ~ok_if_empty:false
+		  ~value_in_list:true
+		  ~packing:hbox#pack
+		  ()
+    in
+    combo#entry#set_editable false;
+
+    let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in
+    entry#misc#set_can_default true;
+    let r_bin =
+      GBin.scrolled_window 
+	~vpolicy:`AUTOMATIC 
+	~hpolicy:`AUTOMATIC
+	~packing:(vbox#pack ~fill:true ~expand:true) () in
+    let result = GText.view ~packing:r_bin#add () in
+    result#misc#set_can_focus false;
+    result#set_editable false;
+    begin match command,term with 
+      | None,None -> ()
+      | Some c, None -> 
+	  combo#entry#set_text c
+	  
+      | Some c, Some t -> 
+	  combo#entry#set_text c;
+	  entry#set_text t
+
+      | None , Some t -> 
+	  entry#set_text t
+    end;
+    entry#misc#grab_focus ();
+    entry#misc#grab_default ();
+
+    let callback () =
+      let phrase = combo#entry#text ^ " " ^ entry#text ^" . " in
+      try 
+	ignore(Coq.interp phrase);
+	result#buffer#set_text (Ideutils.read_stdout ())
+      with e ->
+	let (s,loc) = Coq.process_exn e in
+	assert (Glib.Utf8.validate s);
+	result#buffer#set_text s
+    in
+    ignore (entry#connect#activate ~callback);
+    ignore (combo#entry#connect#activate ~callback);
+    self#window#present ()
+
+  initializer 
+    ignore (new_page_menu#connect#activate 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