| author | wenzelm |
| Wed, 06 Dec 2017 19:34:59 +0100 | |
| changeset 67148 | d24dcac5eb4c |
| parent 67147 | dea94b1aabc3 |
| child 67149 | e61557884799 |
--- 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) } }