# HG changeset patch
# User wenzelm
# Date 1582990230 -3600
# Node ID 633a8d52fef2b29b62261a50549d018941ad6c4e
# Parent  cbe0b6b0bed827452b9e249e3c12d313f3c2f1e7
tuned;

diff -r cbe0b6b0bed8 -r 633a8d52fef2 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Feb 28 21:23:11 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Feb 29 16:30:30 2020 +0100
@@ -362,10 +362,8 @@
 
   def select_entity(text_area: JEditTextArea)
   {
-    for {
-      doc_view <- Document_View.get(text_area)
-      rendering = doc_view.get_rendering()
-    } {
+    for (doc_view <- Document_View.get(text_area)) {
+      val rendering = doc_view.get_rendering()
       val caret_range = JEdit_Lib.caret_range(text_area)
       val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
       val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)