helm/ocaml/grafite2/grafiteMisc.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 let is_empty buri =
  27  List.for_all
  28   (function
  29       Http_getter_types.Ls_section _ -> true
  30     | Http_getter_types.Ls_object _ -> false)
  31   (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
  32
  33 let baseuri_of_baseuri_decl st =
  34   match st with
  35   | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) ->
  36       Some buri
  37   | _ -> None
  38
  39 let baseuri_of_file file =
  40   let uri = ref None in
  41   let ic = open_in file in
  42   let istream = Ulexing.from_utf8_channel ic in
  43   (try
  44     while true do
  45       try
  46         let stm = GrafiteParser.parse_statement istream in
  47         match baseuri_of_baseuri_decl stm with
  48         | Some buri ->
  49             let u = Http_getter_misc.strip_trailing_slash buri in
  50             if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
  51               HLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
  52             (try
  53               ignore(Http_getter.resolve u)
  54             with
  55             | Http_getter_types.Unresolvable_URI _ ->
  56                 HLog.error (file ^ " sets an unresolvable baseuri: "^buri)
  57             | Http_getter_types.Key_not_found _ -> ());
  58             uri := Some u;
  59             raise End_of_file
  60         | None -> ()
  61       with
  62         CicNotationParser.Parse_error err ->
  63           HLog.error ("Unable to parse: " ^ file);
  64           HLog.error ("Parse error: " ^ err);
  65           ()
  66     done
  67   with End_of_file -> close_in ic);
  68   match !uri with
  69   | Some uri -> uri
  70   | None -> failwith ("No baseuri defined in " ^ file)
  71
  72 let obj_file_of_script ~basedir f =
  73   let baseuri = baseuri_of_file f in
  74    LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri