more robust, e.g. when Sidekick produces multi-selection;
authorwenzelm
Wed, 06 Dec 2017 19:34:59 +0100
changeset 67148 d24dcac5eb4c
parent 67147 dea94b1aabc3
child 67149 e61557884799
more robust, e.g. when Sidekick produces multi-selection;
src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Dec 06 18:59:33 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Dec 06 19:34:59 2017 +0100
@@ -445,6 +445,7 @@
 
       buffer.remove(antiq_range.start, antiq_range.length)
       text_area.moveCaretPosition(antiq_range.start)
+      text_area.selectNone
       text_area.setSelectedText(op_text + arg_text)
     }
   }