From: Stefano Zacchiroli 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