# HG changeset patch
# User wenzelm
# Date 1498294952 -7200
# Node ID aa002ed3f6d18d165c4f63e3b583958a2f5511e3
# Parent  8328467d32f4d3a8ee2078d4fd3df745a4b292ca
clarified indentation;

diff -r 8328467d32f4 -r aa002ed3f6d1 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Jun 23 22:25:50 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sat Jun 24 11:02:32 2017 +0200
@@ -348,12 +348,11 @@
       GUI_Thread.require {}
 
       if (!evt.isConsumed) {
-        val backspace = evt.getKeyChar == '\b'
         val special = JEdit_Lib.special_key(evt)
 
         if (PIDE.options.bool("jedit_completion")) {
           dismissed()
-          if (!backspace) {
+          if (evt.getKeyChar != '\b') {
             val immediate = PIDE.options.bool("jedit_completion_immediate")
             if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
               input_delay.revoke()
@@ -368,7 +367,7 @@
           }
         }
 
-        if (!backspace && !special) Isabelle.indent_input(text_area)
+        if (!special) Isabelle.indent_input(text_area)
       }
     }