separate module for text area painting;
authorwenzelm
Tue Jun 14 11:36:08 2011 +0200 (2011-06-14 ago)
changeset 43381806878ae2219
parent 43380 809de915155f
child 43382 5d9d34bdec25
separate module for text area painting;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/text_area_painter.scala
src/Tools/jEdit/src/text_painter.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Jun 14 08:33:51 2011 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Jun 14 11:36:08 2011 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    "src/raw_output_dockable.scala"
     1.5    "src/scala_console.scala"
     1.6    "src/session_dockable.scala"
     1.7 -  "src/text_painter.scala"
     1.8 +  "src/text_area_painter.scala"
     1.9  )
    1.10  
    1.11  declare -a RESOURCES=(
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 08:33:51 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 11:36:08 2011 +0200
     2.3 @@ -162,7 +162,8 @@
     2.4      }
     2.5    }
     2.6  
     2.7 -  private var highlight_range: Option[(Text.Range, Color)] = None
     2.8 +  @volatile private var _highlight_range: Option[(Text.Range, Color)] = None
     2.9 +  def highlight_range(): Option[(Text.Range, Color)] = _highlight_range
    2.10  
    2.11  
    2.12    /* CONTROL-mouse management */
    2.13 @@ -172,12 +173,12 @@
    2.14    private def exit_control()
    2.15    {
    2.16      exit_popup()
    2.17 -    highlight_range = None
    2.18 +    _highlight_range = None
    2.19    }
    2.20  
    2.21    private val focus_listener = new FocusAdapter {
    2.22      override def focusLost(e: FocusEvent) {
    2.23 -      highlight_range = None // FIXME exit_control !?
    2.24 +      _highlight_range = None // FIXME exit_control !?
    2.25      }
    2.26    }
    2.27  
    2.28 @@ -199,121 +200,20 @@
    2.29  
    2.30            if (control) init_popup(snapshot, x, y)
    2.31  
    2.32 -          highlight_range map { case (range, _) => invalidate_line_range(range) }
    2.33 -          highlight_range = if (control) subexp_range(snapshot, x, y) else None
    2.34 -          highlight_range map { case (range, _) => invalidate_line_range(range) }
    2.35 +          _highlight_range map { case (range, _) => invalidate_line_range(range) }
    2.36 +          _highlight_range = if (control) subexp_range(snapshot, x, y) else None
    2.37 +          _highlight_range map { case (range, _) => invalidate_line_range(range) }
    2.38          }
    2.39      }
    2.40    }
    2.41  
    2.42  
    2.43 -  /* TextArea painting */
    2.44 -
    2.45 -  @volatile private var _text_area_snapshot: Option[Document.Snapshot] = None
    2.46 -
    2.47 -  def text_area_snapshot(): Document.Snapshot =
    2.48 -    _text_area_snapshot match {
    2.49 -      case Some(snapshot) => snapshot
    2.50 -      case None => error("Missing text area snapshot")
    2.51 -    }
    2.52 -
    2.53 -  private val set_snapshot = new TextAreaExtension
    2.54 -  {
    2.55 -    override def paintScreenLineRange(gfx: Graphics2D,
    2.56 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.57 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.58 -    {
    2.59 -      _text_area_snapshot = Some(model.snapshot())
    2.60 -    }
    2.61 -  }
    2.62 -
    2.63 -  private val reset_snapshot = new TextAreaExtension
    2.64 -  {
    2.65 -    override def paintScreenLineRange(gfx: Graphics2D,
    2.66 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.67 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.68 -    {
    2.69 -      _text_area_snapshot = None
    2.70 -    }
    2.71 -  }
    2.72 -
    2.73 -  private val background_painter = new TextAreaExtension
    2.74 -  {
    2.75 -    override def paintScreenLineRange(gfx: Graphics2D,
    2.76 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.77 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.78 -    {
    2.79 -      Isabelle.swing_buffer_lock(model.buffer) {
    2.80 -        val snapshot = text_area_snapshot()
    2.81 -        val ascent = text_area.getPainter.getFontMetrics.getAscent
    2.82 -
    2.83 -        for (i <- 0 until physical_lines.length) {
    2.84 -          if (physical_lines(i) != -1) {
    2.85 -            val line_range = proper_line_range(start(i), end(i))
    2.86 +  /* text area painting */
    2.87  
    2.88 -            // background color: status
    2.89 -            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
    2.90 -            for {
    2.91 -              (command, command_start) <- cmds if !command.is_ignored
    2.92 -              val range = line_range.restrict(snapshot.convert(command.range + command_start))
    2.93 -              r <- Isabelle.gfx_range(text_area, range)
    2.94 -              color <- Isabelle_Markup.status_color(snapshot, command)
    2.95 -            } {
    2.96 -              gfx.setColor(color)
    2.97 -              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    2.98 -            }
    2.99 -
   2.100 -            // background color (1): markup
   2.101 -            for {
   2.102 -              Text.Info(range, Some(color)) <-
   2.103 -                snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
   2.104 -              r <- Isabelle.gfx_range(text_area, range)
   2.105 -            } {
   2.106 -              gfx.setColor(color)
   2.107 -              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   2.108 -            }
   2.109 -
   2.110 -            // background color (2): markup
   2.111 -            for {
   2.112 -              Text.Info(range, Some(color)) <-
   2.113 -                snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
   2.114 -              r <- Isabelle.gfx_range(text_area, range)
   2.115 -            } {
   2.116 -              gfx.setColor(color)
   2.117 -              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   2.118 -            }
   2.119 +  private val text_area_painter = new Text_Area_Painter(this)
   2.120  
   2.121 -            // sub-expression highlighting -- potentially from other snapshot
   2.122 -            highlight_range match {
   2.123 -              case Some((range, color)) if line_range.overlaps(range) =>
   2.124 -                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   2.125 -                  case None =>
   2.126 -                  case Some(r) =>
   2.127 -                    gfx.setColor(color)
   2.128 -                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   2.129 -                }
   2.130 -              case _ =>
   2.131 -            }
   2.132 -
   2.133 -            // squiggly underline
   2.134 -            for {
   2.135 -              Text.Info(range, Some(color)) <-
   2.136 -                snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   2.137 -              r <- Isabelle.gfx_range(text_area, range)
   2.138 -            } {
   2.139 -              gfx.setColor(color)
   2.140 -              val x0 = (r.x / 2) * 2
   2.141 -              val y0 = r.y + ascent + 1
   2.142 -              for (x1 <- Range(x0, x0 + r.length, 2)) {
   2.143 -                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   2.144 -                gfx.drawLine(x1, y1, x1 + 1, y1)
   2.145 -              }
   2.146 -            }
   2.147 -          }
   2.148 -        }
   2.149 -      }
   2.150 -    }
   2.151 -
   2.152 +  private val tooltip_painter = new TextAreaExtension
   2.153 +  {
   2.154      override def getToolTipText(x: Int, y: Int): String =
   2.155      {
   2.156        Isabelle.swing_buffer_lock(model.buffer) {
   2.157 @@ -338,11 +238,6 @@
   2.158      }
   2.159    }
   2.160  
   2.161 -  val text_painter = new Text_Painter(this)
   2.162 -
   2.163 -
   2.164 -  /* Gutter painting */
   2.165 -
   2.166    private val gutter_painter = new TextAreaExtension
   2.167    {
   2.168      override def paintScreenLineRange(gfx: Graphics2D,
   2.169 @@ -511,12 +406,8 @@
   2.170    private def activate()
   2.171    {
   2.172      val painter = text_area.getPainter
   2.173 -
   2.174 -    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
   2.175 -    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   2.176 -    text_painter.activate()
   2.177 -    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
   2.178 -
   2.179 +    painter.addExtension(TextAreaPainter.TEXT_LAYER, tooltip_painter)
   2.180 +    text_area_painter.activate()
   2.181      text_area.getGutter.addExtension(gutter_painter)
   2.182      text_area.addFocusListener(focus_listener)
   2.183      text_area.getView.addWindowListener(window_listener)
   2.184 @@ -530,7 +421,6 @@
   2.185    private def deactivate()
   2.186    {
   2.187      val painter = text_area.getPainter
   2.188 -
   2.189      session.commands_changed -= main_actor
   2.190      session.global_settings -= main_actor
   2.191      text_area.removeFocusListener(focus_listener)
   2.192 @@ -539,11 +429,8 @@
   2.193      text_area.removeCaretListener(caret_listener)
   2.194      text_area.removeLeftOfScrollBar(overview)
   2.195      text_area.getGutter.removeExtension(gutter_painter)
   2.196 -
   2.197 -    painter.removeExtension(reset_snapshot)
   2.198 -    text_painter.deactivate()
   2.199 -    painter.removeExtension(background_painter)
   2.200 -    painter.removeExtension(set_snapshot)
   2.201 +    text_area_painter.deactivate()
   2.202 +    painter.removeExtension(tooltip_painter)
   2.203      exit_popup()
   2.204    }
   2.205  }
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 11:36:08 2011 +0200
     3.3 @@ -0,0 +1,286 @@
     3.4 +/*  Title:      Tools/jEdit/src/text_area_painter.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Painter setup for main jEdit text area.
     3.8 +*/
     3.9 +
    3.10 +package isabelle.jedit
    3.11 +
    3.12 +
    3.13 +import isabelle._
    3.14 +
    3.15 +import java.awt.{Graphics, Graphics2D}
    3.16 +import java.util.ArrayList
    3.17 +
    3.18 +import org.gjt.sp.jedit.Debug
    3.19 +import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    3.20 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    3.21 +
    3.22 +
    3.23 +class Text_Area_Painter(doc_view: Document_View)
    3.24 +{
    3.25 +  private val model = doc_view.model
    3.26 +  private val text_area = doc_view.text_area
    3.27 +
    3.28 +  private val orig_text_painter: TextAreaExtension =
    3.29 +  {
    3.30 +    val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
    3.31 +    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    3.32 +    match {
    3.33 +      case List(x) => x
    3.34 +      case _ => error("Expected exactly one " + name)
    3.35 +    }
    3.36 +  }
    3.37 +
    3.38 +
    3.39 +  /* painter snapshot */
    3.40 +
    3.41 +  @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
    3.42 +
    3.43 +  private def painter_snapshot(): Document.Snapshot =
    3.44 +    _painter_snapshot match {
    3.45 +      case Some(snapshot) => snapshot
    3.46 +      case None => error("Missing document snapshot for text area painter")
    3.47 +    }
    3.48 +
    3.49 +  private val set_snapshot = new TextAreaExtension
    3.50 +  {
    3.51 +    override def paintScreenLineRange(gfx: Graphics2D,
    3.52 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.53 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    3.54 +    {
    3.55 +      _painter_snapshot = Some(model.snapshot())
    3.56 +    }
    3.57 +  }
    3.58 +
    3.59 +  private val reset_snapshot = new TextAreaExtension
    3.60 +  {
    3.61 +    override def paintScreenLineRange(gfx: Graphics2D,
    3.62 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.63 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    3.64 +    {
    3.65 +      _painter_snapshot = None
    3.66 +    }
    3.67 +  }
    3.68 +
    3.69 +
    3.70 +  /* text background */
    3.71 +
    3.72 +  private val background_painter = new TextAreaExtension
    3.73 +  {
    3.74 +    override def paintScreenLineRange(gfx: Graphics2D,
    3.75 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.76 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    3.77 +    {
    3.78 +      Isabelle.swing_buffer_lock(model.buffer) {
    3.79 +        val snapshot = painter_snapshot()
    3.80 +        val ascent = text_area.getPainter.getFontMetrics.getAscent
    3.81 +
    3.82 +        for (i <- 0 until physical_lines.length) {
    3.83 +          if (physical_lines(i) != -1) {
    3.84 +            val line_range = doc_view.proper_line_range(start(i), end(i))
    3.85 +
    3.86 +            // background color: status
    3.87 +            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
    3.88 +            for {
    3.89 +              (command, command_start) <- cmds if !command.is_ignored
    3.90 +              val range = line_range.restrict(snapshot.convert(command.range + command_start))
    3.91 +              r <- Isabelle.gfx_range(text_area, range)
    3.92 +              color <- Isabelle_Markup.status_color(snapshot, command)
    3.93 +            } {
    3.94 +              gfx.setColor(color)
    3.95 +              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    3.96 +            }
    3.97 +
    3.98 +            // background color (1): markup
    3.99 +            for {
   3.100 +              Text.Info(range, Some(color)) <-
   3.101 +                snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
   3.102 +              r <- Isabelle.gfx_range(text_area, range)
   3.103 +            } {
   3.104 +              gfx.setColor(color)
   3.105 +              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   3.106 +            }
   3.107 +
   3.108 +            // background color (2): markup
   3.109 +            for {
   3.110 +              Text.Info(range, Some(color)) <-
   3.111 +                snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
   3.112 +              r <- Isabelle.gfx_range(text_area, range)
   3.113 +            } {
   3.114 +              gfx.setColor(color)
   3.115 +              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   3.116 +            }
   3.117 +
   3.118 +            // sub-expression highlighting -- potentially from other snapshot
   3.119 +            doc_view.highlight_range match {
   3.120 +              case Some((range, color)) if line_range.overlaps(range) =>
   3.121 +                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   3.122 +                  case None =>
   3.123 +                  case Some(r) =>
   3.124 +                    gfx.setColor(color)
   3.125 +                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   3.126 +                }
   3.127 +              case _ =>
   3.128 +            }
   3.129 +
   3.130 +            // squiggly underline
   3.131 +            for {
   3.132 +              Text.Info(range, Some(color)) <-
   3.133 +                snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   3.134 +              r <- Isabelle.gfx_range(text_area, range)
   3.135 +            } {
   3.136 +              gfx.setColor(color)
   3.137 +              val x0 = (r.x / 2) * 2
   3.138 +              val y0 = r.y + ascent + 1
   3.139 +              for (x1 <- Range(x0, x0 + r.length, 2)) {
   3.140 +                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   3.141 +                gfx.drawLine(x1, y1, x1 + 1, y1)
   3.142 +              }
   3.143 +            }
   3.144 +          }
   3.145 +        }
   3.146 +      }
   3.147 +    }
   3.148 +  }
   3.149 +
   3.150 +
   3.151 +  /* text */
   3.152 +
   3.153 +  private val text_painter = new TextAreaExtension
   3.154 +  {
   3.155 +    override def paintScreenLineRange(gfx: Graphics2D,
   3.156 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
   3.157 +      start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
   3.158 +    {
   3.159 +      val buffer = text_area.getBuffer
   3.160 +      Isabelle.swing_buffer_lock(buffer) {
   3.161 +        val painter = text_area.getPainter
   3.162 +        val font = painter.getFont
   3.163 +        val font_context = painter.getFontRenderContext
   3.164 +        val font_metrics = painter.getFontMetrics
   3.165 +
   3.166 +        def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   3.167 +        {
   3.168 +          val clip_rect = gfx.getClipBounds
   3.169 +
   3.170 +          var w = 0.0f
   3.171 +          var offset = head_offset
   3.172 +          var chunk = head
   3.173 +          while (chunk != null) {
   3.174 +            val chunk_length = if (chunk.str == null) 0 else chunk.str.length
   3.175 +
   3.176 +            if (x + w + chunk.width > clip_rect.x &&
   3.177 +                x + w < clip_rect.x + clip_rect.width &&
   3.178 +                chunk.accessable && chunk.visible)
   3.179 +            {
   3.180 +              val chunk_range = Text.Range(offset, offset + chunk_length)
   3.181 +              val chunk_font = chunk.style.getFont
   3.182 +              val chunk_color = chunk.style.getForegroundColor
   3.183 +
   3.184 +              val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
   3.185 +
   3.186 +              gfx.setFont(chunk_font)
   3.187 +              if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
   3.188 +                  markup.forall(info => info.info.isEmpty)) {
   3.189 +                gfx.setColor(chunk_color)
   3.190 +                gfx.drawGlyphVector(chunk.gv, x + w, y)
   3.191 +              }
   3.192 +              else {
   3.193 +                var xpos = x + w
   3.194 +                for (Text.Info(range, info) <- markup) {
   3.195 +                  val str = chunk.str.substring(range.start - offset, range.stop - offset)
   3.196 +                  gfx.setColor(info.getOrElse(chunk_color))
   3.197 +                  gfx.drawString(str, xpos.toInt, y.toInt)
   3.198 +                  xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
   3.199 +                }
   3.200 +              }
   3.201 +            }
   3.202 +            w += chunk.width
   3.203 +            offset += chunk_length
   3.204 +            chunk = chunk.next.asInstanceOf[Chunk]
   3.205 +          }
   3.206 +          w
   3.207 +        }
   3.208 +
   3.209 +        // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
   3.210 +        // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
   3.211 +        val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
   3.212 +        val soft_wrap = buffer.getStringProperty("wrap") == "soft"
   3.213 +        val wrap_margin =
   3.214 +        {
   3.215 +          val max = buffer.getIntegerProperty("maxLineLen", 0)
   3.216 +          if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   3.217 +          else if (soft_wrap) painter.getWidth - char_width * 3
   3.218 +          else 0
   3.219 +        }.toFloat
   3.220 +
   3.221 +        val line_infos: Map[Text.Offset, Chunk] =
   3.222 +        {
   3.223 +          val out = new ArrayList[Chunk]
   3.224 +          val handler = new DisplayTokenHandler
   3.225 +          val margin = if (soft_wrap) wrap_margin else 0.0f
   3.226 +
   3.227 +          var result = Map[Text.Offset, Chunk]()
   3.228 +          for (line <- physical_lines.iterator.filter(i => i != -1)) {
   3.229 +            out.clear
   3.230 +            handler.init(painter.getStyles, font_context, painter, out, margin)
   3.231 +            buffer.markTokens(line, handler)
   3.232 +
   3.233 +            val line_start = buffer.getLineStartOffset(line)
   3.234 +            for (i <- 0 until out.size) {
   3.235 +              val chunk = out.get(i)
   3.236 +              result += (line_start + chunk.offset -> chunk)
   3.237 +            }
   3.238 +          }
   3.239 +          result
   3.240 +        }
   3.241 +
   3.242 +        val clip = gfx.getClip
   3.243 +        val x0 = text_area.getHorizontalOffset
   3.244 +        var y0 =
   3.245 +          y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent
   3.246 +
   3.247 +        for (i <- 0 until physical_lines.length) {
   3.248 +          if (physical_lines(i) != -1) {
   3.249 +            line_infos.get(start(i)) match {
   3.250 +              case Some(chunk) =>
   3.251 +                val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
   3.252 +                gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   3.253 +                orig_text_painter.paintValidLine(gfx,
   3.254 +                  first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)
   3.255 +                gfx.setClip(clip)
   3.256 +
   3.257 +              case None =>
   3.258 +            }
   3.259 +          }
   3.260 +          y0 += line_height
   3.261 +        }
   3.262 +      }
   3.263 +    }
   3.264 +  }
   3.265 +
   3.266 +
   3.267 +  /* activation */
   3.268 +
   3.269 +  def activate()
   3.270 +  {
   3.271 +    val painter = text_area.getPainter
   3.272 +    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
   3.273 +    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   3.274 +    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   3.275 +    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
   3.276 +    painter.removeExtension(orig_text_painter)
   3.277 +  }
   3.278 +
   3.279 +  def deactivate()
   3.280 +  {
   3.281 +    val painter = text_area.getPainter
   3.282 +    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   3.283 +    painter.removeExtension(reset_snapshot)
   3.284 +    painter.removeExtension(text_painter)
   3.285 +    painter.removeExtension(background_painter)
   3.286 +    painter.removeExtension(set_snapshot)
   3.287 +  }
   3.288 +}
   3.289 +
     4.1 --- a/src/Tools/jEdit/src/text_painter.scala	Tue Jun 14 08:33:51 2011 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,162 +0,0 @@
     4.4 -/*  Title:      Tools/jEdit/src/text_painter.scala
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -Replacement painter for jEdit text area.
     4.8 -*/
     4.9 -
    4.10 -package isabelle.jedit
    4.11 -
    4.12 -
    4.13 -import isabelle._
    4.14 -
    4.15 -import java.awt.{Graphics, Graphics2D}
    4.16 -import java.util.ArrayList
    4.17 -
    4.18 -import org.gjt.sp.jedit.Debug
    4.19 -import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    4.20 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    4.21 -
    4.22 -
    4.23 -class Text_Painter(doc_view: Document_View) extends TextAreaExtension
    4.24 -{
    4.25 -  private val text_area = doc_view.text_area
    4.26 -
    4.27 -  private val orig_text_painter: TextAreaExtension =
    4.28 -  {
    4.29 -    val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
    4.30 -    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    4.31 -    match {
    4.32 -      case List(x) => x
    4.33 -      case _ => error("Expected exactly one " + name)
    4.34 -    }
    4.35 -  }
    4.36 -
    4.37 -  override def paintScreenLineRange(gfx: Graphics2D,
    4.38 -    first_line: Int, last_line: Int, physical_lines: Array[Int],
    4.39 -    start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
    4.40 -  {
    4.41 -    val buffer = text_area.getBuffer
    4.42 -    Isabelle.swing_buffer_lock(buffer) {
    4.43 -      val painter = text_area.getPainter
    4.44 -      val font = painter.getFont
    4.45 -      val font_context = painter.getFontRenderContext
    4.46 -      val font_metrics = painter.getFontMetrics
    4.47 -
    4.48 -      def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    4.49 -      {
    4.50 -        val clip_rect = gfx.getClipBounds
    4.51 -
    4.52 -        var w = 0.0f
    4.53 -        var offset = head_offset
    4.54 -        var chunk = head
    4.55 -        while (chunk != null) {
    4.56 -          val chunk_length = if (chunk.str == null) 0 else chunk.str.length
    4.57 -
    4.58 -          if (x + w + chunk.width > clip_rect.x &&
    4.59 -              x + w < clip_rect.x + clip_rect.width &&
    4.60 -              chunk.accessable && chunk.visible)
    4.61 -          {
    4.62 -            val chunk_range = Text.Range(offset, offset + chunk_length)
    4.63 -            val chunk_font = chunk.style.getFont
    4.64 -            val chunk_color = chunk.style.getForegroundColor
    4.65 -
    4.66 -            val markup =
    4.67 -              doc_view.text_area_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
    4.68 -
    4.69 -            gfx.setFont(chunk_font)
    4.70 -            if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    4.71 -                markup.forall(info => info.info.isEmpty)) {
    4.72 -              gfx.setColor(chunk_color)
    4.73 -              gfx.drawGlyphVector(chunk.gv, x + w, y)
    4.74 -            }
    4.75 -            else {
    4.76 -              var xpos = x + w
    4.77 -              for (Text.Info(range, info) <- markup) {
    4.78 -                val str = chunk.str.substring(range.start - offset, range.stop - offset)
    4.79 -                gfx.setColor(info.getOrElse(chunk_color))
    4.80 -                gfx.drawString(str, xpos.toInt, y.toInt)
    4.81 -                xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    4.82 -              }
    4.83 -            }
    4.84 -          }
    4.85 -          w += chunk.width
    4.86 -          offset += chunk_length
    4.87 -          chunk = chunk.next.asInstanceOf[Chunk]
    4.88 -        }
    4.89 -        w
    4.90 -      }
    4.91 -
    4.92 -      // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
    4.93 -      // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
    4.94 -      val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
    4.95 -      val soft_wrap = buffer.getStringProperty("wrap") == "soft"
    4.96 -      val wrap_margin =
    4.97 -      {
    4.98 -        val max = buffer.getIntegerProperty("maxLineLen", 0)
    4.99 -        if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   4.100 -        else if (soft_wrap) painter.getWidth - char_width * 3
   4.101 -        else 0
   4.102 -      }.toFloat
   4.103 -
   4.104 -      val line_infos: Map[Text.Offset, Chunk] =
   4.105 -      {
   4.106 -        val out = new ArrayList[Chunk]
   4.107 -        val handler = new DisplayTokenHandler
   4.108 -        val margin = if (soft_wrap) wrap_margin else 0.0f
   4.109 -
   4.110 -        var result = Map[Text.Offset, Chunk]()
   4.111 -        for (line <- physical_lines.iterator.filter(i => i != -1)) {
   4.112 -          out.clear
   4.113 -          handler.init(painter.getStyles, font_context, painter, out, margin)
   4.114 -          buffer.markTokens(line, handler)
   4.115 -
   4.116 -          val line_start = buffer.getLineStartOffset(line)
   4.117 -          for (i <- 0 until out.size) {
   4.118 -            val chunk = out.get(i)
   4.119 -            result += (line_start + chunk.offset -> chunk)
   4.120 -          }
   4.121 -        }
   4.122 -        result
   4.123 -      }
   4.124 -
   4.125 -      val clip = gfx.getClip
   4.126 -      val x0 = text_area.getHorizontalOffset
   4.127 -      var y0 =
   4.128 -        y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent
   4.129 -
   4.130 -      for (i <- 0 until physical_lines.length) {
   4.131 -        if (physical_lines(i) != -1) {
   4.132 -          line_infos.get(start(i)) match {
   4.133 -            case Some(chunk) =>
   4.134 -              val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
   4.135 -              gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   4.136 -              orig_text_painter.paintValidLine(gfx,
   4.137 -                first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)
   4.138 -              gfx.setClip(clip)
   4.139 -
   4.140 -            case None =>
   4.141 -          }
   4.142 -        }
   4.143 -        y0 += line_height
   4.144 -      }
   4.145 -    }
   4.146 -  }
   4.147 -
   4.148 -
   4.149 -  /* activation */
   4.150 -
   4.151 -  def activate()
   4.152 -  {
   4.153 -    val painter = text_area.getPainter
   4.154 -    painter.removeExtension(orig_text_painter)
   4.155 -    painter.addExtension(TextAreaPainter.TEXT_LAYER, this)
   4.156 -  }
   4.157 -
   4.158 -  def deactivate()
   4.159 -  {
   4.160 -    val painter = text_area.getPainter
   4.161 -    painter.removeExtension(this)
   4.162 -    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   4.163 -  }
   4.164 -}
   4.165 -