From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 18 Jan 2005 18:16:43 +0000 (+0000)
Subject: added latex style comment, with start token "%%"
X-Git-Tag: V_0_1_0~130
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d676e46b02980c1b9ede019b6f880223bd2d168f;p=helm.git

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

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"