From ee4ed24e86a1950e6cf168856d81eaf7dca17ee9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 6 Jan 2008 22:59:05 +0000 Subject: [PATCH] matita now works reasonably well, missing roots are still not graphically handled --- components/library/librarian.ml | 7 ++++--- matita/matitaScript.ml | 13 ++++++++----- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/components/library/librarian.ml b/components/library/librarian.ml index f16492394..72f8c50db 100644 --- a/components/library/librarian.ml +++ b/components/library/librarian.ml @@ -69,9 +69,10 @@ let find_root_for ~include_paths file = if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri); ensure_trailing_slash root, remove_trailing_slash uri, path - with Failure "find_in" as exn -> - HLog.error ("Unable to find: "^file); - raise exn + with Failure "find_in" -> + HLog.error ("Unable to find: "^file^"\nPaths explored:\n"); + List.iter (fun x -> HLog.error (" - "^x^"\n")) include_paths; + raise (NoRootFor file) ;; let baseuri_of_script ~include_paths file = diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index fbe8730c4..b0b020f01 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -114,9 +114,12 @@ let wrap_with_make include_paths g f x = (* we know that someone was able to include the .ma, get the baseuri * but was unable to get the compilation output 'xfilename' *) let root, buri, _, tgt = - Librarian.baseuri_of_script ~include_paths mafilename + try + Librarian.baseuri_of_script ~include_paths mafilename + with Librarian.NoRootFor _ -> raise exn in - if MatitacLib.Make.make root [tgt] then f x else raise exn + if MatitacLib.Make.make root [tgt] then f x + else raise (Failure ("Compiling: " ^ tgt)) ;; let eval_with_engine include_paths @@ -791,6 +794,7 @@ object (self) method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in + if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file]; HLog.debug ("evaluating: " ^ first_line s ^ " ..."); let entries, newtext, parsed_len = try @@ -935,7 +939,7 @@ object (self) HLog.debug ("Moving to " ^ Sys.getcwd ()) method saveToFile () = - if self#has_name && buffer#modified then + if self#has_name then let oc = open_out self#filename in output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); @@ -943,8 +947,7 @@ object (self) set_star false; buffer#set_modified false else - if self#has_name then HLog.debug "No need to save" - else HLog.error "Can't save, no filename selected" + HLog.error "Can't save, no filename selected" method private _saveToBackupFile () = if buffer#modified then -- 2.39.2