src/Tools/jEdit/src/document_view.scala
changeset 43381 806878ae2219
parent 43376 0f6880c1c759
child 43387 a59ae768249e
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 08:33:51 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 11:36:08 2011 +0200
     1.3 @@ -162,7 +162,8 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  private var highlight_range: Option[(Text.Range, Color)] = None
     1.8 +  @volatile private var _highlight_range: Option[(Text.Range, Color)] = None
     1.9 +  def highlight_range(): Option[(Text.Range, Color)] = _highlight_range
    1.10  
    1.11  
    1.12    /* CONTROL-mouse management */
    1.13 @@ -172,12 +173,12 @@
    1.14    private def exit_control()
    1.15    {
    1.16      exit_popup()
    1.17 -    highlight_range = None
    1.18 +    _highlight_range = None
    1.19    }
    1.20  
    1.21    private val focus_listener = new FocusAdapter {
    1.22      override def focusLost(e: FocusEvent) {
    1.23 -      highlight_range = None // FIXME exit_control !?
    1.24 +      _highlight_range = None // FIXME exit_control !?
    1.25      }
    1.26    }
    1.27  
    1.28 @@ -199,121 +200,20 @@
    1.29  
    1.30            if (control) init_popup(snapshot, x, y)
    1.31  
    1.32 -          highlight_range map { case (range, _) => invalidate_line_range(range) }
    1.33 -          highlight_range = if (control) subexp_range(snapshot, x, y) else None
    1.34 -          highlight_range map { case (range, _) => invalidate_line_range(range) }
    1.35 +          _highlight_range map { case (range, _) => invalidate_line_range(range) }
    1.36 +          _highlight_range = if (control) subexp_range(snapshot, x, y) else None
    1.37 +          _highlight_range map { case (range, _) => invalidate_line_range(range) }
    1.38          }
    1.39      }
    1.40    }
    1.41  
    1.42  
    1.43 -  /* TextArea painting */
    1.44 -
    1.45 -  @volatile private var _text_area_snapshot: Option[Document.Snapshot] = None
    1.46 -
    1.47 -  def text_area_snapshot(): Document.Snapshot =
    1.48 -    _text_area_snapshot match {
    1.49 -      case Some(snapshot) => snapshot
    1.50 -      case None => error("Missing text area snapshot")
    1.51 -    }
    1.52 -
    1.53 -  private val set_snapshot = new TextAreaExtension
    1.54 -  {
    1.55 -    override def paintScreenLineRange(gfx: Graphics2D,
    1.56 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.57 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.58 -    {
    1.59 -      _text_area_snapshot = Some(model.snapshot())
    1.60 -    }
    1.61 -  }
    1.62 -
    1.63 -  private val reset_snapshot = new TextAreaExtension
    1.64 -  {
    1.65 -    override def paintScreenLineRange(gfx: Graphics2D,
    1.66 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.67 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.68 -    {
    1.69 -      _text_area_snapshot = None
    1.70 -    }
    1.71 -  }
    1.72 -
    1.73 -  private val background_painter = new TextAreaExtension
    1.74 -  {
    1.75 -    override def paintScreenLineRange(gfx: Graphics2D,
    1.76 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.77 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.78 -    {
    1.79 -      Isabelle.swing_buffer_lock(model.buffer) {
    1.80 -        val snapshot = text_area_snapshot()
    1.81 -        val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.82 -
    1.83 -        for (i <- 0 until physical_lines.length) {
    1.84 -          if (physical_lines(i) != -1) {
    1.85 -            val line_range = proper_line_range(start(i), end(i))
    1.86 +  /* text area painting */
    1.87  
    1.88 -            // background color: status
    1.89 -            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
    1.90 -            for {
    1.91 -              (command, command_start) <- cmds if !command.is_ignored
    1.92 -              val range = line_range.restrict(snapshot.convert(command.range + command_start))
    1.93 -              r <- Isabelle.gfx_range(text_area, range)
    1.94 -              color <- Isabelle_Markup.status_color(snapshot, command)
    1.95 -            } {
    1.96 -              gfx.setColor(color)
    1.97 -              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    1.98 -            }
    1.99 -
   1.100 -            // background color (1): markup
   1.101 -            for {
   1.102 -              Text.Info(range, Some(color)) <-
   1.103 -                snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
   1.104 -              r <- Isabelle.gfx_range(text_area, range)
   1.105 -            } {
   1.106 -              gfx.setColor(color)
   1.107 -              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   1.108 -            }
   1.109 -
   1.110 -            // background color (2): markup
   1.111 -            for {
   1.112 -              Text.Info(range, Some(color)) <-
   1.113 -                snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
   1.114 -              r <- Isabelle.gfx_range(text_area, range)
   1.115 -            } {
   1.116 -              gfx.setColor(color)
   1.117 -              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   1.118 -            }
   1.119 +  private val text_area_painter = new Text_Area_Painter(this)
   1.120  
   1.121 -            // sub-expression highlighting -- potentially from other snapshot
   1.122 -            highlight_range match {
   1.123 -              case Some((range, color)) if line_range.overlaps(range) =>
   1.124 -                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   1.125 -                  case None =>
   1.126 -                  case Some(r) =>
   1.127 -                    gfx.setColor(color)
   1.128 -                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   1.129 -                }
   1.130 -              case _ =>
   1.131 -            }
   1.132 -
   1.133 -            // squiggly underline
   1.134 -            for {
   1.135 -              Text.Info(range, Some(color)) <-
   1.136 -                snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   1.137 -              r <- Isabelle.gfx_range(text_area, range)
   1.138 -            } {
   1.139 -              gfx.setColor(color)
   1.140 -              val x0 = (r.x / 2) * 2
   1.141 -              val y0 = r.y + ascent + 1
   1.142 -              for (x1 <- Range(x0, x0 + r.length, 2)) {
   1.143 -                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   1.144 -                gfx.drawLine(x1, y1, x1 + 1, y1)
   1.145 -              }
   1.146 -            }
   1.147 -          }
   1.148 -        }
   1.149 -      }
   1.150 -    }
   1.151 -
   1.152 +  private val tooltip_painter = new TextAreaExtension
   1.153 +  {
   1.154      override def getToolTipText(x: Int, y: Int): String =
   1.155      {
   1.156        Isabelle.swing_buffer_lock(model.buffer) {
   1.157 @@ -338,11 +238,6 @@
   1.158      }
   1.159    }
   1.160  
   1.161 -  val text_painter = new Text_Painter(this)
   1.162 -
   1.163 -
   1.164 -  /* Gutter painting */
   1.165 -
   1.166    private val gutter_painter = new TextAreaExtension
   1.167    {
   1.168      override def paintScreenLineRange(gfx: Graphics2D,
   1.169 @@ -511,12 +406,8 @@
   1.170    private def activate()
   1.171    {
   1.172      val painter = text_area.getPainter
   1.173 -
   1.174 -    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
   1.175 -    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   1.176 -    text_painter.activate()
   1.177 -    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
   1.178 -
   1.179 +    painter.addExtension(TextAreaPainter.TEXT_LAYER, tooltip_painter)
   1.180 +    text_area_painter.activate()
   1.181      text_area.getGutter.addExtension(gutter_painter)
   1.182      text_area.addFocusListener(focus_listener)
   1.183      text_area.getView.addWindowListener(window_listener)
   1.184 @@ -530,7 +421,6 @@
   1.185    private def deactivate()
   1.186    {
   1.187      val painter = text_area.getPainter
   1.188 -
   1.189      session.commands_changed -= main_actor
   1.190      session.global_settings -= main_actor
   1.191      text_area.removeFocusListener(focus_listener)
   1.192 @@ -539,11 +429,8 @@
   1.193      text_area.removeCaretListener(caret_listener)
   1.194      text_area.removeLeftOfScrollBar(overview)
   1.195      text_area.getGutter.removeExtension(gutter_painter)
   1.196 -
   1.197 -    painter.removeExtension(reset_snapshot)
   1.198 -    text_painter.deactivate()
   1.199 -    painter.removeExtension(background_painter)
   1.200 -    painter.removeExtension(set_snapshot)
   1.201 +    text_area_painter.deactivate()
   1.202 +    painter.removeExtension(tooltip_painter)
   1.203      exit_popup()
   1.204    }
   1.205  }