diff options
| author | herbelin | 2009-06-29 19:15:14 +0000 |
|---|---|---|
| committer | herbelin | 2009-06-29 19:15:14 +0000 |
| commit | f8e2c78e8bfd8679a77e3cf676bde58c4efffd45 (patch) | |
| tree | 6e49a2f913b740da6bb0d25228542fc669c87cb6 /parsing | |
| parent | 54723df2707b84d90ff6ca3c4285122405a39f6b (diff) | |
Miscellaneous practical commits:
- theories: made a hint database with the constructor of eq_true
- coqide: binding F5 to About dans coqide + made coqide aware of
string interpretation inside comments
- lexer: added warning when ending comments inside a strings itself in a comment
- xlate: completed patten-matching on IntroForthComing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/lexer.ml4 | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 7a1421592c..008a0f0b5d 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -248,10 +248,18 @@ let rec number len = parser let escape len c = store len c -let rec string bp len = parser +let rec string in_comments bp len = parser | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> - if esc then string bp (store len '"') s else len - | [< 'c; s >] -> string bp (store len c) s + if esc then string in_comments bp (store len '"') s else len + | [< ''*'; s >] -> + (parser + | [< '')'; s >] -> + if in_comments then + warning "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 + | [< >] -> + string in_comments bp (store len '*') s) s + | [< 'c; s >] -> string in_comments bp (store len c) s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string (* Hook for exporting comment into xml theory files *) @@ -337,7 +345,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 bp2 0 s); + else ignore (string true bp2 0 s); comment bp s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment | [< 'z; s >] -> real_push_char z; comment bp s @@ -446,7 +454,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 bp 0 >] ep -> + | [< ''\"'; len = string false bp 0 >] ep -> comment_stop bp; (("STRING", get_buff len), (bp, ep)) | [< ' ('(' as c); |