fixed save/exit stuff

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 038aa7fd13539a0cf7d1a6575d36dfa6628f556e..b8c9b91b3308b327ce14015248338a4ac0f9d17d 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -189,27 +189,68 @@ let popup_message
   GtkThread.main ();
   m#destroy () 
 
+let popup_message_lowlevel
+  ~title ~message ?(no_separator=true) ~callback ~message_type ~buttons
+  ?parent  ?(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.dialog 
+      ~no_separator 
+      ?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
+  let stock = 
+    match message_type with
+    | `WARNING -> `DIALOG_WARNING
+    | `INFO -> `DIALOG_INFO
+    | `ERROR ->`DIALOG_ERROR 
+    | `QUESTION -> `DIALOG_QUESTION
+  in
+  let image = GMisc.image ~stock ~icon_size:`DIALOG () in
+  let label = GMisc.label ~markup:message () in
+  let hbox = GPack.hbox ~spacing:10 () in
+  hbox#pack ~from:`START ~expand:true ~fill:true (image:>GObj.widget);
+  hbox#pack ~from:`START ~expand:true ~fill:true (label:>GObj.widget);
+  m#vbox#pack ~from:`START 
+    ~padding:20 ~expand:true ~fill:true (hbox:>GObj.widget);
+  List.iter (fun (x,y) -> m#add_button_stock x y) buttons;
+  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 ();
+  m#destroy () 
+
 
 let ask_confirmation ~title ~message ?parent () =
-  let rc = ref false in
+  let rc = ref `YES in
   let callback = 
-    function `YES -> rc := true | `NO -> rc := false | _ -> rc := false
+    function 
+    | `YES -> rc := `YES
+    | `NO -> rc := `NO
+    | `CANCEL -> rc := `CANCEL
+    | `DELETE_EVENT -> rc := `CANCEL
   in
-  let buttons = GWindow.Buttons.yes_no in
+  let buttons = [`CANCEL,`CANCEL ; `NO,`NO ; `YES,`YES] in
   try
-    popup_message ~title ~message ~message_type:`WARNING ~callback ~buttons
-      ?parent ();
+    popup_message_lowlevel 
+      ~title ~message ~message_type:`WARNING ~callback ~buttons ?parent ();
     !rc
   with
-  | PopupClosed -> false
+  | PopupClosed -> `CANCEL
 
 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 ()
+    popup_message 
+      ~title ~message ~message_type:`ERROR ~callback ~buttons ?parent ()
   with
   | PopupClosed -> ()
 

diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli
index 8a9f8d6fbbd763129fc0e823e063fb8ca2b338d6..7d4e289551cce5435cea4d1e7f6bcf8d9fedbc38 100644 (file)
--- a/helm/matita/matitaGtkMisc.mli
+++ b/helm/matita/matitaGtkMisc.mli
@@ -112,7 +112,7 @@ val ask_confirmation:
   title:string -> 
   message:string -> 
   ?parent:#GWindow.window_skel ->
-    unit -> bool
+    unit -> [`YES | `NO | `CANCEL]
 
 val report_error:
   title:string -> 

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index dc81593c54cddffc035aa0c30bc81e951e8e5d36..fa6059d1ea0eebb8139ac900f86e767074daeacd 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -251,17 +251,21 @@ class gui () =
       in
         (* quit *)
       self#setQuitCallback (fun () -> 
-        if 
-          MatitaGtkMisc.ask_confirmation 
-            ~parent:main#toplevel
-            ~title:"Unsaved work!" 
-            ~message:("Your work is <b>unsaved</b>!\n\n"^
-                 "<i>Do you want to save the script before exiting?</i>")
-            ()
-        then 
-          (saveScript ();prerr_endline "SAVE";GMain.Main.quit ())
-        else
-          GMain.Main.quit ());
+        if source_view#buffer#modified then
+          begin
+            let rc =  
+              MatitaGtkMisc.ask_confirmation 
+                ~parent:main#toplevel
+                ~title:"Unsaved work!" 
+                ~message:("Your work is <b>unsaved</b>!\n\n"^
+                     "<i>Do you want to save the script before exiting?</i>")
+                ()
+            in
+            match rc with
+            | `YES -> saveScript ();GMain.Main.quit ()
+            | `NO -> GMain.Main.quit ()
+            | `CANCEL -> ()
+          end else GMain.Main.quit ());
       connect_button self#main#scriptAdvanceButton advance;
       connect_button self#main#scriptRetractButton retract;
       connect_button self#main#scriptTopButton top;

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 043fc31e43d45825f621dd485494645751b687f6..0d6bfedee5ea0ec6d6ef68a3e904ad6389be5580 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -298,7 +298,7 @@ object (self)
   val mutable filename = std_filename
   
   initializer 
-    ignore(GMain.Timeout.add ~ms:20000 
+    ignore(GMain.Timeout.add ~ms:30000 
        ~callback:(fun _ -> self#_saveToBackuptFile ();true));
     ignore(buffer#connect#modified_changed 
        (fun _ -> if buffer#modified then 
@@ -414,12 +414,15 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     buffer#set_modified false
   
   method private _saveToBackuptFile () =
-    let f = filename ^ "~" in 
-    let oc = open_out f in
-    output_string oc (buffer#get_text ~start:buffer#start_iter
-                        ~stop:buffer#end_iter ());
-    close_out oc;
-    MatitaLog.debug ("backup file " ^ f ^ " saved")
+    if buffer#modified then
+      begin
+        let f = filename ^ "~" in 
+        let oc = open_out f in
+        output_string oc (buffer#get_text ~start:buffer#start_iter
+                            ~stop:buffer#end_iter ());
+        close_out oc;
+        MatitaLog.debug ("backup " ^ f ^ " saved")                    
+      end
   
   method private goto_top =
     MatitaSync.time_travel ~present:self#status ~past:init;