Imported Upstream version 8.3pl1upstream/8.3pl1

1 files changed, 73 insertions, 33 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 08452fe2..fdf33c39 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coqide.ml 13708 2010-12-13 14:49:29Z gmelquio $ *)
 
 open Preferences
 open Vernacexpr
@@ -251,27 +251,31 @@ let break () =
     end
 
 let do_if_not_computing text f x =
-  if Mutex.try_lock coq_computing then
-    let threaded_task () =
-      prerr_endline "Getting lock";
-      try
-        f x;
-        prerr_endline "Releasing lock";
-        Mutex.unlock coq_computing;
-      with e ->
-        prerr_endline "Releasing lock (on error)";
-        Mutex.unlock coq_computing;
-        raise e
-    in
-      prerr_endline ("Launching thread " ^ text);
-      ignore (Glib.Timeout.add ~ms:300 ~callback:
-                  (fun () -> if Mutex.try_lock coq_computing
-                             then (Mutex.unlock coq_computing; false)
-                             else (pbar#pulse (); true)));
-      ignore (Thread.create threaded_task ())
-  else
-    prerr_endline
-      "Discarded order (computations are ongoing)"
+  let threaded_task () =
+    (* Beware: mutexes must be locked and unlocked in the same thread
+       on at least FreeBSD (see bug #2431) *)
+    if Mutex.try_lock coq_computing then
+      begin
+        prerr_endline "Getting lock";
+        try
+          f x;
+          prerr_endline "Releasing lock";
+          Mutex.unlock coq_computing;
+        with e ->
+          prerr_endline "Releasing lock (on error)";
+          Mutex.unlock coq_computing;
+          raise e
+      end
+    else
+      prerr_endline
+        "Discarded order (computations are ongoing)"
+  in
+  prerr_endline ("Launching thread " ^ text);
+  ignore (Glib.Timeout.add ~ms:300 ~callback:
+            (fun () -> if Mutex.try_lock coq_computing
+              then (Mutex.unlock coq_computing; false)
+              else (pbar#pulse (); true)));
+  ignore (Thread.create threaded_task ())
 
 (* XXX - 1 appel *)
 let kill_input_view i =
@@ -282,15 +286,59 @@ let kill_input_view i =
     v.proof_view#destroy ();
     v.message_view#destroy ();
     session_notebook#remove_page i
+
+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
+
 (*
 (* XXX - beaucoups d'appels, a garder *)
 let get_current_view =
   focused_session
  *)
 let remove_current_view_page () =
-  let c = session_notebook#current_page in
-    kill_input_view c
-
+  let do_remove () =
+    let c = session_notebook#current_page in
+      kill_input_view 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 ()
+        | _ -> ()
 
 (* Reset this to None on page change ! *)
 let (last_completion:(string*int*int*bool) option ref) = ref None
@@ -383,14 +431,6 @@ let activate_input i =
   set_active_view i;
   prerr_endline "exiting activate_input"
 
-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