bugfix update in basic_2

[helm.git] / matita / components / library / librarian.ml

diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml
index 791141b88c23f4233f51f4b990ac543b07f49348..13fccbfa25479beee0e52634cc75ebddf7dbf2ec 100644 (file)
--- a/matita/components/library/librarian.ml
+++ b/matita/components/library/librarian.ml
@@ -23,6 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
+exception FileNotFound of string
 exception NoRootFor of string
 
 let absolutize path =
@@ -83,7 +84,7 @@ let find_root_for ~include_paths file =
        HLog.error ("We are in: " ^ Sys.getcwd ());
        HLog.error ("Unable to find: "^file^"\nPaths explored:");
        List.iter (fun x -> HLog.error (" - "^x)) include_paths;
-       raise (NoRootFor file)
+       raise (FileNotFound file)
    in
    let path = find_path_for file in   
    let path = absolutize path in
@@ -110,8 +111,12 @@ let find_root_for ~include_paths file =
 
 let mk_baseuri root extra =
   let chop name = 
+(* FG: there is no reason why matita should edit just matita files
+       matita's editor is good on its own and has interesting facilities
+       including predefined virtuals
     assert(Filename.check_suffix name ".ma" ||
       Filename.check_suffix name ".mma");
+*)    
     try Filename.chop_extension name
     with Invalid_argument "Filename.chop_extension" -> name
   in
@@ -128,7 +133,7 @@ let baseuri_of_script ~include_paths file =
     match l1, l2 with
     | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2
     | l,[] -> l
-    | _ -> raise (NoRootFor (file ^" "^path^" "^root))
+    | _ -> assert false
   in
   let extra_buri = substract lpath lroot in
   let extra = String.concat "/" extra_buri in