X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2Fengine.ml;h=8a8a74ac545b644aedb95915d0271b222d764150;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=c25201508f8a3660a47251f23fea353f2afc5899;hpb=9722a8d7b63e62f2b5b00de008304485371f7bf6;p=helm.git diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index c25201508..8a8a74ac5 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module F = Filename @@ -34,7 +34,7 @@ let out_int i = P.printf "%u\n" i let out_length uris = out_int (US.cardinal uris) let out_uris uris = - let map uri = P.printf "%s\n" (U.string_of_uri uri) in + let map uri = P.printf "%S\n" (U.string_of_uri uri) in US.iter map uris let is_registry str = @@ -43,14 +43,14 @@ let is_registry str = let get_uri str = let str = H.normalize_path str in let dir, file = - if H.is_regular str && F.check_suffix str ".ma" + if H.is_regular str && F.check_suffix str ".ma" then F.dirname str, F.chop_extension (F.basename str) else if H.is_dir str then str, "" else missing str in let rec aux bdir file = match B.find_roots_in_dir bdir with - | [root] -> - let buri = L.assoc "baseuri" (B.load_root_file root) in + | [root] -> + let buri = L.assoc "baseuri" (B.load_root_file root) in F.concat bdir file, F.concat buri file | roots -> if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir roots else