]> matita.cs.unibo.it Git - helm.git/blob - components/grafite_parser/dependenciesParser.ml
686caa5b108bbf9e0c971f19c1fecebbe3b8b2b8
[helm.git] / components / grafite_parser / dependenciesParser.ml
1 (* Copyright (C) 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 (* $Id$ *)
27
28 exception UnableToInclude of string
29
30   (* statements meaningful for matitadep *)
31 type dependency =
32   | IncludeDep of string
33   | BaseuriDep of string
34   | UriDep of UriManager.uri
35   
36 let pp_dependency = function
37   | IncludeDep str -> "include \"" ^ str ^ "\""
38   | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""
39   | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
40
41 let parse_dependencies lexbuf = 
42   let tok_stream,_ =
43     CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf)
44   in
45   let rec parse acc = 
46    try
47     (parser
48     | [< '("URI", u) >] ->
49         parse (UriDep (UriManager.uri_of_string u) :: acc)
50     | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
51         parse (IncludeDep fname :: acc)
52     | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] ->
53         parse (BaseuriDep baseuri :: acc)
54     | [< '("EOI", _) >] -> acc
55     | [< 'tok >] -> parse acc
56     | [<  >] -> acc) tok_stream
57    with
58     Stream.Error _ -> parse acc
59   in
60   List.rev (parse [])
61
62 let make_absolute paths path =
63    let rec aux = function
64    | [] -> ignore (Unix.stat path); path
65    | p :: tl ->
66       let path = p ^ "/" ^ path in
67        try
68          ignore (Unix.stat path); path
69        with Unix.Unix_error _ -> aux tl
70    in
71    try
72      aux paths
73    with Unix.Unix_error _ -> raise (UnableToInclude path)
74 ;;
75        
76 let baseuri_of_script ~include_paths file = 
77  let file = make_absolute include_paths file in
78  let ic = open_in file in
79  let istream = Ulexing.from_utf8_channel ic in
80  let rec find_baseuri =
81   function
82      [] -> failwith ("No baseuri defined in " ^ file)
83    | BaseuriDep s::_ -> s
84    | _::tl -> find_baseuri tl in
85  let buri = find_baseuri (parse_dependencies istream) in
86  let uri = Http_getter_misc.strip_trailing_slash buri in
87  if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
88    HLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
89  uri