From: Enrico Tassi Date: Tue, 28 Jun 2005 10:58:10 +0000 (+0000) Subject: added "are you sure you want to quit with usaved script?" X-Git-Tag: INDEXING_NO_PROOFS~28 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=030d34e0dc025b94d7f0459eff0a84e2ac108b73;p=helm.git added "are you sure you want to quit with usaved script?" --- diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index d45452a52..b53bbd209 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -23,6 +23,7 @@ * http://helm.cs.unibo.it/ *) +exception PopupClosed open Printf open MatitaTypes @@ -166,24 +167,51 @@ class type gui = method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end -let ask_confirmation ~(gui:#gui) ?(cancel = true) ?(title = "") ?(msg = "") () = - let dialog = gui#newConfirmationDialog () in - dialog#confirmationDialog#set_title title; - dialog#confirmationDialogLabel#set_label msg; - let result = ref None in - let return r _ = - result := Some r; - dialog#confirmationDialog#destroy (); - GMain.Main.quit () +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 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 () + + +let ask_confirmation ~title ~message ?parent () = + let rc = ref false in + let callback = + function `YES -> rc := true | `NO -> rc := false | _ -> rc := false in - 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) - + let buttons = GWindow.Buttons.yes_no in + try + popup_message ~title ~message ~message_type:`WARNING ~callback ~buttons + ?parent (); + !rc + with + | PopupClosed -> false + +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_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () = let dialog = gui#newEmptyDialog () in dialog#emptyDialog#set_title title; diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index d18ff281d..8a9f8d6fb 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -107,13 +107,18 @@ class type gui = (** {3 Dialogs} *) - (** @return true if user hit "ok" button, false if user hit "cancel" button - * @param cancel if set to true a cancel button is shown to the user, otherwise - * it is not (and indeed the function will return true). Defaults to true *) + (* @param parent to center the window on it *) val ask_confirmation: - gui:#gui -> - ?cancel:bool -> ?title:string -> ?msg:string -> unit -> - bool + title:string -> + message:string -> + ?parent:#GWindow.window_skel -> + unit -> bool + +val report_error: + title:string -> + message:string -> + ?parent:#GWindow.window_skel -> + unit -> unit (** @param multiline (default: false) if true a TextView widget will be used * for prompting the user otherwise a TextEntry widget will be diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 1e2b54826..dc81593c5 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -183,8 +183,6 @@ class gui () = | false -> self#main#toplevel#unfullscreen ()) ~check:self#main#fullscreenMenuItem; self#main#fullscreenMenuItem#set_active false; - (* quit *) - self#setQuitCallback (fun () -> exit 0); (* log *) MatitaLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := @@ -251,6 +249,19 @@ class gui () = connect_key self#sourceView#event ~modifiers:[`CONTROL] ~stop:true sym f in + (* quit *) + self#setQuitCallback (fun () -> + if + MatitaGtkMisc.ask_confirmation + ~parent:main#toplevel + ~title:"Unsaved work!" + ~message:("Your work is unsaved!\n\n"^ + "Do you want to save the script before exiting?") + () + then + (saveScript ();prerr_endline "SAVE";GMain.Main.quit ()) + else + GMain.Main.quit ()); connect_button self#main#scriptAdvanceButton advance; connect_button self#main#scriptRetractButton retract; connect_button self#main#scriptTopButton top; @@ -356,8 +367,9 @@ class gui () = keyBindingBoxes method setQuitCallback callback = - ignore (main#toplevel#connect#destroy callback); ignore (main#quitMenuItem#connect#activate callback); + ignore (main#toplevel#event#connect#delete + (fun _ -> callback ();true)); self#addKeyBinding GdkKeysyms._q callback method chooseFile ?(ok_not_exists = false) () = diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 5b1f4d5b3..7b25b375c 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -350,9 +350,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in let toplevel = win#toplevel in let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in - let fail msg = - ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ()) - ~title:"Cic browser" ~msg ~cancel:false ()); + let fail message = + MatitaGtkMisc.report_error ~title:"Cic browser" ~message () in let tags = [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");