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
| `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.\n<i>Should I generate it?</i>"
+ 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 <b>unsaved</b>!\n\n"^
+ "<i>Do you want to save the script before exiting?</i>")
+ ()
class gui () =
(* creation order _is_ relevant for windows placement *)
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));
(* log *)
MatitaLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
- (fun exn ->
- MatitaLog.error
- (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
+ (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
(* script *)
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
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
(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"))
in
(* quit *)
self#setQuitCallback (fun () ->
- if
- MatitaGtkMisc.ask_confirmation
- ~parent:main#toplevel
- ~title:"Unsaved work!"
- ~message:("Your work is <b>unsaved</b>!\n\n"^
- "<i>Do you want to save the script before exiting?</i>")
- ()
- then
- (saveScript ();prerr_endline "SAVE";GMain.Main.quit ())
- else
- GMain.Main.quit ());
+ let status = (MatitaScript.instance ())#status in
+ if source_view#buffer#modified then
+ begin
+ 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;
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
projects / helm.git / blobdiff