# 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