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
~title:"A .moo can be generated"
~message:(Printf.sprintf
"%s can be generated for %s.\n<i>Should I generate it?</i>"
- mooname fname)
+ (Filename.basename mooname) (Filename.basename fname))
~parent ()
in
let b =
~default:BuildTimeConf.default_font_size "matita.font_size"
in
let source_buffer = source_view#source_buffer in
-(* let _ =
- source_view#event#connect#selection_clear (fun _ ->
- prerr_endline "source_view: selection clear";
- false)
- in *)
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
(*~comments:"comments"*)
~copyright:"Copyright (C) 2005, the HELM team"
~license:(String.concat "\n" (parse_txt_file "LICENSE"))
- (*?logo:GdkPixbuf.pixbuf*)
- (*?logo_icon_name:string*)
+ ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png"))
~name:"Matita"
~version:BuildTimeConf.version
~website:"http://helm.cs.unibo.it"
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
(* toolbar *)
let module A = GrafiteAst in
let hole = CicNotationPt.UserInput in
- let loc = Disambiguate.dummy_floc in
+ let loc = DisambiguateTypes.dummy_floc in
let tac ast _ =
if (MatitaScript.instance ())#onGoingProof () then
(MatitaScript.instance ())#advance
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, None, [])));
- connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, [])));
+ 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));
(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))); (* ALB *)
+ connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
MatitaGtkMisc.toggle_widget_visibility
~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
~check:main#tacticsBarMenuItem;
(* log *)
MatitaLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
- (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
+ (fun exn ->
+ if not (Helm_registry.get_bool "matita.debug") then
+ MatitaLog.error (MatitaExcPp.to_string exn)
+ else raise exn);
(* script *)
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
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 ->
+ 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);
script#reset ();
script#assignFileName f;
source_view#source_buffer#begin_not_undoable_action ();
let selection = dialog#interpChoiceTreeView#selection in
ignore (selection#connect#changed (fun _ ->
match selection#get_selected_rows with
- | [path] ->
- MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path));
- interp_no := Some (model#get_interp_no path)
+ | [path] -> interp_no := Some (model#get_interp_no path)
| _ -> assert false));
dialog#interpChoiceDialog#show ();
GtkThread.main ();