From a2e44a2dbe77c5ce227ea7e12d2cfce903221254 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 20 Apr 2012 11:38:44 +0000
Subject: Cleaning up widget code and using a naming convention for such files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15232 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/command_windows.ml | 158 -------------------------------------------------
 1 file changed, 158 deletions(-)
 delete mode 100644 ide/command_windows.ml

(limited to 'ide/command_windows.ml')

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
deleted file mode 100644
index a34e5ebeb3..0000000000
--- a/ide/command_windows.ml
+++ /dev/null
@@ -1,158 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <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        *)
-(************************************************************************)
-
-class command_window coqtop current =
-(*  let window = GWindow.window
-		 ~allow_grow:true ~allow_shrink:true
-		 ~width:500 ~height:250
-		 ~position:`CENTER
-		 ~title:"CoqIde queries" ~show:false ()
-  in *)
-  let views = ref [] in
-  let frame = GBin.frame ~label:"Command Pane" ~shadow_type:`IN () in
-  let _ = frame#misc#hide () in
-  let _ = GtkData.AccelGroup.create () in
-  let hbox = GPack.hbox ~homogeneous:false ~packing:frame#add () in
-  let toolbar = GButton.toolbar
-		  ~orientation:`VERTICAL
-		  ~style:`ICONS
-		  ~tooltips:true
-		  ~packing:(hbox#pack
-			       ~expand:false
-			       ~fill:false)
-		  ()
-  in
-  let notebook = GPack.notebook ~scrollable:true
-		   ~packing:(hbox#pack
-			       ~expand:true
-			       ~fill:true
-			    )
-		   ()
-  in
-  let _ =
-    toolbar#insert_button
-      ~tooltip:"Hide Commands Pane"
-      ~text:"Hide Pane"
-      ~icon:(Ideutils.stock_to_widget `CLOSE)
-      ~callback:frame#misc#hide
-      ()
-  in
-  let new_page_menu =
-    toolbar#insert_button
-      ~tooltip:"New Page"
-      ~text:"New Page"
-      ~icon:(Ideutils.stock_to_widget `NEW)
-      ()
-  in
-
-  let remove_cb () =
-    let index = notebook#current_page in
-    let () = notebook#remove_page index in
-    views := Minilib.list_filter_i (fun i x -> i <> index) !views
-  in
-  let _ =
-    toolbar#insert_button
-      ~tooltip:"Delete Page"
-      ~text:"Delete Page"
-      ~icon:(Ideutils.stock_to_widget `DELETE)
-      ~callback:remove_cb
-      ()
-  in
-object(self)
-  val frame = frame
-
-
-  val new_page_menu = new_page_menu
-  val notebook = notebook
-
-  method frame = frame
-  method new_command ?command ?term () =
-    let frame = GBin.frame
-		  ~shadow_type:`ETCHED_OUT
-		  ()
-    in
-    let _ = notebook#append_page frame#coerce in
-    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_box_entry_text ~strings:Coq_commands.state_preserving
-		  ~packing:hbox#pack
-		  ()
-    in
-    let on_activate c () =
-      if List.mem combo#entry#text Coq_commands.state_preserving then c ()
-      else prerr_endline "Not a state preserving command"
-    in
-    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 ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in
-    let result = GText.view ~packing:r_bin#add () in
-    let () = views := !views @ [result] in
-    result#misc#modify_font !current.Preferences.text_font;
-    let clr = Tags.color_of_string !current.Preferences.background_color in
-    result#misc#modify_base [`NORMAL, `COLOR clr];
-    result#misc#set_can_focus true; (* false causes problems for selection *)
-    result#set_editable false;
-    let callback () =
-      let com = combo#entry#text in
-      let phrase =
-	if String.get com (String.length com - 1) = '.'
-	then com ^ " " else com ^ " " ^ entry#text ^" . "
-      in
-      try
-        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 = Printexc.to_string e in
-	assert (Glib.Utf8.validate s);
-	result#buffer#set_text s
-    in
-    ignore (combo#entry#connect#activate ~callback:(on_activate callback));
-    ignore (ok_b#connect#clicked ~callback:(on_activate callback));
-
-    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;
-    on_activate callback ();
-    entry#misc#grab_focus ();
-    entry#misc#grab_default ();
-    ignore (entry#connect#activate ~callback);
-    ignore (combo#entry#connect#activate ~callback);
-    self#frame#misc#show ()
-
-  method refresh_font () =
-    let iter view = view#misc#modify_font !current.Preferences.text_font in
-    List.iter iter !views
-
-  method refresh_color () =
-    let clr = Tags.color_of_string !current.Preferences.background_color in
-    let iter view = view#misc#modify_base [`NORMAL, `COLOR clr] in
-    List.iter iter !views
-
-  initializer
-    ignore (new_page_menu#connect#clicked ~callback:self#new_command);
-   (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*)
-end
-- 
cgit v1.2.3