# HG changeset patch
# User wenzelm
# Date 1439299489 -7200
# Node ID cc7a1285693f7aa86d2628277e420a510b63025f
# Parent  89b7c84b0480a7b55051d2b3f563f43499f1a1d9
tuned;

diff -r 89b7c84b0480 -r cc7a1285693f src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Aug 11 14:35:08 2015 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Aug 11 15:24:49 2015 +0200
@@ -146,12 +146,16 @@
   // owned by GUI thread
 
   private val highlight_area =
-    new Active_Area[Color]((r: Rendering) => r.highlight _, None)
+    new Active_Area[Color](
+      (rendering: Rendering) => rendering.highlight _, None)
+
   private val hyperlink_area =
     new Active_Area[PIDE.editor.Hyperlink](
-      (r: Rendering) => r.hyperlink _, Some(Cursor.HAND_CURSOR))
+      (rendering: Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR))
+
   private val active_area =
-    new Active_Area[XML.Elem]((r: Rendering) => r.active _, Some(Cursor.DEFAULT_CURSOR))
+    new Active_Area[XML.Elem](
+      (rendering: Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR))
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (active_area, false))