X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fpxp%2Fpxp%2Ftools%2Fucs2_to_utf8%2Flexer.mll;fp=helm%2FDEVEL%2Fpxp%2Fpxp%2Ftools%2Fucs2_to_utf8%2Flexer.mll;h=dfbeb5ad12533401f273bc55f60c602949ae454f;hb=c03d2c1fdab8d228cb88aaba5ca0f556318bebc5;hp=0000000000000000000000000000000000000000;hpb=758057e85325f94cd88583feb1fdf6b038e35055;p=helm.git

diff --git a/helm/DEVEL/pxp/pxp/tools/ucs2_to_utf8/lexer.mll b/helm/DEVEL/pxp/pxp/tools/ucs2_to_utf8/lexer.mll
new file mode 100644
index 000000000..dfbeb5ad1
--- /dev/null
+++ b/helm/DEVEL/pxp/pxp/tools/ucs2_to_utf8/lexer.mll
@@ -0,0 +1,43 @@
+{
+(******************************************************)
+(*    Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>   *)
+(*                   14/05/2000                       *)
+(******************************************************)
+
+open Parser
+
+let comment_depth = ref 0;;
+
+let charint_of_lexeme l =
+ String.set l 0 '0' ;
+ int_of_string l
+;;
+}
+
+let digit = ['0'-'9']|['A'-'F']
+
+rule token =
+ parse
+    [' ' '\t' '\n']                           { token lexbuf }
+  | "let"                                     { LET }
+  | (['a'-'z']|'_')(['a'-'z']|['A'-'Z']|'_'|['0'-'9']|'\'')*
+                                              { IDENT (Lexing.lexeme lexbuf) }
+  | '='                                       { EQ }
+  | ";;"                                      { END_OF_LET }
+  | "|"                                       { PIPE }
+  | '['                                       { LBRACKET }
+  | ']'                                       { RBRACKET }
+  | '-'                                       { RANGE }
+  | "(*"                                      { incr comment_depth ;
+                                                comment lexbuf
+                                              }
+  | "#x" digit digit digit digit              { CHAR (charint_of_lexeme (Lexing.lexeme lexbuf)) }
+  | eof                                       { EOF }
+
+and comment =
+ parse
+    "(*" { incr comment_depth ; comment lexbuf }
+  | "*)" { decr comment_depth ;
+           if !comment_depth = 0 then token lexbuf else comment lexbuf
+         }
+  | _    { comment lexbuf }