author | wenzelm |
Sat, 24 Jun 2017 11:14:23 +0200 | |
changeset 66186 | 9de577f2dc3b |
parent 66185 | aa002ed3f6d1 |
child 66187 | 85925d4ae93d |
--- a/src/Tools/jEdit/src/completion_popup.scala Sat Jun 24 11:02:32 2017 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Sat Jun 24 11:14:23 2017 +0200 @@ -367,7 +367,9 @@ } } - if (!special) Isabelle.indent_input(text_area) + val selection = text_area.getSelection() + if (!special && (selection == null || selection.length == 0)) + Isabelle.indent_input(text_area) } }