let initial_statuses current baseuri =
let status = new MatitaEngine.status baseuri in
(match current with
- Some current ->
- NCicLibrary.time_travel status;
+ Some current -> NCicLibrary.time_travel status;
(*
(* MATITA 1.0: there is a known bug in invalidation; temporary fix here *)
NCicEnvironment.invalidate () *)
| None -> ());
status
in
-let read_include_paths file =
- try
- let root, _buri, _fname, _tgt =
- Librarian.baseuri_of_script ~include_paths:[] file in
- let includes =
- try
- Str.split (Str.regexp " ")
- (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
- with Not_found -> []
- in
- let rc = root :: includes in
- List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
- []
-in
let default_buri = "cic:/matita/tests" in
let default_fname = ".unnamed.ma" in
object (self)
List.iter (fun o -> o status) observers
method activate =
+ NCicLibrary.replace self#status;
self#notify
method loadFromFile f =
let f = Librarian.absolutize file in
tab_label#set_text (Filename.basename f);
filename_ <- Some f;
- include_paths_ <- read_include_paths f;
+ include_paths_ <- MatitaEngine.read_include_paths ~include_paths:[] f;
self#reset_buffer
method set_star b =
method private _saveToBackupFile () =
if buffer#modified then
begin
- let f = self#filename in
+ let f = self#filename ^ "~" in
let oc = open_out f in
output_string oc (buffer#get_text ~start:buffer#start_iter
~stop:buffer#end_iter ());
close_out oc;
- HLog.debug ("backup " ^ f ^ " saved")
+ HLog.debug ("backup " ^ f ^ " saved")
end
method private reset_buffer =