From d676e46b02980c1b9ede019b6f880223bd2d168f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 18 Jan 2005 18:16:43 +0000 Subject: [PATCH] added latex style comment, with start token "%%" --- helm/ocaml/cic_disambiguation/cicTextualLexer2.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index b62230a33..9534704ed 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -37,6 +37,8 @@ let regexp symbol_char = ' ' '\t' '\n' '\\' '(' '[' '{' ')' ']' '}' '?' ] +let regexp comment_char = [^ '\n' ] +let regexp comment = "%%" comment_char* let regexp blanks = blank+ let regexp num = digit+ let regexp tex_token = '\\' alpha+ @@ -129,6 +131,11 @@ let rec token = lexer return lexbuf ("SYMBOL", Utf8Macro.expand macro) with Utf8Macro.Macro_not_found _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) + | comment -> + let comment = + Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 2) + in + return lexbuf ("COMMENT", comment) | eof -> return lexbuf ("EOI", "") | _ -> error lexbuf "Invalid character" -- 2.39.2