# HG changeset patch # User wenzelm # Date 1743777305 -7200 # Node ID 314d6b215f9008cd4cc3a1934cd91b880b1e1749 # Parent 64eeb82f8b02f7226324be73d68195d3345e98b2 tuned: setCaretPosition already includes selectNone; diff -r 64eeb82f8b02 -r 314d6b215f90 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Fri Apr 04 15:23:11 2025 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Fri Apr 04 16:35:05 2025 +0200 @@ -465,8 +465,7 @@ else Symbol.cartouche(arg.get) buffer.remove(antiq_range.start, antiq_range.length) - text_area.moveCaretPosition(antiq_range.start) - text_area.selectNone + text_area.setCaretPosition(antiq_range.start) text_area.setSelectedText(op_text + arg_text) } }