diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-25 12:50:11 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-25 12:50:11 +0000 |
| commit | 83e8538118c0b060cb6f231726cda9178f4146bc (patch) | |
| tree | 5b5537a8f8956a40e16cb8724c14bfb498bffaa6 /ide | |
| parent | bb950a09785c1e5a95e6368852a0d8a4b5003f5d (diff) | |
Fix r15259 to get rid of bug 2783
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15363 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index fd5186a9e..dabfd763d 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -394,7 +394,9 @@ let tag_on_insert buffer = We retag up to the next "." instead. *) let stop = grab_ending_dot insert in try split_slice_lax buffer start stop - with Coq_lex.Unterminated -> () + with Coq_lex.Unterminated -> + try split_slice_lax buffer start buffer#end_iter + with Coq_lex.Unterminated -> () with Not_found -> (* This is raised by [grab_sentence_start] *) let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in |