let ask_and_save_moo_if_needed parent fname status =
let save () =
- MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
+ let moo_fname = MatitaMisc.obj_file_of_script fname in
+ MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
if (MatitaScript.instance ())#eos &&
status.MatitaTypes.proof_status = MatitaTypes.No_proof
then
let get_devel_selected () =
match model#easy_mselection () with
| [[name;_]] -> MatitamakeLib.development_for_name name
- | _ -> assert false
+ | _ -> None
in
let refresh () =
while Glib.Main.pending () do
let fname = fileSel#fileSelectionWin#filename in
if Sys.file_exists fname then
begin
- if is_regular fname && not(_only_directory) then
+ if HExtlib.is_regular fname && not (_only_directory) then
return (Some fname)
- else if _only_directory && is_dir fname then
+ else if _only_directory && HExtlib.is_dir fname then
return (Some fname)
end
else
(tac_w_term (A.Transitivity (loc, hole)));
connect_button tbar#assumptionButton (tac (A.Assumption loc));
connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
- connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None)));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
MatitaGtkMisc.toggle_widget_visibility
~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
~check:main#tacticsBarMenuItem;
MatitaLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
(fun exn ->
- if Helm_registry.get_bool "matita.catch_top_level_exn" then
+ if not (Helm_registry.get_bool "matita.debug") then
MatitaLog.error (MatitaExcPp.to_string exn)
else raise exn);
(* script *)