diff options
| author | pboutill | 2012-10-23 12:31:26 +0000 |
|---|---|---|
| committer | pboutill | 2012-10-23 12:31:26 +0000 |
| commit | 06a07009d7b83fa924ca3e30f6335fba1288c370 (patch) | |
| tree | dee0dc5c2462f266549d1df0471e5da45158c070 /ide | |
| parent | cb67b008528dc000290d5cbd93816d1ac51cadae (diff) | |
Text inserted by insert_this_phrase_on_success correct tagging
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15923 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 1655ffb8a4..75a5c5ae33 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -866,6 +866,7 @@ object(self) if stop#starts_line then input_buffer#insert ~iter:stop insertphrase else input_buffer#insert ~iter:stop ("\n"^insertphrase); + tag_on_insert (input_buffer :> GText.buffer); let start = self#get_start_of_input in input_buffer#move_mark ~where:stop (`NAME "start_of_input"); let tag = @@ -923,7 +924,7 @@ object(self) (List.exists (fun p -> self#insert_this_phrase_on_success handle - ("progress "^p^".\n") (p^".\n")) l) + ("progress "^p^".") (p^".")) l) method private include_file_dir_in_path handle = match filename with |