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));
| false -> self#main#toplevel#unfullscreen ())
~check:self#main#fullscreenMenuItem;
self#main#fullscreenMenuItem#set_active false;
- (* quit *)
- self#setQuitCallback (fun () -> exit 0);
(* 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
connect_key self#sourceView#event
~modifiers:[`CONTROL] ~stop:true sym f
in
+ (* quit *)
+ self#setQuitCallback (fun () ->
+ if source_view#buffer#modified then
+ begin
+ let rc =
+ 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>")
+ ()
+ 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 ());
connect_button self#main#scriptAdvanceButton advance;
connect_button self#main#scriptRetractButton retract;
connect_button self#main#scriptTopButton top;
keyBindingBoxes
method setQuitCallback callback =
- ignore (main#toplevel#connect#destroy callback);
ignore (main#quitMenuItem#connect#activate callback);
+ ignore (main#toplevel#event#connect#delete
+ (fun _ -> callback ();true));
self#addKeyBinding GdkKeysyms._q callback
method chooseFile ?(ok_not_exists = false) () =