From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 15 Oct 2002 16:03:09 +0000 (+0000)
Subject: textual parser: caml-like comments added (not nestable)
X-Git-Tag: new_mathql_before_first_merge~3
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eddba0cc1b08d5d787793095c5fb0d39ee5ec2f7;p=helm.git

textual parser: caml-like comments added (not nestable)
utilities     : pretty-printing patched
---

diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll
index 89d62375a..a0884e79d 100644
--- a/helm/ocaml/mathql/mQueryTLexer.mll
+++ b/helm/ocaml/mathql/mQueryTLexer.mll
@@ -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 }
diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml
index c5e111fae..ea1829719 100644
--- a/helm/ocaml/mathql/mQueryUtil.ml
+++ b/helm/ocaml/mathql/mQueryUtil.ml
@@ -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 ^ ")"