X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=686f54399327801a5193dd0c42dfa7df18fef898;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=038aa7fd13539a0cf7d1a6575d36dfa6628f556e;hpb=05963c3c472ae13fbc9f5f80bd0fe2a616390340;p=helm.git diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 038aa7fd1..686f54399 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -29,13 +29,6 @@ open Printf open MatitaTypes let wrap_callback f = f -(* -let wrap_callback f () = - try - f () - with exn -> - MatitaLog.error (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) -*) let connect_button (button: #GButton.button) callback = ignore (button#connect#clicked (wrap_callback callback)) @@ -90,35 +83,89 @@ let add_key_binding key callback (evbox: GBin.event_box) = false | _ -> false)) -class stringListModel (tree_view: GTree.view) = +class multiStringListModel ~cols (tree_view: GTree.view) = let column_list = new GTree.column_list in - let text_column = column_list#add Gobject.Data.string in + let text_columns = + let rec aux = function + | 0 -> [] + | n -> column_list#add Gobject.Data.string :: aux (n - 1) + in + aux cols + in let list_store = GTree.list_store column_list in - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in + let renderers = + List.map + (fun text_column -> + (GTree.cell_renderer_text [], ["text", text_column])) + text_columns + in + let view_columns = + List.map + (fun renderer -> GTree.view_column ~renderer ()) + renderers + in object (self) + val text_columns = text_columns + initializer tree_view#set_model (Some (list_store :> GTree.model)); - ignore (tree_view#append_column view_column) + List.iter + (fun view_column -> ignore (tree_view#append_column view_column)) + view_columns method list_store = list_store - method easy_append s = + method easy_mappend slist = let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s + List.iter2 + (fun s text_column -> + list_store#set ~row:tree_iter ~column:text_column s) + slist text_columns - method easy_insert pos s = + method easy_minsert pos s = let tree_iter = list_store#insert pos in - list_store#set ~row:tree_iter ~column:text_column s + List.iter2 + (fun s text_column -> + list_store#set ~row:tree_iter ~column:text_column s) + s text_columns - method easy_selection () = + method easy_mselection () = List.map (fun tree_path -> let iter = list_store#get_iter tree_path in - list_store#get ~row:iter ~column:text_column) + List.map + (fun text_column -> + list_store#get ~row:iter ~column:text_column) + text_columns) tree_view#selection#get_selected_rows end +class stringListModel (tree_view: GTree.view) = + object (self) + inherit multiStringListModel ~cols:1 tree_view as multi + + method list_store = multi#list_store + + method easy_append s = + multi#easy_mappend [s] + + method easy_insert pos s = + multi#easy_minsert pos [s] + + method easy_selection () = + let m = List.map + (fun tree_path -> + let iter = self#list_store#get_iter tree_path in + List.map + (fun text_column -> + self#list_store#get ~row:iter ~column:text_column) + text_columns) + tree_view#selection#get_selected_rows + in + List.map (function [x] -> x | _ -> assert false) m + end + + class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list) (tree_view: GTree.view) = @@ -189,27 +236,73 @@ let popup_message GtkThread.main (); m#destroy () +let popup_message_lowlevel + ~title ~message ?(no_separator=true) ~callback ~message_type ~buttons + ?parent ?(destroy_with_parent=true) ?(allow_grow=false) ?(allow_shrink=false) + ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint + ?(position=`CENTER_ON_PARENT) ?wm_name ?wm_class ?border_width ?width + ?height ?(show=true) () += + let m = + GWindow.dialog + ~no_separator + ?parent ~destroy_with_parent + ~title ~allow_grow ~allow_shrink ?icon ~modal ~resizable ?screen + ?type_hint ~position ?wm_name ?wm_class ?border_width ?width ?height + ~show:false () + in + let stock = + match message_type with + | `WARNING -> `DIALOG_WARNING + | `INFO -> `DIALOG_INFO + | `ERROR ->`DIALOG_ERROR + | `QUESTION -> `DIALOG_QUESTION + in + let image = GMisc.image ~stock ~icon_size:`DIALOG () in + let label = GMisc.label ~markup:message () in + label#set_line_wrap true; + let hbox = GPack.hbox ~spacing:10 () in + hbox#pack ~from:`START ~expand:true ~fill:true (image:>GObj.widget); + hbox#pack ~from:`START ~expand:true ~fill:true (label:>GObj.widget); + m#vbox#pack ~from:`START + ~padding:20 ~expand:true ~fill:true (hbox:>GObj.widget); + List.iter (fun (x, y) -> + m#add_button_stock x y; + if y = `CANCEL then + m#set_default_response y + ) buttons; + ignore(m#connect#response + ~callback:(fun a -> GMain.Main.quit ();callback a)); + ignore(m#connect#close + ~callback:(fun _ -> GMain.Main.quit ();callback `POPUPCLOSED)); + if show = true then + m#show (); + GtkThread.main (); + m#destroy () + let ask_confirmation ~title ~message ?parent () = - let rc = ref false in + let rc = ref `YES in let callback = - function `YES -> rc := true | `NO -> rc := false | _ -> rc := false + function + | `YES -> rc := `YES + | `NO -> rc := `NO + | `CANCEL -> rc := `CANCEL + | `DELETE_EVENT -> rc := `CANCEL + | `POPUPCLOSED -> rc := `CANCEL in - let buttons = GWindow.Buttons.yes_no in - try - popup_message ~title ~message ~message_type:`WARNING ~callback ~buttons - ?parent (); + let buttons = [`YES,`YES ; `NO,`NO ; `CANCEL,`CANCEL] in + popup_message_lowlevel + ~title ~message ~message_type:`WARNING ~callback ~buttons ?parent (); !rc - with - | PopupClosed -> false let report_error ~title ~message ?parent () = let rc = ref false in let callback _ = () in let buttons = GWindow.Buttons.ok in try - popup_message ~title ~message ~message_type:`ERROR ~callback ~buttons - ?parent () + popup_message + ~title ~message ~message_type:`ERROR ~callback ~buttons ?parent () with | PopupClosed -> ()