X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2FmatitaList.ml;h=95250b26c13a65888f4af69635227353b7afcd1c;hb=ea99a55173ebdcfe60f3b3d6f6c979f5d7785d48;hp=ee6cb417afeede5fe163439af7b57352e68c7aa7;hpb=9722a8d7b63e62f2b5b00de008304485371f7bf6;p=helm.git

diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml
index ee6cb417a..95250b26c 100644
--- a/matita/components/binaries/probe/matitaList.ml
+++ b/matita/components/binaries/probe/matitaList.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 A = Array
@@ -21,75 +21,76 @@ module H  = HExtlib
 
 module O = Options
 module E = Engine
+module X = Error
 
 let chop_extension file =
-   try F.chop_extension file
-   with Invalid_argument("Filename.chop_extension") -> file
+  try F.chop_extension file
+  with Invalid_argument _ -> file
 
 let script devel = chop_extension devel ^ ".ma"
 
 let src_exists path = !O.no_devel || Y.file_exists path
 
-let is_obj base path = 
-   if H.is_regular (F.concat base path) then
-      F.check_suffix path ".con.ng" ||
-      F.check_suffix path ".ind.ng" ||
-      F.check_suffix path ".var.ng"
+let is_obj base path =
+  if H.is_regular (F.concat base path) then
+    F.check_suffix path ".con.ng" ||
+    F.check_suffix path ".ind.ng" ||
+    F.check_suffix path ".var.ng"
   else false
 
-let is_src base path = 
-   H.is_regular (F.concat base path) &&
-   F.check_suffix path ".ng"
+let is_src base path =
+  H.is_regular (F.concat base path) &&
+  F.check_suffix path ".ng"
 
 let is_dir base path =
-   H.is_dir (F.concat base path)
+  H.is_dir (F.concat base path)
 
 let is_script devel =
-   src_exists (script devel)
+  src_exists (script devel)
 
 let mk_file path =
-   if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
-   else path ^ ".ng"
+  if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
+  else path ^ ".ng"
 
 let add_obj path =
-   let path = F.chop_extension path in   
-   let str = F.concat "cic:" path in
-   O.objs := US.add (U.uri_of_string str) !O.objs
+  let path = F.chop_extension path in
+  let str = F.concat "cic:" path in
+  O.objs := US.add (U.uri_of_string str) !O.objs
 
 let add_src devel path =
-   let path = F.chop_extension path in   
-   let str = F.concat "cic:" path ^ "/" in
-   O.srcs := US.add (U.uri_of_string str) !O.srcs;
-   E.mac (script devel)
+  let path = F.chop_extension path in
+  let str = F.concat "cic:" path ^ "/" in
+  O.srcs := US.add (U.uri_of_string str) !O.srcs;
+  E.mac (script devel)
 
 let add_remove base path =
-   O.remove := F.concat base path :: !O.remove
+  O.remove := F.concat base path :: !O.remove
 
 let rec scan_entry inner base devel path =
-(*   Printf.eprintf "%b %s %s%!\n" inner devel path; *)
-   if is_obj base path && inner then add_obj path else
-   if is_src base path && is_script devel then add_src devel path else 
-   if is_dir base path && is_script devel then scan_dir true base devel path else
-   if is_dir base path && src_exists devel then scan_dir false base devel path else
-   add_remove base path
+(*  Printf.eprintf "%b %s %s%!\n" inner devel path; *)
+  if is_obj base path && inner then add_obj path else
+  if is_src base path && is_script devel then add_src devel path else
+  if is_dir base path && is_script devel then scan_dir true base devel path else
+  if is_dir base path && src_exists devel then scan_dir false base devel path else
+  add_remove base path
 
 and scan_dir inner base devel path =
-   let files = Y.readdir (F.concat base path) in
-   let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in
-   A.iter (map base) files
+  let files = Y.readdir (F.concat base path) in
+  let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in
+  A.iter (map base) files
 
 let from_uri base devel uri =
-   O.no_devel := devel = "";
-   let str = U.string_of_uri uri in
-   let i = S.index str '/' in
-   let protocol = S.sub str 0 i in
-   if protocol = "cic:" then 
-      let path = S.sub str (succ i) (S.length str - succ i) in
-      let file = mk_file path in
-      if Y.file_exists (F.concat base file) then
-         scan_entry (is_script devel) base devel file 
-      else E.missing path
-   else E.unsupported protocol
+  O.no_devel := devel = "";
+  let str = U.string_of_uri uri in
+  let i = S.index str '/' in
+  let protocol = S.sub str 0 i in
+  if protocol = "cic:" then
+    let path = S.sub str (succ i) (S.length str - succ i) in
+    let file = mk_file path in
+    if Y.file_exists (F.concat base file) then
+      scan_entry (is_script devel) base devel file
+    else X.missing path
+  else X.unsupported protocol
 
 let from_string base devel s =
-   from_uri base devel (U.uri_of_string s)
+  from_uri base devel (U.uri_of_string s)