X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flibrary%2Flibrarian.ml;fp=matita%2Fcomponents%2Flibrary%2Flibrarian.ml;h=9ffde2b87d0444c6d9ad012b4e26e9641d45a513;hb=2e17165ef9e63367cc290ad555145b4c22a4582b;hp=791141b88c23f4233f51f4b990ac543b07f49348;hpb=748cd8bf9d30cf3fb07d7a4dde32e41b2dbfe5fa;p=helm.git diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml index 791141b88..9ffde2b87 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 = @@ -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 @@ -128,7 +129,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