X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flibrary%2Flibrarian.ml;h=bcb84fd6791f9f142defb474dd33f6c8c83958cd;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hp=7d159af2467a26cddfac6ef9e4863a42961db0d4;hpb=d8c17db3c787f3ea964bbcd3b27427ca44b356d0;p=helm.git

diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml
index 7d159af24..bcb84fd67 100644
--- 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 =
@@ -40,7 +41,7 @@ let find_root path =
   let path = absolutize path in
   let paths = List.rev (Str.split (Str.regexp "/") path) in
   let rec build = function
-    | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
+    | _he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
     | [] -> ["/"]
   in
   let paths = List.map HExtlib.normalize_path (build paths) in
@@ -77,20 +78,13 @@ let load_root_file rootpath =
 
 let find_root_for ~include_paths file = 
   let include_paths = "" :: Sys.getcwd () :: include_paths in
-   let rec find_path_for file =
+   let find_path_for file =
       try HExtlib.find_in include_paths file
       with Failure "find_in" -> 
-         if Filename.check_suffix file ".ma" then begin
-            let mma = Filename.chop_suffix file ".ma" ^ ".mma" in
-            HLog.warn ("We look for: " ^ mma);
-            let path = find_path_for mma in
-	    Filename.chop_suffix path ".mma" ^ ".ma"
-         end else begin
-            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)
-         end         
+       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 (FileNotFound file)
    in
    let path = find_path_for file in   
    let path = absolutize path in
@@ -117,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
@@ -135,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