X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=5ea3903835f05dafa4a83dc4c6b2711b84aa3a5d;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=c9b387178bc8cd1c780de9940d481013a1d035a0;hpb=d9394782ed9580f3565eb9b4682d8348aae6349e;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c9b387178..5ea390383 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -42,7 +42,7 @@ end
class console ~(buffer: GText.buffer) () =
object (self)
val error_tag = buffer#create_tag [ `FOREGROUND "red" ]
- val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
+ val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
val message_tag = buffer#create_tag []
val debug_tag = buffer#create_tag [ `FOREGROUND "#888888" ]
method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
@@ -58,6 +58,51 @@ 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 &&
+ status.MatitaTypes.proof_status = MatitaTypes.No_proof
+ 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 *)
@@ -156,8 +201,8 @@ class gui () =
connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
- connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None)));
- connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole)));
+ connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, [])));
+ connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, [])));
connect_button tbar#splitButton (tac (A.Split loc));
connect_button tbar#leftButton (tac (A.Left loc));
connect_button tbar#rightButton (tac (A.Right loc));
@@ -202,17 +247,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,7 +265,37 @@ class gui () =
(s ())#saveToFile ();
console#message ("'"^f^"' saved.\n");
in
- let newScript () = (s ())#reset (); disableSave () 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 ();
+ (s ())#template ();
+ disableSave ();
+ script_fname <- None
+ in
let cursor () =
source_buffer#place_cursor
(source_buffer#get_iter_at_mark (`NAME "locked"))
@@ -249,23 +313,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; GMain.Main.quit ()
+ | 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;
@@ -312,7 +389,14 @@ class gui () =
let script = MatitaScript.instance () in
script#reset ();
script#assignFileName file;
- script#loadFromFile ();
+ if not (Sys.file_exists file) then
+ begin
+ let oc = open_out file in
+ let template = MatitaMisc.input_file BuildTimeConf.script_template in
+ output_string oc template;
+ close_out oc
+ end;
+ script#loadFromFile ();
console#message ("'"^file^"' loaded.");
self#_enableSaveTo file