snapshot:

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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 874c75c590a8a9ee04d73380dae16ea553cb7152..aebd2dbc9e536859514474c428abd2bdfeca7906 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -27,6 +27,9 @@ open Printf
 
 open MatitaTypes
 
+let connect_button (button: GButton.button) callback =
+  ignore (button#connect#clicked callback)
+
 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 +145,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 +171,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 +200,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 ()));
@@ -228,8 +230,8 @@ 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);
   dialog#confirmationDialog#show ();
   GtkThread.main ();
   (match !result with None -> assert false | Some r -> r)
@@ -252,15 +254,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)