X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=a0755371ba330d7b930da56748398a5f93f158e6;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=874c75c590a8a9ee04d73380dae16ea553cb7152;hpb=190e42f1030ea3d459c4040bb0e8503a7c096820;p=helm.git

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 874c75c59..a0755371b 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -27,6 +27,21 @@ open Printf
 
 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 ()));
@@ -142,8 +157,6 @@ class type gui =
     method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
   end
 
-exception Cancel
-
 let interactive_user_uri_choice
   ~(gui:#gui) ~(selection_mode:[`SINGLE|`MULTIPLE]) ?(title = "")
   ?(msg = "") ?(nonvars_button=false) uris
@@ -170,16 +183,16 @@ let interactive_user_uri_choice
       GMain.Main.quit ()
     in
     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
-    ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ ->
-      return (Some (Lazy.force nonvars_uris))));
-    ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ ->
+    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))));
-    ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ ->
+      return (Some (Lazy.force nonvars_uris)));
+    connect_button dialog#uriChoiceSelectedButton (fun _ ->
       match model#easy_selection () with
       | [] -> ()
-      | uris -> return (Some uris)));
-    ignore (dialog#uriChoiceAbortButton#connect#clicked (fun _ -> return None));
+      | uris -> return (Some uris));
+    connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
     dialog#uriChoiceDialog#show ();
     GtkThread.main ();
     (match !choices with 
@@ -199,10 +212,11 @@ let interactive_interp_choice ~(gui:#gui) choices =
     dialog#interpChoiceDialog#destroy ();
     GMain.Main.quit ()
   in
+  let fail _ = interp_no := None; return () in
   ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
-  ignore (dialog#interpChoiceOkButton#connect#clicked (fun _ ->
-    match !interp_no with None -> () | Some _ -> return ()));
-  ignore (dialog#interpChoiceCancelButton#connect#clicked return);
+  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 ()));
@@ -217,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;
@@ -228,8 +242,9 @@ let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
     GMain.Main.quit ()
   in
   ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
-  ignore (dialog#confirmationDialogOkButton#connect#clicked (return true));
-  ignore (dialog#confirmationDialogCancelButton#connect#clicked (return false));
+  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)
@@ -252,15 +267,15 @@ let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
     in
     let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in
     view#misc#grab_focus ();
-    ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ ->
-      return (Some (view#buffer#get_text ()))))
+    connect_button dialog#emptyDialogOkButton (fun _ ->
+      return (Some (view#buffer#get_text ())))
   end else begin (* monoline input required: use a TextEntry widget *)
     let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in
     entry#misc#grab_focus ();
-    ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ ->
-      return (Some entry#text)))
+    connect_button dialog#emptyDialogOkButton (fun _ ->
+      return (Some entry#text))
   end;
-  ignore (dialog#emptyDialogCancelButton#connect#clicked (fun _ ->return None));
+  connect_button dialog#emptyDialogCancelButton (fun _ ->return None);
   dialog#emptyDialog#show ();
   GtkThread.main ();
   (match !result with None -> raise Cancel | Some r -> r)