X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fmathql%2FmQueryTLexer.mll;h=f677ef688e77c3edc2076bb2e9997f607766bddb;hb=f41a5585a648d57e4d8a24d664b0a5ce5d591148;hp=9cc22c2dcbc0d8076ea29124910bc8c248624967;hpb=115b3d9f3d295fd00fd0cd76f1e7d32f76dda8e8;p=helm.git diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll index 9cc22c2dc..f677ef688 100644 --- a/helm/ocaml/mathql/mQueryTLexer.mll +++ b/helm/ocaml/mathql/mQueryTLexer.mll @@ -42,21 +42,23 @@ } let SPC = [' ' '\t' '\n']+ -let ALPHA = ['A'-'Z' 'a'-'z'] +let ALPHA = ['A'-'Z' 'a'-'z' '_'] let NUM = ['0'-'9'] let IDEN = ALPHA (NUM | ALPHA)* let QSTR = [^ '"' '\\']+ rule comm_token = parse - | "*)" { query_token lexbuf } - | [^ '*']* { comm_token lexbuf } + | "(*" { comm_token lexbuf; comm_token lexbuf } + | "*)" { () } + | ['*' '('] { comm_token lexbuf } + | [^ '*' '(']* { comm_token lexbuf } and string_token = parse | '"' { DQ } | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) } | QSTR { STR (Lexing.lexeme lexbuf) } | eof { EOF } and query_token = parse - | "(*" { comm_token lexbuf } + | "(*" { comm_token lexbuf; query_token lexbuf } | SPC { query_token lexbuf } | '"' { let str = qstr string_token lexbuf in out ("STR " ^ str); STR str }