1.1 --- a/src/Pure/PIDE/document.scala	Fri Jul 02 21:48:54 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Jul 03 20:20:13 2010 +0200
     1.3 @@ -14,13 +14,13 @@
     1.4  {
     1.5    /* command start positions */
     1.6  
     1.7 -  def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
     1.8 +  def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
     1.9    {
    1.10 -    var offset = 0
    1.11 -    for (cmd <- commands.iterator) yield {
    1.12 -      val start = offset
    1.13 -      offset += cmd.length
    1.14 -      (cmd, start)
    1.15 +    var i = offset
    1.16 +    for (command <- commands) yield {
    1.17 +      val start = i
    1.18 +      i += command.length
    1.19 +      (command, start)
    1.20      }
    1.21    }
    1.22  
    1.23 @@ -60,9 +60,10 @@
    1.24      {
    1.25        eds match {
    1.26          case e :: es =>
    1.27 -          command_starts(commands).find {   // FIXME relative search!
    1.28 +          command_starts(commands.iterator).find {
    1.29              case (cmd, cmd_start) =>
    1.30 -              e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
    1.31 +              e.can_edit(cmd.source, cmd_start) ||
    1.32 +                e.is_insert && e.start == cmd_start + cmd.length
    1.33            } match {
    1.34              case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
    1.35                val (rest, text) = e.edit(cmd.source, cmd_start)
    1.36 @@ -144,7 +145,7 @@
    1.37  {
    1.38    /* command ranges */
    1.39  
    1.40 -  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
    1.41 +  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands.iterator)
    1.42  
    1.43    def command_start(cmd: Command): Option[Int] =
    1.44      command_starts.find(_._1 == cmd).map(_._2)

     2.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jul 02 21:48:54 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Jul 03 20:20:13 2010 +0200
     2.3 @@ -95,14 +95,6 @@
     2.4    def to_current(doc: Document, offset: Int): Int =
     2.5      (offset /: changes_from(doc)) ((i, change) => change after i)
     2.6  
     2.7 -  def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
     2.8 -  {
     2.9 -    val start = doc.command_start(cmd).get  // FIXME total?
    2.10 -    val stop = start + cmd.length
    2.11 -    (buffer.getLineOfOffset(to_current(doc, start)),
    2.12 -     buffer.getLineOfOffset(to_current(doc, stop)))
    2.13 -  }
    2.14 -
    2.15  
    2.16    /* text edits */
    2.17  

     3.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Jul 02 21:48:54 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Jul 03 20:20:13 2010 +0200
     3.3 @@ -104,13 +104,10 @@
     3.4        react {
     3.5          case Command_Set(changed) =>
     3.6            Swing_Thread.now {
     3.7 +            // FIXME cover doc states as well!!?
     3.8              val document = model.recent_document()
     3.9 -            // FIXME cover doc states as well!!?
    3.10 -            for (command <- changed if document.commands.contains(command)) {
    3.11 -              update_syntax(document, command)
    3.12 -              invalidate_line(document, command)
    3.13 -              overview.repaint()
    3.14 -            }
    3.15 +            if (changed.exists(document.commands.contains))
    3.16 +              full_repaint(document, changed)
    3.17            }
    3.18  
    3.19          case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
    3.20 @@ -118,34 +115,82 @@
    3.21      }
    3.22    }
    3.23  
    3.24 +  def full_repaint(document: Document, changed: Set[Command])
    3.25 +  {
    3.26 +    Swing_Thread.assert()
    3.27 +
    3.28 +    val buffer = model.buffer
    3.29 +    var visible_change = false
    3.30 +
    3.31 +    for ((command, start) <- document.command_starts) {
    3.32 +      if (changed(command)) {
    3.33 +        val stop = start + command.length
    3.34 +        val line1 = buffer.getLineOfOffset(model.to_current(document, start))
    3.35 +        val line2 = buffer.getLineOfOffset(model.to_current(document, stop))
    3.36 +        if (line2 >= text_area.getFirstLine &&
    3.37 +            line1 <= text_area.getFirstLine + text_area.getVisibleLines)
    3.38 +          visible_change = true
    3.39 +        text_area.invalidateLineRange(line1, line2)
    3.40 +      }
    3.41 +    }
    3.42 +    if (visible_change) model.buffer.propertiesChanged()
    3.43 +
    3.44 +    overview.repaint()  // FIXME paint here!?
    3.45 +  }
    3.46 +
    3.47  
    3.48    /* text_area_extension */
    3.49  
    3.50    private val text_area_extension = new TextAreaExtension
    3.51    {
    3.52 -    override def paintValidLine(gfx: Graphics2D,
    3.53 -      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
    3.54 +    override def paintScreenLineRange(gfx: Graphics2D,
    3.55 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.56 +      start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
    3.57      {
    3.58 -      val document = model.recent_document()
    3.59 -      def from_current(pos: Int) = model.from_current(document, pos)
    3.60 -      def to_current(pos: Int) = model.to_current(document, pos)
    3.61 +      Swing_Thread.now {
    3.62 +        val document = model.recent_document()
    3.63 +        def from_current(pos: Int) = model.from_current(document, pos)
    3.64 +        def to_current(pos: Int) = model.to_current(document, pos)
    3.65  
    3.66 -      val line_end = model.visible_line_end(start, end)
    3.67 -      val line_height = text_area.getPainter.getFontMetrics.getHeight
    3.68 +        val command_range: Iterable[(Command, Int)] =
    3.69 +        {
    3.70 +          val range = document.command_range(from_current(start(0)))
    3.71 +          if (range.hasNext) {
    3.72 +            val (cmd0, start0) = range.next
    3.73 +            new Iterable[(Command, Int)] {
    3.74 +              def iterator = Document.command_starts(document.commands.iterator(cmd0), start0)
    3.75 +            }
    3.76 +          }
    3.77 +          else Iterable.empty
    3.78 +        }
    3.79  
    3.80 -      val saved_color = gfx.getColor
    3.81 -      try {
    3.82 -        for ((command, command_start) <-
    3.83 -          document.command_range(from_current(start), from_current(line_end)) if !command.is_ignored)
    3.84 -        {
    3.85 -          val p = text_area.offsetToXY(start max to_current(command_start))
    3.86 -          val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
    3.87 -          assert(p.y == q.y)
    3.88 -          gfx.setColor(Document_View.choose_color(document, command))
    3.89 -          gfx.fillRect(p.x, y, q.x - p.x, line_height)
    3.90 +        val saved_color = gfx.getColor
    3.91 +        try {
    3.92 +          var y = y0
    3.93 +          for (i <- 0 until physical_lines.length) {
    3.94 +            if (physical_lines(i) != -1) {
    3.95 +              val line_start = start(i)
    3.96 +              val line_end = model.visible_line_end(line_start, end(i))
    3.97 +
    3.98 +              val a = from_current(line_start)
    3.99 +              val b = from_current(line_end)
   3.100 +              val cmds = command_range.iterator.
   3.101 +                dropWhile { case (cmd, c) => c + cmd.length <= a } .
   3.102 +                takeWhile { case (_, c) => c < b }
   3.103 +
   3.104 +              for ((command, command_start) <- cmds if !command.is_ignored) {
   3.105 +                val p = text_area.offsetToXY(line_start max to_current(command_start))
   3.106 +                val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
   3.107 +                assert(p.y == q.y)
   3.108 +                gfx.setColor(Document_View.choose_color(document, command))
   3.109 +                gfx.fillRect(p.x, y, q.x - p.x, line_height)
   3.110 +              }
   3.111 +            }
   3.112 +            y += line_height
   3.113 +          }
   3.114          }
   3.115 +        finally { gfx.setColor(saved_color) }
   3.116        }
   3.117 -      finally { gfx.setColor(saved_color) }
   3.118      }
   3.119  
   3.120      override def getToolTipText(x: Int, y: Int): String =
   3.121 @@ -186,30 +231,6 @@
   3.122    }
   3.123  
   3.124  
   3.125 -  /* (re)painting */
   3.126 -
   3.127 -  private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
   3.128 -  // FIXME update_delay property
   3.129 -
   3.130 -  private def update_syntax(document: Document, cmd: Command)
   3.131 -  {
   3.132 -    val (line1, line2) = model.lines_of_command(document, cmd)
   3.133 -    if (line2 >= text_area.getFirstLine &&
   3.134 -      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
   3.135 -        update_delay()
   3.136 -  }
   3.137 -
   3.138 -  private def invalidate_line(document: Document, cmd: Command) =
   3.139 -  {
   3.140 -    val (start, stop) = model.lines_of_command(document, cmd)
   3.141 -    text_area.invalidateLineRange(start, stop)
   3.142 -  }
   3.143 -
   3.144 -  private def invalidate_all() =
   3.145 -    text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
   3.146 -      text_area.getLastPhysicalLine)
   3.147 -
   3.148 -
   3.149    /* overview of command status left of scrollbar */
   3.150  
   3.151    private val overview = new JPanel(new BorderLayout)
   3.152 @@ -252,9 +273,9 @@
   3.153        val buffer = model.buffer
   3.154        val document = model.recent_document()
   3.155        def to_current(pos: Int) = model.to_current(document, pos)
   3.156 -      val saved_color = gfx.getColor
   3.157 +      val saved_color = gfx.getColor  // FIXME needed!?
   3.158        try {
   3.159 -        for ((command, start) <- document.command_range(0) if !command.is_ignored) {
   3.160 +        for ((command, start) <- document.command_starts if !command.is_ignored) {
   3.161            val line1 = buffer.getLineOfOffset(to_current(start))
   3.162            val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
   3.163            val y = line_to_y(line1)