]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/pxp/pxp/lexers/pxp_lex_aux_utf8.ml
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / DEVEL / pxp / pxp / lexers / pxp_lex_aux_utf8.ml
1 (* $Id$
2  * ----------------------------------------------------------------------
3  *
4  *)
5
6 (* NOTE: Currently, this module is *identical* to Pxp_lex_aux_iso88591 *)
7
8   open Pxp_types
9   open Pxp_lexer_types
10
11   let get_name_end s k =
12     (* Get the index of the end+1 of the name beginning at position k *)
13     let l = String.length s in
14     let rec find j =
15       if j < l then
16         match s.[j] with
17           | ('\009'|'\010'|'\013'|'\032') -> j
18           |_                              -> find (j+1)
19       else
20         l
21     in
22     find k
23
24   let get_ws_end s k =
25     let l =  String.length s in
26     let rec find j =
27       if j < l then
28         match s.[j] with
29             (' '|'\t'|'\r'|'\n') -> find (j+1)
30           | _                    -> j
31       else
32         l
33     in
34     find k
35
36   let scan_pi pi xml_scanner =
37     let s = String.sub pi 2 (String.length pi - 4) in
38             (* the PI without the leading "<?" and the trailing "?>" *)
39     let xml_lexbuf = Lexing.from_string (s ^ " ") in
40       (* Add space because the lexer expects whitespace after every
41        * clause; by adding a space there is always whitespace at the 
42        * end of the string.
43        *)
44
45     (* The first word of a PI must be a name: Extract it. *)
46
47     let s_name, s_len =
48       match xml_scanner xml_lexbuf with
49           Pro_name n -> 
50             let ltok = String.length (Lexing.lexeme xml_lexbuf) in
51             if String.length n = ltok then
52               (* No whitespace after the name *)
53               raise (WF_error ("Bad processing instruction"));
54             n, ltok
55         | _ -> raise (WF_error ("Bad processing instruction"))
56     in
57
58     (* Note: s_len is the length of s_name + the whitespace following s_name *)
59
60     match s_name with
61         "xml" -> begin
62           (* It is a <?xml ...?> PI: Get the other tokens *)
63           let rec collect () =
64             let t = xml_scanner xml_lexbuf in
65             (* prerr_endline (string_of_int (Lexing.lexeme_end xml_lexbuf)); *)
66             if t = Pro_eof then
67               []
68             else
69               t :: collect()
70           in
71           PI_xml (collect())
72         end
73       | _ -> 
74           let len_param = String.length s - s_len in
75           (* It is possible that len_param = -1 *)
76           if len_param >= 1 then
77             PI(s_name, String.sub s s_len len_param)
78           else
79             PI(s_name, "")
80
81 (* ======================================================================
82  * History:
83  * 
84  * $Log$
85  * Revision 1.1  2000/11/17 09:57:32  lpadovan
86  * Initial revision
87  *
88  * Revision 1.2  2000/05/29 23:53:12  gerd
89  *      Updated because Markup_* modules have been renamed to Pxp_*.
90  *
91  * Revision 1.1  2000/05/20 20:33:25  gerd
92  *      Initial revision.
93  *
94  * 
95  *)