From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 4 Nov 2005 13:02:54 +0000 (+0000)
Subject: better distinction of (* *) and (** *) comments
X-Git-Tag: V_0_7_2_3~134
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95e23a75677e51444fdef6aaff7a01511756119c;p=helm.git

better distinction of (* *) and (** *) comments
- first kind of comments is thrown away by the lexer, still admitting comment nesting
- second kind of comment is lexed as usual returning "BEGINCOMMENT" .... "ENDCOMMENT" token stream
---

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 13a8b3883..9fa6270ee 100644
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -64,9 +64,10 @@ let regexp meta_anonymous = "$_"
 let regexp qstring = '"' [^ '"']* '"'
 
 let regexp begincomment = "(**" xml_blank
+let regexp beginnote = "(*"
 let regexp endcomment = "*)"
-let regexp comment_char = [^'*'] | '*'[^')']
-let regexp note = "(*" ([^'*'] | "**") comment_char* "*)"
+(* let regexp comment_char = [^'*'] | '*'[^')']
+let regexp note = "|+" ([^'*'] | "**") comment_char* "+|" *)
 
 let level1_layouts = 
   [ "sub"; "sup";
@@ -230,6 +231,20 @@ let rec level2_meta_token =
         remove_left_quote (Ulexing.utf8_lexeme lexbuf))
   | eof -> return_eoi lexbuf
 
+let rec comment_token acc depth =
+  lexer
+  | beginnote ->
+      let acc = acc ^ Ulexing.utf8_lexeme lexbuf in
+      comment_token acc (depth + 1) lexbuf
+  | endcomment ->
+      let acc = acc ^ Ulexing.utf8_lexeme lexbuf in
+      if depth = 0
+      then acc
+      else comment_token acc (depth - 1) lexbuf
+  | _ ->
+      let acc = acc ^ Ulexing.utf8_lexeme lexbuf in
+      comment_token acc depth lexbuf
+
   (** @param k continuation to be invoked when no ligature has been found *)
 let rec ligatures_token k =
   lexer
@@ -274,11 +289,13 @@ and level2_ast_token =
       return lexbuf ("UNPARSED_META",
         remove_left_quote (Ulexing.utf8_lexeme lexbuf))
   | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous")
-  | note -> 
-      let comment =
+  | beginnote -> 
+      let comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in
+(*       let comment =
         Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4)
       in
-      return lexbuf ("NOTE", comment)
+      return lexbuf ("NOTE", comment) *)
+      ligatures_token level2_ast_token lexbuf
   | begincomment -> return lexbuf ("BEGINCOMMENT","")
   | endcomment -> return lexbuf ("ENDCOMMENT","")
   | eof -> return_eoi lexbuf