X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryTLexer.mll;h=f677ef688e77c3edc2076bb2e9997f607766bddb;hb=f41a5585a648d57e4d8a24d664b0a5ce5d591148;hp=770f4d86d1313652244afcc3556d23e55dc15e42;hpb=daed03214fe10758d3d8b4164a27733952e28536;p=helm.git diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll index 770f4d86d..f677ef688 100644 --- a/helm/ocaml/mathql/mQueryTLexer.mll +++ b/helm/ocaml/mathql/mQueryTLexer.mll @@ -48,15 +48,17 @@ 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 }