Avoid silent loss of data when closing an unsaved buffer.

Patch by David Baelde.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13707 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 46 insertions, 10 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 42680dffc..0f535cfef 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -258,9 +258,53 @@ let do_if_not_computing text f x =
       prerr_endline
         "Discarded order (computations are ongoing)"
 
+let warning msg =
+  GToolbox.message_box ~title:"Warning"
+    ~icon:(let img = GMisc.image () in
+	     img#set_stock `DIALOG_WARNING;
+	     img#set_icon_size `DIALOG;
+	     img#coerce)
+    msg
+
 let remove_current_view_page () =
-  let c = session_notebook#current_page in
-  session_notebook#remove_page c
+  let do_remove () =
+    let c = session_notebook#current_page in
+      session_notebook#remove_page c
+  in
+  let current = session_notebook#current_term in
+    if current.script#buffer#modified then
+      match GToolbox.question_box ~title:"Close"
+              ~buttons:["Save Buffer and Close";
+                        "Close without Saving";
+                        "Don't Close"]
+              ~default:0
+              ~icon:(let img = GMisc.image () in
+                       img#set_stock `DIALOG_WARNING;
+                       img#set_icon_size `DIALOG;
+                       img#coerce)
+              "This buffer has unsaved modifications"
+      with
+        | 1 ->
+            begin match current.analyzed_view#filename with
+              | None ->
+                  begin match select_file_for_save ~title:"Save file" () with
+                    | None -> ()
+                    | Some f ->
+                        if current.analyzed_view#save_as f then begin
+                          flash_info ("File " ^ f ^ " saved") ;
+                          do_remove ()
+                        end else
+                          warning  ("Save Failed (check if " ^ f ^ " is writable)")
+                  end
+              | Some f ->
+                  if current.analyzed_view#save f then begin
+                    flash_info ("File " ^ f ^ " saved") ;
+                    do_remove ()
+                  end else
+                    warning  ("Save Failed (check if " ^ f ^ " is writable)")
+            end
+        | 2 -> do_remove ()
+        | _ -> ()
 
 
 let print_items = [
@@ -364,14 +408,6 @@ exception Found
 (* For find_phrase_starting_at *)
 exception Stop of int
 
-let warning msg =
-  GToolbox.message_box ~title:"Warning"
-    ~icon:(let img = GMisc.image () in
-	     img#set_stock `DIALOG_WARNING;
-	     img#set_icon_size `DIALOG;
-	     img#coerce)
-    msg
-
 let apply_tag (buffer:GText.buffer) orig off_conv from upto sort =
   let conv_and_apply start stop tag =
     let start = orig#forward_chars (off_conv from) in