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 ------------------------------------------------ ide/command_windows.mli | 16 ----- ide/coqide.ml | 6 +- ide/ide.mllib | 4 +- ide/typed_notebook.ml | 67 -------------------- ide/wg_Command.ml | 158 ++++++++++++++++++++++++++++++++++++++++++++++++ ide/wg_Command.mli | 16 +++++ ide/wg_Notebook.ml | 67 ++++++++++++++++++++ ide/wg_Notebook.mli | 38 ++++++++++++ 9 files changed, 284 insertions(+), 246 deletions(-) delete mode 100644 ide/command_windows.ml delete mode 100644 ide/command_windows.mli delete mode 100644 ide/typed_notebook.ml create mode 100644 ide/wg_Command.ml create mode 100644 ide/wg_Command.mli create mode 100644 ide/wg_Notebook.ml create mode 100644 ide/wg_Notebook.mli 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 *) -(* 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 diff --git a/ide/command_windows.mli b/ide/command_windows.mli deleted file mode 100644 index c34b6cf67a..0000000000 --- a/ide/command_windows.mli +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Preferences.pref ref -> - object - method new_command : ?command:string -> ?term:string -> unit -> unit - method frame : GBin.frame - method refresh_font : unit -> unit - method refresh_color : unit -> unit - end diff --git a/ide/coqide.ml b/ide/coqide.ml index 263ccf7a6d..9540fe4b96 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -102,7 +102,7 @@ type viewable_script = message_view : GText.view; analyzed_view : analyzed_views; toplvl : Coq.coqtop ref; - command : Command_windows.command_window; + command : Wg_Command.command_window; } let kill_session s = @@ -159,7 +159,7 @@ let build_session s = (Some session_tab#coerce,None,session_paned#coerce) let session_notebook = - Typed_notebook.create build_session kill_session + Wg_Notebook.create build_session kill_session ~border_width:2 ~show_border:false ~scrollable:true () let cb = GData.clipboard Gdk.Atom.primary @@ -1512,7 +1512,7 @@ let create_session file = |Subst_args -> Project_file.args_from_project the_file !custom_project_files !current.project_file_name in let ct = ref (Coq.spawn_coqtop coqtop_args) in - let command = new Command_windows.command_window ct current in + let command = new Wg_Command.command_window ct current in let legacy_av = new analyzed_view script proof message stack ct file in let () = legacy_av#update_stats in let _ = diff --git a/ide/ide.mllib b/ide/ide.mllib index 9bbf9b0d9e..ee498ba0c6 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -9,7 +9,7 @@ Configwin Editable_cells Config_parser Tags -Typed_notebook +Wg_Notebook Config_lexer Utf8_convert Preferences @@ -21,6 +21,6 @@ Gtk_parsing Undo Coq Coq_commands -Command_windows +Wg_Command Coqide_ui Coqide diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml deleted file mode 100644 index 499d56bd9a..0000000000 --- a/ide/typed_notebook.ml +++ /dev/null @@ -1,67 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* if i = real_pos then term else x) 0 term_list; - super#set_page ?tab_label ?menu_label page - - method get_nth_term i = - List.nth term_list i - - method term_num p = - Minilib.list_index0 p term_list - - method pages = term_list - - method remove_page index = - term_list <- Minilib.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list; - super#remove_page index - - method current_term = - List.nth term_list super#current_page -end - -let create make kill = - GtkPack.Notebook.make_params [] - ~cont:(GContainer.pack_container - ~create:(fun pl -> - let nb = GtkPack.Notebook.create pl in - (new typed_notebook make kill nb))) - diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml new file mode 100644 index 0000000000..a34e5ebeb3 --- /dev/null +++ b/ide/wg_Command.ml @@ -0,0 +1,158 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli new file mode 100644 index 0000000000..c34b6cf67a --- /dev/null +++ b/ide/wg_Command.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Preferences.pref ref -> + object + method new_command : ?command:string -> ?term:string -> unit -> unit + method frame : GBin.frame + method refresh_font : unit -> unit + method refresh_color : unit -> unit + end diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml new file mode 100644 index 0000000000..499d56bd9a --- /dev/null +++ b/ide/wg_Notebook.ml @@ -0,0 +1,67 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* if i = real_pos then term else x) 0 term_list; + super#set_page ?tab_label ?menu_label page + + method get_nth_term i = + List.nth term_list i + + method term_num p = + Minilib.list_index0 p term_list + + method pages = term_list + + method remove_page index = + term_list <- Minilib.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list; + super#remove_page index + + method current_term = + List.nth term_list super#current_page +end + +let create make kill = + GtkPack.Notebook.make_params [] + ~cont:(GContainer.pack_container + ~create:(fun pl -> + let nb = GtkPack.Notebook.create pl in + (new typed_notebook make kill nb))) + diff --git a/ide/wg_Notebook.mli b/ide/wg_Notebook.mli new file mode 100644 index 0000000000..d413a4b02d --- /dev/null +++ b/ide/wg_Notebook.mli @@ -0,0 +1,38 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* GObj.widget option * GObj.widget option * GObj.widget) -> + ('a -> unit) -> + Gtk.notebook Gtk.obj -> +object + inherit GPack.notebook + method append_term : 'a -> int + method prepend_term : 'a -> int + method set_term : 'a -> unit + method get_nth_term : int -> 'a + method term_num : 'a -> int + method pages : 'a list + method remove_page : int -> unit + method current_term : 'a +end + +val create : + ('a -> GObj.widget option * GObj.widget option * GObj.widget) -> + ('a -> unit) -> + ?enable_popup:bool -> + ?homogeneous_tabs:bool -> + ?scrollable:bool -> + ?show_border:bool -> + ?show_tabs:bool -> + ?tab_border:int -> + ?tab_pos:Gtk.Tags.position -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> 'a typed_notebook -- cgit v1.2.3