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