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