matita/components/binaries/probe/engine.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module F = Filename
  13 module L = List
  14 module P = Printf
  15
  16 module U  = NUri
  17 module US = U.UriSet
  18 module B  = Librarian
  19 module H  = HExtlib
  20
  21 let unsupported protocol =
  22    failwith (P.sprintf "probe: unsupported protocol: %s" protocol)
  23
  24 let missing path =
  25    failwith (P.sprintf "probe: missing path: %s" path)
  26
  27 let unrooted path =
  28    failwith (P.sprintf "probe: missing root: %s" path)
  29
  30 let out_int i = P.printf "%u\n" i
  31
  32 let out_length uris = out_int (US.cardinal uris)
  33
  34 let out_uris uris =
  35    let map uri = P.printf "%s\n" (U.string_of_uri uri) in
  36    US.iter map uris
  37
  38 let is_registry str =
  39    F.check_suffix str ".conf.xml"
  40
  41 let get_uri str =
  42   let str = H.normalize_path str in
  43   let dir, file =
  44       if H.is_regular str && F.check_suffix str ".ma"
  45       then F.dirname str, F.chop_extension (F.basename str)
  46       else if H.is_dir str then str, ""
  47       else missing str
  48    in
  49    let rec aux bdir file = match B.find_roots_in_dir bdir with
  50       | [root] ->
  51          let buri = L.assoc "baseuri" (B.load_root_file root) in
  52          F.concat bdir file, F.concat buri file
  53       | _      ->
  54          if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir else
  55          aux (F.dirname bdir) (F.concat (F.basename bdir) file)
  56    in
  57    aux dir file
  58 (*
  59
  60    let bpath = F.dirname str ^ "/" in
  61    bpath, buri
  62 *)