X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=7b73eb112b5b2c5f517711da398f67ec1ca82054;hb=646ade789430669f4a6be3ecbf47d89fe865f132;hp=5ac24f8f66c9abdd262e6f477dd368188edc01e9;hpb=1b3aa3daa64f8b68aa08ff1c5458ba828398f897;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5ac24f8f6..7b73eb112 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -58,6 +58,50 @@ class console ~(buffer: GText.buffer) () =
| `Message -> self#message (s ^ "\n")
| `Warning -> self#warning (s ^ "\n")
end
+
+let clean_current_baseuri status =
+ try
+ let baseuri = MatitaTypes.get_string_option status "baseuri" in
+ MatitacleanLib.clean_baseuris [baseuri]
+ with MatitaTypes.Option_error _ -> ()
+
+let ask_and_save_moo_if_needed parent fname status =
+ let save () =
+ MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev
+ in
+ if (MatitaScript.instance ())#eos then
+ begin
+ let mooname =
+ MatitaMisc.obj_file_of_script fname
+ in
+ let rc =
+ MatitaGtkMisc.ask_confirmation
+ ~title:"A .moo can be generated"
+ ~message:(Printf.sprintf
+ "%s can be generated for %s.\nShould I generate it?"
+ mooname fname)
+ ~parent ()
+ in
+ let b =
+ match rc with
+ | `YES -> true
+ | `NO -> false
+ | `CANCEL -> raise MatitaTypes.Cancel
+ in
+ if b then
+ save ()
+ else
+ clean_current_baseuri status
+ end
+ else
+ clean_current_baseuri status
+
+let ask_unsaved parent =
+ MatitaGtkMisc.ask_confirmation
+ ~parent ~title:"Unsaved work!"
+ ~message:("Your work is unsaved!\n\n"^
+ "Do you want to save the script before exiting?")
+ ()
class gui () =
(* creation order _is_ relevant for windows placement *)
@@ -202,17 +246,6 @@ class gui () =
script_fname <- None;
self#main#saveMenuItem#misc#set_sensitive false
in
- let loadScript () =
- let script = s () in
- match self#chooseFile () with
- | Some f ->
- script#reset ();
- script#assignFileName f;
- script#loadFromFile ();
- console#message ("'"^f^"' loaded.\n");
- self#_enableSaveTo f
- | None -> ()
- in
let saveAsScript () =
let script = s () in
match self#chooseFile ~ok_not_exists:true () with
@@ -231,6 +264,31 @@ class gui () =
(s ())#saveToFile ();
console#message ("'"^f^"' saved.\n");
in
+ let loadScript () =
+ let script = s () in
+ let status = script#status in
+ try
+ if source_view#buffer#modified then
+ begin
+ match ask_unsaved main#toplevel with
+ | `YES -> saveScript ()
+ | `NO -> ()
+ | `CANCEL -> raise MatitaTypes.Cancel
+ end;
+ (match script_fname with
+ | None -> ()
+ | Some fname ->
+ ask_and_save_moo_if_needed main#toplevel fname status);
+ match self#chooseFile () with
+ | Some f ->
+ script#reset ();
+ script#assignFileName f;
+ script#loadFromFile ();
+ console#message ("'"^f^"' loaded.\n");
+ self#_enableSaveTo f
+ | None -> ()
+ with MatitaTypes.Cancel -> ()
+ in
let newScript () = (s ())#reset (); disableSave () in
let cursor () =
source_buffer#place_cursor
@@ -249,23 +307,36 @@ class gui () =
in
(* quit *)
self#setQuitCallback (fun () ->
+ let status = (MatitaScript.instance ())#status in
if source_view#buffer#modified then
begin
- let rc =
- MatitaGtkMisc.ask_confirmation
- ~parent:main#toplevel
- ~title:"Unsaved work!"
- ~message:("Your work is unsaved!\n\n"^
- "Do you want to save the script before exiting?")
- ()
- in
- match rc with
- | `YES -> saveScript ();
- if not source_view#buffer#modified then
- GMain.Main.quit ()
- | `NO -> GMain.Main.quit ()
- | `CANCEL -> ()
- end else GMain.Main.quit ());
+ let rc = ask_unsaved main#toplevel in
+ try
+ match rc with
+ | `YES -> saveScript ();
+ if not source_view#buffer#modified then
+ begin
+ (match script_fname with
+ | None -> ()
+ | Some fname ->
+ ask_and_save_moo_if_needed
+ main#toplevel fname status);
+ GMain.Main.quit ()
+ end
+ | `NO -> GMain.Main.quit ()
+ | `CANCEL -> raise MatitaTypes.Cancel
+ with MatitaTypes.Cancel -> ()
+ end
+ else
+ begin
+ (match script_fname with
+ | None -> clean_current_baseuri status
+ | Some fname ->
+ try
+ ask_and_save_moo_if_needed main#toplevel fname status;
+ GMain.Main.quit ()
+ with MatitaTypes.Cancel -> ())
+ end);
connect_button self#main#scriptAdvanceButton advance;
connect_button self#main#scriptRetractButton retract;
connect_button self#main#scriptTopButton top;