# HG changeset patch
# User wenzelm
# Date 1283630425 -7200
# Node ID 947c62440026b1b5778420a9127959e940ca0446
# Parent  12dac4b58df8f1b979c6c155c1514211282c711a
basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);

diff -r 12dac4b58df8 -r 947c62440026 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat Sep 04 00:59:03 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Sep 04 22:00:25 2010 +0200
@@ -12,11 +12,12 @@
 
 import scala.actors.Actor._
 
-import java.awt.event.{MouseAdapter, MouseEvent}
+import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
 import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
 import javax.swing.{JPanel, ToolTipManager}
 import javax.swing.event.{CaretListener, CaretEvent}
 
+import org.gjt.sp.jedit.OperatingSystem
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
 import org.gjt.sp.jedit.syntax.SyntaxStyle
@@ -161,6 +162,29 @@
   }
 
 
+  /* subexpression highlighting */
+
+  private var highlight_point: Option[(Int, Int)] = None
+
+  private val focus_listener = new FocusAdapter {
+    override def focusLost(e: FocusEvent) { highlight_point = None }
+  }
+
+  private val mouse_motion_listener = new MouseMotionAdapter {
+    override def mouseMoved(e: MouseEvent) {
+      val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+      def refresh()
+      {
+        val offset = text_area.xyToOffset(e.getX(), e.getY())
+        text_area.invalidateLine(model.buffer.getLineOfOffset(offset))
+      }
+      if (!model.buffer.isLoaded) highlight_point = None
+      else if (!control) { highlight_point = None; refresh() }
+      else { highlight_point = Some((e.getX(), e.getY())); refresh() }
+    }
+  }
+
+
   /* text_area_extension */
 
   private val text_area_extension = new TextAreaExtension
@@ -173,6 +197,22 @@
         val snapshot = model.snapshot()
         val saved_color = gfx.getColor
         val ascent = text_area.getPainter.getFontMetrics.getAscent
+
+        // subexpression markup
+        val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
+        {
+          case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) => Some(range)
+        }
+        val subexp_range: Option[Text.Range] =
+          highlight_point match {
+            case Some((x, y)) =>
+              val offset = text_area.xyToOffset(x, y)
+              val markup =
+                snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
+              if (markup.hasNext) markup.next.info else None
+            case None => None
+          }
+
         try {
           for (i <- 0 until physical_lines.length) {
             if (physical_lines(i) != -1) {
@@ -189,6 +229,19 @@
                 gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
               }
 
+              // subexpression highlighting
+              if (subexp_range.isDefined) {
+                val range = snapshot.convert(subexp_range.get)
+                if (line_range.overlaps(range)) {
+                  Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
+                    case None =>
+                    case Some(r) =>
+                      gfx.setColor(Color.black)
+                      gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
+                  }
+                }
+              }
+
               // squiggly underline
               for {
                 Text.Info(range, color) <-
@@ -315,6 +368,8 @@
   {
     text_area.getPainter.
       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
+    text_area.addFocusListener(focus_listener)
+    text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
     text_area.addCaretListener(caret_listener)
     text_area.addLeftOfScrollBar(overview)
     session.commands_changed += commands_changed_actor
@@ -323,8 +378,10 @@
   private def deactivate()
   {
     session.commands_changed -= commands_changed_actor
+    text_area.removeFocusListener(focus_listener)
+    text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
+    text_area.removeCaretListener(caret_listener)
     text_area.removeLeftOfScrollBar(overview)
-    text_area.removeCaretListener(caret_listener)
     text_area.getPainter.removeExtension(text_area_extension)
   }
 }
\ No newline at end of file