X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=3c0d1b4c359ba15ba418b70f1cd74585a6d27484;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=80f5676cd7665ca66c0c59aaa5230d66934b9f64;hpb=07dde6f87105c18b28fc784b7d596a5d242e1225;p=helm.git diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 80f5676cd..3c0d1b4c3 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2004, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,11 +23,47 @@ * http://helm.cs.unibo.it/ *) -let toggle_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) = +exception PopupClosed +open Printf + +open MatitaTypes + +let wrap_callback f = f + +let connect_button (button: #GButton.button) callback = + ignore (button#connect#clicked (wrap_callback callback)) + +let connect_toggle_button (button: #GButton.toggle_button) callback = + ignore (button#connect#toggled (wrap_callback callback)) + +let connect_menu_item (menu_item: #GMenu.menu_item) callback = + ignore (menu_item#connect#activate (wrap_callback callback)) + +let connect_key (ev:GObj.event_ops) ?(modifiers = []) ?(stop = false) key + callback += + ignore (ev#connect#key_press (fun key' -> + let modifiers' = GdkEvent.Key.state key' in + (match key' with + | key' when GdkEvent.Key.keyval key' = key + && List.for_all (fun m -> List.mem m modifiers') modifiers -> + callback (); + stop + | _ -> false))) + +let toggle_widget_visibility ~(widget: GObj.widget) + ~(check: GMenu.check_menu_item) += ignore (check#connect#toggled (fun _ -> - if check#active then win#show () else win#misc#hide ())); - ignore (win#event#connect#delete (fun _ -> - win#misc#hide (); + if check#active then widget#misc#show () else widget#misc#hide ())) + +let toggle_window_visibility ~(window: GWindow.window) + ~(check: GMenu.check_menu_item) += + ignore (check#connect#toggled (fun _ -> + if check#active then window#show () else window#misc#hide ())); + ignore (window#event#connect#delete (fun _ -> + window#misc#hide (); check#set_active false; true)) @@ -37,6 +73,9 @@ let toggle_win ?(check: GMenu.check_menu_item option) (win: GWindow.window) () = | None -> () | Some check -> check#set_active (not check#active) +let toggle_callback ~callback ~(check: GMenu.check_menu_item) = + ignore (check#connect#toggled (fun _ -> callback check#active)) + let add_key_binding key callback (evbox: GBin.event_box) = ignore (evbox#event#connect#key_press (function | key' when GdkEvent.Key.keyval key' = key -> @@ -44,27 +83,119 @@ let add_key_binding key callback (evbox: GBin.event_box) = false | _ -> false)) +class multiStringListModel ~cols (tree_view: GTree.view) = + let column_list = new GTree.column_list 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 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)); + List.iter + (fun view_column -> ignore (tree_view#append_column view_column)) + view_columns + + method list_store = list_store + + method easy_mappend slist = + let tree_iter = list_store#append () in + List.iter2 + (fun s text_column -> + list_store#set ~row:tree_iter ~column:text_column s) + slist text_columns + + method easy_minsert pos s = + let tree_iter = list_store#insert pos in + List.iter2 + (fun s text_column -> + list_store#set ~row:tree_iter ~column:text_column s) + s text_columns + + method easy_mselection () = + List.map + (fun tree_path -> + let iter = list_store#get_iter tree_path in + 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) += let column_list = new GTree.column_list in + let tag_column = column_list#add Gobject.Data.gobject in let text_column = column_list#add Gobject.Data.string in let list_store = GTree.list_store column_list in + let text_renderer = (GTree.cell_renderer_text [], ["text", text_column]) in + let tag_renderer = (GTree.cell_renderer_pixbuf [], ["pixbuf", tag_column]) in + let text_vcolumn = GTree.view_column ~renderer:text_renderer () in + let tag_vcolumn = GTree.view_column ~renderer:tag_renderer () in + let lookup_pixbuf tag = + try List.assoc tag tags with Not_found -> assert false + in object (self) - initializer - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in tree_view#set_model (Some (list_store :> GTree.model)); - ignore (tree_view#append_column view_column) + ignore (tree_view#append_column tag_vcolumn); + ignore (tree_view#append_column text_vcolumn) method list_store = list_store - method easy_append s = + method easy_append ~tag s = let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s + list_store#set ~row:tree_iter ~column:text_column s; + list_store#set ~row:tree_iter ~column:tag_column (lookup_pixbuf tag) - method easy_insert pos s = + method easy_insert pos ~tag s = let tree_iter = list_store#insert pos in - list_store#set ~row:tree_iter ~column:text_column s + list_store#set ~row:tree_iter ~column:text_column s; + list_store#set ~row:tree_iter ~column:tag_column (lookup_pixbuf tag) method easy_selection () = List.map @@ -72,84 +203,241 @@ class stringListModel (tree_view: GTree.view) = let iter = list_store#get_iter tree_path in list_store#get ~row:iter ~column:text_column) tree_view#selection#get_selected_rows - end -let is_var_uri s = - try - String.sub s (String.length s - 4) 4 = ".var" - with Invalid_argument _ -> false +class recordModel (tree_view:GTree.view) = + let cols_list = new GTree.column_list in + let text_col = cols_list#add Gobject.Data.string in +(* let combo_col = cols_list#add (Gobject.Data.gobject_by_name "GtkListStore") in *) + let combo_col = cols_list#add Gobject.Data.int in + let toggle_col = cols_list#add Gobject.Data.boolean in + let list_store = GTree.list_store cols_list in + let text_rend = (GTree.cell_renderer_text [], ["text", text_col]) in + let combo_rend = GTree.cell_renderer_combo [] in +(* let combo_rend = (GTree.cell_renderer_combo [], [|+"model", combo_col+|]) in *) + let toggle_rend = + (GTree.cell_renderer_toggle [`ACTIVATABLE true], ["active", toggle_col]) + in + let text_vcol = GTree.view_column ~renderer:text_rend () in + let combo_vcol = GTree.view_column ~renderer:(combo_rend, []) () in + let _ = + combo_vcol#set_cell_data_func combo_rend + (fun _ _ -> + prerr_endline "qui"; + let model, col = + GTree.store_of_list Gobject.Data.string ["a"; "b"; "c"] + in + combo_rend#set_properties [ + `MODEL (Some (model :> GTree.model)); + `TEXT_COLUMN col + ]) + in + let toggle_vcol = GTree.view_column ~renderer:toggle_rend () in + object (self) + initializer + tree_view#set_model (Some (list_store :> GTree.model)); + ignore (tree_view#append_column text_vcol); + ignore (tree_view#append_column combo_vcol); + ignore (tree_view#append_column toggle_vcol) -let non p x = not (p x) + method list_store = list_store + + method easy_append s (combo:int) (toggle:bool) = + let tree_iter = list_store#append () in + list_store#set ~row:tree_iter ~column:text_col s; + list_store#set ~row:tree_iter ~column:combo_col combo; + list_store#set ~row:tree_iter ~column:toggle_col toggle + end class type gui = object - method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newConfirmationDialog : - title:string -> msg:string -> unit -> - MatitaGeneratedGui.confirmationDialog + method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog + method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end -let interactive_user_uri_choice - ~(gui:#gui) ~(selection_mode:Gtk.Tags.selection_mode) ?(title = "") - ?(msg = "") ?(nonvars_button=false) uris +let popup_message + ~title ~message ~buttons ~callback + ?(message_type=`QUESTION) ?parent ?(use_markup=true) + ?(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 nonvars_uris = lazy (List.filter (non is_var_uri) uris) in - if (selection_mode <> `SINGLE) && - (Helm_registry.get_bool "matita.auto_disambiguation") - then - Lazy.force nonvars_uris - else begin - let dialog = gui#newUriDialog () in - dialog#uriChoiceTreeView#selection#set_mode selection_mode; - let model = new stringListModel dialog#uriChoiceTreeView in - let choices = ref None in - let nonvars = ref false in - dialog#uriChoiceDialog#set_title title; - dialog#uriChoiceLabel#set_text msg; - List.iter model#easy_append uris; - dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; - let return v = - choices := v; - dialog#uriChoiceDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ -> - return (Some (Lazy.force nonvars_uris)))); - ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ -> - Helm_registry.set_bool "matita.auto_disambiguation" true; - return (Some (Lazy.force nonvars_uris)))); - ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ -> - match model#easy_selection () with - | [] -> () - | uris -> return (Some uris))); - ignore (dialog#uriChoiceAbortButton#connect#clicked (fun _ -> return None)); - ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); - dialog#uriChoiceDialog#show (); - GtkThread.main (); - (match !choices with - | None -> raise MatitaTypes.No_choice - | Some uris -> uris) - end + let m = + GWindow.message_dialog + ~message ~use_markup ~message_type ~buttons ?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 () + in + ignore(m#connect#response + ~callback:(fun a -> GMain.Main.quit ();callback a)); + ignore(m#connect#close + ~callback:(fun _ -> GMain.Main.quit ();raise PopupClosed)); + 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 `YES in + let callback = + function + | `YES -> rc := `YES + | `NO -> rc := `NO + | `CANCEL -> rc := `CANCEL + | `DELETE_EVENT -> rc := `CANCEL + | `POPUPCLOSED -> rc := `CANCEL + in + let buttons = [`YES,`YES ; `NO,`NO ; `CANCEL,`CANCEL] in + popup_message_lowlevel + ~title ~message ~message_type:`WARNING ~callback ~buttons ?parent (); + !rc -let interactive_interp_choice ~(gui:#gui) choices = - (* TODO Zack implement interactive_interp_choice *) - MatitaTypes.warning - "'interactive_interp_choice' not implemented: returning 1st interpretation"; - [0] +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 () + with + | PopupClosed -> () -let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () = - let dialog = gui#newConfirmationDialog ~title ~msg () in + +let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false) + ?default () += + let dialog = gui#newEmptyDialog () in + dialog#emptyDialog#set_title title; + dialog#emptyDialogLabel#set_label message; let result = ref None in - let return r _ = - result := Some r; - dialog#confirmationDialog#destroy (); + let return r = + result := r; + dialog#emptyDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#emptyDialog#event#connect#delete (fun _ -> true)); + if multiline then begin (* multiline input required: use a TextView widget *) + let win = + GBin.scrolled_window ~width:400 ~height:150 ~hpolicy:`NEVER + ~vpolicy:`ALWAYS ~packing:dialog#emptyDialogVBox#add () + in + let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in + let buffer = view#buffer in + (match default with + | None -> () + | Some text -> + buffer#set_text text; + buffer#select_range buffer#start_iter buffer#end_iter); + view#misc#grab_focus (); + connect_button dialog#emptyDialogOkButton (fun _ -> + return (Some (buffer#get_text ()))) + end else begin (* monoline input required: use a TextEntry widget *) + let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in + (match default with + | None -> () + | Some text -> + entry#set_text text; + entry#select_region ~start:0 ~stop:max_int); + entry#misc#grab_focus (); + connect_button dialog#emptyDialogOkButton (fun _ -> + return (Some entry#text)) + end; + connect_button dialog#emptyDialogCancelButton (fun _ ->return None); + dialog#emptyDialog#show (); + GtkThread.main (); + (match !result with None -> raise Cancel | Some r -> r) + +type combo_status = Free of string | Locked of string + +let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "") + ~fields ~records () += + let fields = Array.of_list fields in + let fields_no = Array.length fields in + assert (fields_no > 0); + let dialog = gui#newRecordDialog () in + dialog#recordChoiceDialog#set_title title; + dialog#recordChoiceDialogLabel#set_label message; + let model = new recordModel dialog#recordChoiceTreeView in + dialog#recordChoiceTreeView#set_headers_visible true; + let combos = + Array.init fields_no + (fun _ -> GTree.store_of_list Gobject.Data.string ["a"; "b"; "c"]) + in + let (store, col) = combos.(0) in + store#set ~row:(store#append ()) ~column:col "uno"; + store#set ~row:(store#append ()) ~column:col "due"; + let toggles = Array.init fields_no (fun _ -> false) in + Array.iteri + (fun i f -> model#easy_append f i toggles.(i)) + fields; + let status = Array.map (fun s -> Free s) fields in + let record_no = ref None in + let return _ = + dialog#recordChoiceDialog#destroy (); GMain.Main.quit () in - ignore (dialog#confirmationDialogOkButton#connect#clicked (return true)); - ignore (dialog#confirmationDialogCancelButton#connect#clicked (return false)); - ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true)); - dialog#confirmationDialog#show (); + let fail _ = record_no := None; return () in + ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#recordChoiceOkButton (fun _ -> + match !record_no with None -> () | Some _ -> return ()); + connect_button dialog#recordChoiceCancelButton fail; +(* ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ -> + interp_no := Some (model#get_interp_no path); + return ())); + let selection = dialog#recordChoiceTreeView#selection in + ignore (selection#connect#changed (fun _ -> + match selection#get_selected_rows with + | [path] -> interp_no := Some (model#get_interp_no path) + | _ -> assert false)); *) + dialog#recordChoiceDialog#show (); GtkThread.main (); - (match !result with None -> assert false | Some r -> r) + (match !record_no with Some n -> n | _ -> raise MatitaTypes.Cancel)