]> matita.cs.unibo.it Git - helm.git/commitdiff
textual parser: caml-like comments added (not nestable)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 15 Oct 2002 16:03:09 +0000 (16:03 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 15 Oct 2002 16:03:09 +0000 (16:03 +0000)
utilities     : pretty-printing patched

helm/ocaml/mathql/mQueryTLexer.mll
helm/ocaml/mathql/mQueryUtil.ml

index 89d62375a24c1730c0a43e2eaa5ee2ff49b9dc18..a0884e79dd21a7a6ec2f23da7380875a6639d4d6 100644 (file)
@@ -43,12 +43,16 @@ let NUM   = ['0'-'9']
 let IDEN  = ALPHA (NUM | ALPHA)*
 let QSTR  = [^ '"' '\\']+
 
-rule string_token = parse
+rule comm_token = parse
+   | "*)"        { query_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 }
    | SPC         { query_token lexbuf }
    | '"'         { STR (qstr string_token lexbuf) }
    | '('         { LP }
index c5e111fae62ab3db227746cb10f7366e9a4067b9..ea1829719f37bfd86641ecf4cadecb4f8deba55c 100644 (file)
@@ -67,7 +67,8 @@ let text_of_query x =
    and txt_boole = function
       | M.False       -> "false"
       | M.True        -> "true"
-      | M.Ex b x      -> "ex [" ^ txt_list txt_rvar "," b ^ "] " ^ txt_boole x
+      | M.Ex b x      -> "ex " ^ txt_boole x
+(*    | M.Ex b x      -> "ex [" ^ txt_list txt_rvar "," b ^ "] " ^ txt_boole x *)
       | M.Not x       -> "not " ^ txt_boole x
       | M.And (x, y)  -> "(" ^ txt_boole x ^ " and " ^ txt_boole y ^ ")"
       | M.Or (x, y)   -> "(" ^ txt_boole x ^ " or " ^ txt_boole y ^ ")"