# HG changeset patch # User wenzelm # Date 1512585299 -3600 # Node ID d24dcac5eb4c0a3ddefb842ac410c106c209b8f2 # Parent dea94b1aabc3c1480acc3328cff6660c20820b84 more robust, e.g. when Sidekick produces multi-selection; diff -r dea94b1aabc3 -r d24dcac5eb4c 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) } }