]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/binaries/probe/engine.ml
arithmetics for λδ
[helm.git] / matita / components / binaries / probe / engine.ml
index c25201508f8a3660a47251f23fea353f2afc5899..8a8a74ac545b644aedb95915d0271b222d764150 100644 (file)
@@ -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