1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat Sep 04 00:59:03 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Sep 04 22:00:25 2010 +0200
     1.3 @@ -12,11 +12,12 @@
     1.4  
     1.5  import scala.actors.Actor._
     1.6  
     1.7 -import java.awt.event.{MouseAdapter, MouseEvent}
     1.8 +import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
     1.9  import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
    1.10  import javax.swing.{JPanel, ToolTipManager}
    1.11  import javax.swing.event.{CaretListener, CaretEvent}
    1.12  
    1.13 +import org.gjt.sp.jedit.OperatingSystem
    1.14  import org.gjt.sp.jedit.gui.RolloverButton
    1.15  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    1.16  import org.gjt.sp.jedit.syntax.SyntaxStyle
    1.17 @@ -161,6 +162,29 @@
    1.18    }
    1.19  
    1.20  
    1.21 +  /* subexpression highlighting */
    1.22 +
    1.23 +  private var highlight_point: Option[(Int, Int)] = None
    1.24 +
    1.25 +  private val focus_listener = new FocusAdapter {
    1.26 +    override def focusLost(e: FocusEvent) { highlight_point = None }
    1.27 +  }
    1.28 +
    1.29 +  private val mouse_motion_listener = new MouseMotionAdapter {
    1.30 +    override def mouseMoved(e: MouseEvent) {
    1.31 +      val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
    1.32 +      def refresh()
    1.33 +      {
    1.34 +        val offset = text_area.xyToOffset(e.getX(), e.getY())
    1.35 +        text_area.invalidateLine(model.buffer.getLineOfOffset(offset))
    1.36 +      }
    1.37 +      if (!model.buffer.isLoaded) highlight_point = None
    1.38 +      else if (!control) { highlight_point = None; refresh() }
    1.39 +      else { highlight_point = Some((e.getX(), e.getY())); refresh() }
    1.40 +    }
    1.41 +  }
    1.42 +
    1.43 +
    1.44    /* text_area_extension */
    1.45  
    1.46    private val text_area_extension = new TextAreaExtension
    1.47 @@ -173,6 +197,22 @@
    1.48          val snapshot = model.snapshot()
    1.49          val saved_color = gfx.getColor
    1.50          val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.51 +
    1.52 +        // subexpression markup
    1.53 +        val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
    1.54 +        {
    1.55 +          case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) => Some(range)
    1.56 +        }
    1.57 +        val subexp_range: Option[Text.Range] =
    1.58 +          highlight_point match {
    1.59 +            case Some((x, y)) =>
    1.60 +              val offset = text_area.xyToOffset(x, y)
    1.61 +              val markup =
    1.62 +                snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
    1.63 +              if (markup.hasNext) markup.next.info else None
    1.64 +            case None => None
    1.65 +          }
    1.66 +
    1.67          try {
    1.68            for (i <- 0 until physical_lines.length) {
    1.69              if (physical_lines(i) != -1) {
    1.70 @@ -189,6 +229,19 @@
    1.71                  gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    1.72                }
    1.73  
    1.74 +              // subexpression highlighting
    1.75 +              if (subexp_range.isDefined) {
    1.76 +                val range = snapshot.convert(subexp_range.get)
    1.77 +                if (line_range.overlaps(range)) {
    1.78 +                  Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
    1.79 +                    case None =>
    1.80 +                    case Some(r) =>
    1.81 +                      gfx.setColor(Color.black)
    1.82 +                      gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
    1.83 +                  }
    1.84 +                }
    1.85 +              }
    1.86 +
    1.87                // squiggly underline
    1.88                for {
    1.89                  Text.Info(range, color) <-
    1.90 @@ -315,6 +368,8 @@
    1.91    {
    1.92      text_area.getPainter.
    1.93        addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
    1.94 +    text_area.addFocusListener(focus_listener)
    1.95 +    text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
    1.96      text_area.addCaretListener(caret_listener)
    1.97      text_area.addLeftOfScrollBar(overview)
    1.98      session.commands_changed += commands_changed_actor
    1.99 @@ -323,8 +378,10 @@
   1.100    private def deactivate()
   1.101    {
   1.102      session.commands_changed -= commands_changed_actor
   1.103 +    text_area.removeFocusListener(focus_listener)
   1.104 +    text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
   1.105 +    text_area.removeCaretListener(caret_listener)
   1.106      text_area.removeLeftOfScrollBar(overview)
   1.107 -    text_area.removeCaretListener(caret_listener)
   1.108      text_area.getPainter.removeExtension(text_area_extension)
   1.109    }
   1.110  }
   1.111 \ No newline at end of file