diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-07 15:16:44 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-07 15:16:44 +0000 |
commit | c0543e34982b837c228232350febb8b30673a848 (patch) | |
tree | 6cc7bf34cf8ca84dec2a7e0c1f97f89a6737bb65 | |
parent | 8a257c7d5f10cd7939611c7bb10be5415f4cc887 (diff) |
Bug 2217: In coqide, a comment alone is now a sentence that isn't send to coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14268 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | ide/coq_lex.mll | 14 | ||||
-rw-r--r-- | ide/coqide.ml | 14 |
2 files changed, 17 insertions, 11 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 51e0610bc..4bb4b5beb 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -131,8 +131,9 @@ rule coq_string = parse and comment = parse | "(*" { ignore (comment lexbuf); comment lexbuf } | "\"" { ignore (coq_string lexbuf); comment lexbuf } - | "*)" { Lexing.lexeme_end lexbuf } - | eof { Lexing.lexeme_end lexbuf } + | "*)" space? { (* See undotted_command rule to understand the space? *) + (true, Lexing.lexeme_start lexbuf + 2) } + | eof { (false, Lexing.lexeme_end lexbuf) } | _ { comment lexbuf } and sentence stamp = parse @@ -142,10 +143,13 @@ and sentence stamp = parse } | "(*" { let comm_start = Lexing.lexeme_start lexbuf in - let comm_end = comment lexbuf in - if !start then last_leading_blank := comm_end; + let trully_terminated,comm_end = comment lexbuf in stamp comm_start comm_end Comment; - sentence stamp lexbuf + (* A comment alone is a sentence. + A comment in a sentence doesn't terminate the sentence. + *) + if not !start then sentence stamp lexbuf + else if not trully_terminated then raise Not_found } | "\"" { let str_start = Lexing.lexeme_start lexbuf in diff --git a/ide/coqide.ml b/ide/coqide.ml index aaa17d517..92d4bb79a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -947,12 +947,14 @@ object(self) in match sync get_next_phrase () with | None -> raise Unsuccessful - | Some (loc,phrase) -> - try match self#send_to_coq ct verbosely phrase true true true with - | Some safe -> sync mark_processed safe loc - | None -> sync remove_tag loc; raise Unsuccessful - with - | RestartCoqtop -> sync remove_tag loc; raise RestartCoqtop + | Some ((_,stop) as loc,phrase) -> + if stop#backward_char#has_tag Tags.Script.comment + then sync mark_processed Safe loc + else try match self#send_to_coq ct verbosely phrase true true true with + | Some safe -> sync mark_processed safe loc + | None -> sync remove_tag loc; raise Unsuccessful + with + | RestartCoqtop -> sync remove_tag loc; raise RestartCoqtop method process_next_phrase verbosely = try self#process_one_phrase !mycoqtop verbosely true true |