diff options
Diffstat (limited to 'ide/wg_Command.ml')
-rw-r--r-- | ide/wg_Command.ml | 158 |
1 files changed, 158 insertions, 0 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml new file mode 100644 index 000000000..a34e5ebeb --- /dev/null +++ b/ide/wg_Command.ml @@ -0,0 +1,158 @@ +(************************************************************************) +(* 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 |