src/Tools/jEdit/src/completion_popup.scala

--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jan 15 19:54:50 2020 +0100
@@ -368,7 +368,7 @@
         }
 
         val selection = text_area.getSelection()
-        if (!special && (selection == null || selection.length == 0))
+        if (!special && (selection == null || selection.isEmpty))
           Isabelle.indent_input(text_area)
       }
     }