# HG changeset patch
# User wenzelm
# Date 1396088982 -3600
# Node ID 1147854080b4c3d304085cebd37cada32048417b
# Parent  b1cf8ddc2e040e17262d3d6164141664f7d5e49b
tuned rendering -- change mouse pointer for active areas;

diff -r b1cf8ddc2e04 -r 1147854080b4 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 29 10:49:32 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 29 11:29:42 2014 +0100
@@ -10,7 +10,7 @@
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Color, Point, Toolkit}
+import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import java.awt.font.TextAttribute
@@ -100,7 +100,9 @@
 
   /* active areas within the text */
 
-  private class Active_Area[A](rendering: Rendering => Text.Range => Option[Text.Info[A]])
+  private class Active_Area[A](
+    rendering: Rendering => Text.Range => Option[Text.Info[A]],
+    cursor: Option[Int])
   {
     private var the_text_info: Option[(String, Text.Info[A])] = None
 
@@ -115,6 +117,12 @@
         new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
 
       if (new_text_info != old_text_info) {
+        if (cursor.isDefined) {
+          if (new_text_info.isDefined)
+            text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))
+          else
+            text_area.getPainter.resetCursor
+        }
         for {
           r0 <- JEdit_Lib.visible_range(text_area)
           opt <- List(old_text_info, new_text_info)
@@ -133,10 +141,13 @@
 
   // owned by Swing thread
 
-  private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
+  private val highlight_area =
+    new Active_Area[Color]((r: Rendering) => r.highlight _, None)
   private val hyperlink_area =
-    new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _)
-  private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
+    new Active_Area[PIDE.editor.Hyperlink](
+      (r: Rendering) => r.hyperlink _, Some(Cursor.HAND_CURSOR))
+  private val active_area =
+    new Active_Area[XML.Elem]((r: Rendering) => r.active _, Some(Cursor.DEFAULT_CURSOR))
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (active_area, false))