method debug s = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
method clear () =
buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
- method log_callback (tag: MatitaLog.log_tag) s =
+ method log_callback (tag: HLog.log_tag) s =
match tag with
| `Debug -> self#debug (s ^ "\n")
| `Error -> self#error (s ^ "\n")
let clean_current_baseuri status =
try
let baseuri = MatitaTypes.get_string_option status "baseuri" in
- MatitacleanLib.clean_baseuris [baseuri]
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir [baseuri]
with MatitaTypes.Option_error _ -> ()
let ask_and_save_moo_if_needed parent fname status =
+ let basedir = Helm_registry.get "matita.basedir" in
let save () =
- let moo_fname = MatitacleanLib.obj_file_of_script fname in
- MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
+ let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in
+ GrafiteMarshal.save_moo moo_fname
+ status.MatitaTypes.moo_content_rev in
if (MatitaScript.current ())#eos &&
status.MatitaTypes.proof_status = MatitaTypes.No_proof
then
begin
- let mooname =
- MatitacleanLib.obj_file_of_script fname
- in
+ let mooname = MatitaMisc.obj_file_of_script ~basedir fname in
let rc =
MatitaGtkMisc.ask_confirmation
~title:"A .moo can be generated"
newDevel#toplevel#misc#hide()
end
else
- MatitaLog.error ("The selected root does not contain " ^
+ HLog.error ("The selected root does not contain " ^
match next_devel_must_contain with
| Some x -> x
| _ -> assert false));
~check:main#fullscreenMenuItem;
main#fullscreenMenuItem#set_active false;
(* log *)
- MatitaLog.set_log_callback self#console#log_callback;
+ HLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
(fun exn ->
if not (Helm_registry.get_bool "matita.debug") then
source_buffer#place_cursor
(source_buffer#get_iter (`OFFSET x'));
end;
- MatitaLog.error msg
+ HLog.error msg
else raise exn);
(* script *)
ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
| None ->
- MatitaLog.warn (sprintf "can't load language file %s"
+ HLog.warn (sprintf "can't load language file %s"
BuildTimeConf.lang_file)
| Some matita_lang ->
source_buffer#set_language matita_lang;