X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualLexer2.ml;h=9534704edd466caeabd591cc9ed6ebf84ef8b7d2;hb=8c578ae2acfb32b39610aebbd4baab3a31775a9f;hp=b62230a335aa84b1da78e8d3eb0687b6c00b534a;hpb=66a331a32509281f0c28ced014640e98a49cc0e0;p=helm.git

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"