diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-08 14:08:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-08 14:08:52 +0000 |
| commit | 12fe4b7af1170d00963277a29fd6acc1123aa6d9 (patch) | |
| tree | 035fc7e6c6b8fce2e6e95b1a3660e39c629b6eff /parsing | |
| parent | 31c44227059be9227f8fc921f74a80094f9bbcfe (diff) | |
Made warning about ending comments in string less intrusive so as to support
things like (* "forall X : (* Type *), X" *) without warnings
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13971 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/lexer.ml4 | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5e2b10a7a..c94b42c28 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -268,12 +268,19 @@ let rec number len = parser let rec string in_comments bp len = parser | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> if esc then string in_comments bp (store len '"') s else len + | [< ''('; s >] -> + (parser + | [< ''*'; s >] -> + string (Option.map succ in_comments) bp (store (store len '(') '*') s + | [< >] -> + string in_comments bp (store len '(') s) s | [< ''*'; s >] -> (parser | [< '')'; s >] -> - if in_comments then + if in_comments = Some 0 then msg_warning (str "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment."); - string in_comments bp (store (store len '*') ')') s + let in_comments = Option.map pred in_comments in + string in_comments bp (store (store len '*') ')') s | [< >] -> string in_comments bp (store len '*') s) s | [< 'c; s >] -> string in_comments bp (store len c) s @@ -362,7 +369,7 @@ let rec comment bp = parser bp2 | [< s >] -> real_push_char '*'; comment bp s >] -> () | [< ''"'; s >] -> if Flags.do_beautify() then (push_string"\"";comm_string bp2 s) - else ignore (string true bp2 0 s); + else ignore (string (Some 0) bp2 0 s); comment bp s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment | [< 'z; s >] -> real_push_char z; comment bp s @@ -471,7 +478,7 @@ let rec next_token = parser bp | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> comment_stop bp; (INT (get_buff len), (bp, ep)) - | [< ''\"'; len = string false bp 0 >] ep -> + | [< ''\"'; len = string None bp 0 >] ep -> comment_stop bp; (STRING (get_buff len), (bp, ep)) | [< ' ('(' as c); |