--- 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)