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 module M = MacLexer
  22
  23 let unsupported protocol =
  24    failwith (P.sprintf "probe: unsupported protocol: %s" protocol)
  25
  26 let missing path =
  27    failwith (P.sprintf "probe: missing path: %s" path)
  28
  29 let unrooted path roots =
  30    failwith (P.sprintf "probe: missing root: %s (found roots: %u)" path (L.length roots))
  31
  32 let out_int i = P.printf "%u\n" i
  33
  34 let out_length uris = out_int (US.cardinal uris)
  35
  36 let out_uris uris =
  37    let map uri = P.printf "%s\n" (U.string_of_uri uri) in
  38    US.iter map uris
  39
  40 let is_registry str =
  41    F.check_suffix str ".conf.xml"
  42
  43 let get_uri str =
  44   let str = H.normalize_path str in
  45   let dir, file =
  46       if H.is_regular str && F.check_suffix str ".ma"
  47       then F.dirname str, F.chop_extension (F.basename str)
  48       else if H.is_dir str then str, ""
  49       else missing str
  50    in
  51    let rec aux bdir file = match B.find_roots_in_dir bdir with
  52       | [root] ->
  53          let buri = L.assoc "baseuri" (B.load_root_file root) in
  54          F.concat bdir file, F.concat buri file
  55       | roots  ->
  56          if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir roots else
  57          aux (F.dirname bdir) (F.concat (F.basename bdir) file)
  58    in
  59    aux dir file
  60
  61 let mac fname =
  62    let ich = open_in fname in
  63    let lexbuf = Lexing.from_channel ich in
  64    M.token lexbuf; close_in ich
  65