diff options
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 158 |
1 files changed, 0 insertions, 158 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml deleted file mode 100644 index 67b09656..00000000 --- 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-2014 *) -(* \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 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 on_activate c () = - if List.mem combo#entry#text Coq_commands.state_preserving then c () - else result#buffer#set_text "Error: Not a state preserving command" - in - 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 0 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 |