# HG changeset patch
# User wenzelm
# Date 1498295663 -7200
# Node ID 9de577f2dc3b0db3c8a29c4683986b79ecf314fa
# Parent  aa002ed3f6d18d165c4f63e3b583958a2f5511e3
clarified indentation;

diff -r aa002ed3f6d1 -r 9de577f2dc3b src/Tools/jEdit/src/completion_popup.scala
--- 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)
       }
     }