diff options
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 106 |
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 |