Remove underscores from inserted texts.

Underscores are used as prefix for accelerators in gtk. In particular,
double underscores are used to escape them. So, when applying a template,
underscores should be cleaned from the inserted text.

1 files changed, 14 insertions, 4 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8d95dcee27..b91a5612c1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -881,10 +881,20 @@ let no_under = Util.String.map (fun x -> if x = '_' then '-' else x)
 let alpha_items menu_name item_name l =
   let mk_item text =
     let text' =
-      let last = String.length text - 1 in
-      if text.[last] = '.'
-      then text ^"\n"
-      else text ^" "
+      let len = String.length text in
+      let buf = Buffer.create (len + 1) in
+      let escaped = ref false in
+      String.iter (fun c ->
+          if !escaped then
+            let () = Buffer.add_char buf c in
+            escaped := false
+          else if c = '_' then escaped := true
+          else Buffer.add_char buf c
+        ) text;
+      if text.[len - 1] = '.'
+      then Buffer.add_char buf '\n'
+      else Buffer.add_char buf ' ';
+      Buffer.contents buf
     in
     let callback _ =
       on_current_term (fun sn -> sn.buffer#insert_interactive text')