snapshot, notably:

[helm.git] / helm / matita / matitaGtkMisc.ml

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index aebd2dbc9e536859514474c428abd2bdfeca7906..a0755371ba330d7b930da56748398a5f93f158e6 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -30,6 +30,18 @@ open MatitaTypes
 let connect_button (button: GButton.button) callback =
   ignore (button#connect#clicked 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 _ ->
     if check#active then win#show () else win#misc#hide ()));
@@ -219,7 +231,7 @@ let interactive_interp_choice ~(gui:#gui) choices =
   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 +244,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)