X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=0301b31f2e3981a02aad48493943af7a04c03223;hb=e6708c10ad615233628900902101216cc2f5baf5;hp=aebd2dbc9e536859514474c428abd2bdfeca7906;hpb=142d3076f2a4dc17d9045c2bba4d4b01eddfd008;p=helm.git

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index aebd2dbc9..0301b31f2 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
@@ -27,8 +27,35 @@ open Printf
 
 open MatitaTypes
 
-let connect_button (button: GButton.button) callback =
-  ignore (button#connect#clicked callback)
+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))
+
+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_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) =
   ignore (check#connect#toggled (fun _ ->
@@ -82,61 +109,6 @@ class stringListModel (tree_view: GTree.view) =
 
   end
 
-class interpModel =
-  let cols = new GTree.column_list in
-  let id_col = cols#add Gobject.Data.string in
-  let dsc_col = cols#add Gobject.Data.string in
-  let interp_no_col = cols#add Gobject.Data.int in
-  let tree_store = GTree.tree_store cols in
-  let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
-  let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
-  let id_view_col = GTree.view_column ~renderer:id_renderer () in
-  let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
-  fun tree_view choices ->
-    object
-      initializer
-        tree_view#set_model (Some (tree_store :> GTree.model));
-        ignore (tree_view#append_column id_view_col);
-        ignore (tree_view#append_column dsc_view_col);
-        let name_of_interp =
-          (* try to find a reasonable name for an interpretation *)
-          let idx = ref 0 in
-          fun interp ->
-            try
-              List.assoc "0" interp
-            with Not_found ->
-              incr idx; string_of_int !idx
-        in
-        tree_store#clear ();
-        let idx = ref ~-1 in
-        List.iter
-          (fun interp ->
-            incr idx;
-            let interp_row = tree_store#append () in
-            tree_store#set ~row:interp_row ~column:id_col
-              (name_of_interp interp);
-            tree_store#set ~row:interp_row ~column:interp_no_col !idx;
-            List.iter
-              (fun (id, dsc) ->
-                let row = tree_store#append ~parent:interp_row () in
-                tree_store#set ~row ~column:id_col id;
-                tree_store#set ~row ~column:dsc_col dsc;
-                tree_store#set ~row ~column:interp_no_col !idx)
-              interp)
-          choices
-
-      method get_interp_no tree_path =
-        let iter = tree_store#get_iter tree_path in
-        tree_store#get ~row:iter ~column:interp_no_col
-    end
-
-let is_var_uri s =
-  try
-    String.sub s (String.length s - 4) 4 = ".var"
-  with Invalid_argument _ -> false
-
-let non p x = not (p x)
-
 class type gui =
   object
     method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
@@ -145,81 +117,7 @@ class type gui =
     method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
   end
 
-let interactive_user_uri_choice
-  ~(gui:#gui) ~(selection_mode:[`SINGLE|`MULTIPLE]) ?(title = "")
-  ?(msg = "") ?(nonvars_button=false) uris
-=
-  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 :> Gtk.Tags.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#uriChoiceDialog#event#connect#delete (fun _ -> true));
-    connect_button dialog#uriChoiceConstantsButton (fun _ ->
-      return (Some (Lazy.force nonvars_uris)));
-    connect_button dialog#uriChoiceAutoButton (fun _ ->
-      Helm_registry.set_bool "matita.auto_disambiguation" true;
-      return (Some (Lazy.force nonvars_uris)));
-    connect_button dialog#uriChoiceSelectedButton (fun _ ->
-      match model#easy_selection () with
-      | [] -> ()
-      | uris -> return (Some uris));
-    connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
-    dialog#uriChoiceDialog#show ();
-    GtkThread.main ();
-    (match !choices with 
-    | None -> raise Cancel
-    | Some uris -> uris)
-  end
-
-let interactive_interp_choice ~(gui:#gui) choices =
-  assert (choices <> []);
-  let dialog = gui#newInterpDialog () in
-  let model = new interpModel dialog#interpChoiceTreeView choices in
-  let interp_len = List.length (List.hd choices) in
-  dialog#interpChoiceDialog#set_title "Interpretation choice";
-  dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
-  let interp_no = ref None in
-  let return _ =
-    dialog#interpChoiceDialog#destroy ();
-    GMain.Main.quit ()
-  in
-  let fail _ = interp_no := None; return () in
-  ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
-  connect_button dialog#interpChoiceOkButton (fun _ ->
-    match !interp_no with None -> () | Some _ -> return ());
-  connect_button dialog#interpChoiceCancelButton fail;
-  ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
-    interp_no := Some (model#get_interp_no path);
-    return ()));
-  let selection = dialog#interpChoiceTreeView#selection in
-  ignore (selection#connect#changed (fun _ ->
-    match selection#get_selected_rows with
-    | [path] ->
-        debug_print (sprintf "selection: %d" (model#get_interp_no path));
-        interp_no := Some (model#get_interp_no path)
-    | _ -> assert false));
-  dialog#interpChoiceDialog#show ();
-  GtkThread.main ();
-  (match !interp_no with Some row -> [row] | _ -> raise Cancel)
-
-let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
+let ask_confirmation ~(gui:#gui) ?(cancel = true) ?(title = "") ?(msg = "") () =
   let dialog = gui#newConfirmationDialog () in
   dialog#confirmationDialog#set_title title;
   dialog#confirmationDialogLabel#set_label msg;
@@ -232,6 +130,7 @@ let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
   ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
   connect_button dialog#confirmationDialogOkButton (return true);
   connect_button dialog#confirmationDialogCancelButton (return false);
+  if not cancel then dialog#confirmationDialogCancelButton#misc#hide ();
   dialog#confirmationDialog#show ();
   GtkThread.main ();
   (match !result with None -> assert false | Some r -> r)