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