1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat Sep 04 22:00:25 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Sep 04 22:36:42 2010 +0200
     1.3 @@ -124,6 +124,13 @@
     1.4      proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
     1.5    }
     1.6  
     1.7 +  def invalidate_line_range(range: Text.Range)
     1.8 +  {
     1.9 +    text_area.invalidateLineRange(
    1.10 +      model.buffer.getLineOfOffset(range.start),
    1.11 +      model.buffer.getLineOfOffset(range.stop))
    1.12 +  }
    1.13 +
    1.14  
    1.15    /* commands_changed_actor */
    1.16  
    1.17 @@ -164,23 +171,35 @@
    1.18  
    1.19    /* subexpression highlighting */
    1.20  
    1.21 -  private var highlight_point: Option[(Int, Int)] = None
    1.22 +  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
    1.23 +  {
    1.24 +    val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
    1.25 +    {
    1.26 +      case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) =>
    1.27 +        Some(snapshot.convert(range))
    1.28 +    }
    1.29 +    val offset = text_area.xyToOffset(x, y)
    1.30 +    val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
    1.31 +    if (markup.hasNext) markup.next.info else None
    1.32 +  }
    1.33 +
    1.34 +  private var highlight_range: Option[Text.Range] = None
    1.35  
    1.36    private val focus_listener = new FocusAdapter {
    1.37 -    override def focusLost(e: FocusEvent) { highlight_point = None }
    1.38 +    override def focusLost(e: FocusEvent) { highlight_range = None }
    1.39    }
    1.40  
    1.41    private val mouse_motion_listener = new MouseMotionAdapter {
    1.42      override def mouseMoved(e: MouseEvent) {
    1.43        val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
    1.44 -      def refresh()
    1.45 -      {
    1.46 -        val offset = text_area.xyToOffset(e.getX(), e.getY())
    1.47 -        text_area.invalidateLine(model.buffer.getLineOfOffset(offset))
    1.48 -      }
    1.49 -      if (!model.buffer.isLoaded) highlight_point = None
    1.50 -      else if (!control) { highlight_point = None; refresh() }
    1.51 -      else { highlight_point = Some((e.getX(), e.getY())); refresh() }
    1.52 +      if (!model.buffer.isLoaded) highlight_range = None
    1.53 +      else
    1.54 +        Isabelle.swing_buffer_lock(model.buffer) {
    1.55 +          highlight_range.map(invalidate_line_range(_))
    1.56 +          highlight_range =
    1.57 +            if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
    1.58 +          highlight_range.map(invalidate_line_range(_))
    1.59 +        }
    1.60      }
    1.61    }
    1.62  
    1.63 @@ -198,21 +217,6 @@
    1.64          val saved_color = gfx.getColor
    1.65          val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.66  
    1.67 -        // subexpression markup
    1.68 -        val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
    1.69 -        {
    1.70 -          case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) => Some(range)
    1.71 -        }
    1.72 -        val subexp_range: Option[Text.Range] =
    1.73 -          highlight_point match {
    1.74 -            case Some((x, y)) =>
    1.75 -              val offset = text_area.xyToOffset(x, y)
    1.76 -              val markup =
    1.77 -                snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
    1.78 -              if (markup.hasNext) markup.next.info else None
    1.79 -            case None => None
    1.80 -          }
    1.81 -
    1.82          try {
    1.83            for (i <- 0 until physical_lines.length) {
    1.84              if (physical_lines(i) != -1) {
    1.85 @@ -229,11 +233,10 @@
    1.86                  gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    1.87                }
    1.88  
    1.89 -              // subexpression highlighting
    1.90 -              if (subexp_range.isDefined) {
    1.91 -                val range = snapshot.convert(subexp_range.get)
    1.92 -                if (line_range.overlaps(range)) {
    1.93 -                  Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
    1.94 +              // subexpression highlighting -- potentially from other snapshot
    1.95 +              if (highlight_range.isDefined) {
    1.96 +                if (line_range.overlaps(highlight_range.get)) {
    1.97 +                  Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
    1.98                      case None =>
    1.99                      case Some(r) =>
   1.100                        gfx.setColor(Color.black)