From bb71ef3952f9dba1487a6b655752438005aa9ec9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 31 May 2005 13:40:59 +0000 Subject: [PATCH] fixed comments --- helm/ocaml/cic_disambiguation/cicTextualLexer2.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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+ -- 2.39.2