summaryrefslogtreecommitdiff
path: root/ide/coqide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml106
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