From: Enrico Tassi Date: Tue, 31 May 2005 13:40:59 +0000 (+0000) Subject: fixed comments X-Git-Tag: PRE_INDEX_1~90 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb71ef3952f9dba1487a6b655752438005aa9ec9;p=helm.git fixed comments --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 4cf0e4270..733166d7e 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -38,10 +38,13 @@ let regexp symbol_char = '\\' '(' '[' '{' ')' ']' '}' '?' ] let regexp dust = "%%" [^ '\n']* '\n' -let regexp comment_char = [^ "*)" ] + +let regexp comment_char = [^ ")" ] let regexp note = "(*" comment_char* "*)" + let regexp commentbegin = "(**" let regexp commentend = "**)" + let regexp blanks = blank+ let regexp num = digit+ let regexp tex_token = '\\' alpha+