tuned;

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