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

2 files changed, 15 insertions, 14 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
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index bd426b6fd3..93ef6596c1 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -124,25 +124,25 @@ let hyp_next_tac sigma env (id,_,ast) =
   let id_s = Names.string_of_id id in
   let type_s = string_of_ppcmds (pr_ltype_env env ast) in
   [
-    ("clear "^id_s),("clear "^id_s^".\n");
-    ("apply "^id_s),("apply "^id_s^".\n");
-    ("exact "^id_s),("exact "^id_s^".\n");
-    ("generalize "^id_s),("generalize "^id_s^".\n");
-    ("absurd <"^id_s^">"),("absurd "^type_s^".\n")
+    ("clear "^id_s),("clear "^id_s^".");
+    ("apply "^id_s),("apply "^id_s^".");
+    ("exact "^id_s),("exact "^id_s^".");
+    ("generalize "^id_s),("generalize "^id_s^".");
+    ("absurd <"^id_s^">"),("absurd "^type_s^".")
   ] @ [
-    ("discriminate "^id_s),("discriminate "^id_s^".\n");
-    ("injection "^id_s),("injection "^id_s^".\n")
+    ("discriminate "^id_s),("discriminate "^id_s^".");
+    ("injection "^id_s),("injection "^id_s^".")
   ] @ [
-    ("rewrite "^id_s),("rewrite "^id_s^".\n");
-    ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n")
+    ("rewrite "^id_s),("rewrite "^id_s^".");
+    ("rewrite <- "^id_s),("rewrite <- "^id_s^".")
   ] @ [
-    ("elim "^id_s), ("elim "^id_s^".\n");
-    ("inversion "^id_s), ("inversion "^id_s^".\n");
-    ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n")
+    ("elim "^id_s), ("elim "^id_s^".");
+    ("inversion "^id_s), ("inversion "^id_s^".");
+    ("inversion clear "^id_s), ("inversion_clear "^id_s^".")
   ]
 
 let concl_next_tac sigma concl =
-  let expand s = (s,s^".\n") in
+  let expand s = (s,s^".") in
   List.map expand ([
     "intro";
     "intros";