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