added latex style comment, with start token "%%"

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index b62230a335aa84b1da78e8d3eb0687b6c00b534a..9534704edd466caeabd591cc9ed6ebf84ef8b7d2 100644 (file)
--- 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"