matita now works reasonably well,

missing roots are still not graphically handled

diff --git a/components/library/librarian.ml b/components/library/librarian.ml
index f1649239460939d2915f226bc38b90312df3e82d..72f8c50db9fcfca38e13070a79271e26206bc771 100644 (file)
--- 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 fbe8730c43bfd4f90b156b3e7457488ba575ed8d..b0b020f0115bd8e7ffe3ff39dc798948a326fdf0 100644 (file)
--- 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