do not highlight ignored command spans;
authorwenzelm
Sat May 29 20:34:28 2010 +0200 (2010-05-29)
changeset 37188b78ff6b4f4b3
parent 37187 dc1927a0f534
child 37189 2b4e52ecf6fc
do not highlight ignored command spans;
tuned;
src/Tools/jEdit/src/jedit/document_view.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat May 29 20:03:47 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat May 29 20:34:28 2010 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4        val saved_color = gfx.getColor
     1.5        try {
     1.6          for ((command, command_start) <-
     1.7 -          document.command_range(from_current(start), from_current(end)))
     1.8 +          document.command_range(from_current(start), from_current(end)) if !command.is_ignored)
     1.9          {
    1.10            val begin = start max to_current(command_start)
    1.11            val finish = (end - 1) min to_current(command_start + command.length)
    1.12 @@ -245,15 +245,19 @@
    1.13        super.paintComponent(gfx)
    1.14        val buffer = model.buffer
    1.15        val document = model.recent_document()
    1.16 -
    1.17 -      for ((command, start) <- document.command_range(0)) {
    1.18 -        val line1 = buffer.getLineOfOffset(model.to_current(document, start))
    1.19 -        val line2 = buffer.getLineOfOffset(model.to_current(document, start + command.length)) + 1
    1.20 -        val y = line_to_y(line1)
    1.21 -        val height = HEIGHT * (line2 - line1)
    1.22 -        gfx.setColor(Document_View.choose_color(document, command))
    1.23 -        gfx.fillRect(0, y, getWidth - 1, height)
    1.24 +      def to_current(pos: Int) = model.to_current(document, pos)
    1.25 +      val saved_color = gfx.getColor
    1.26 +      try {
    1.27 +        for ((command, start) <- document.command_range(0) if !command.is_ignored) {
    1.28 +          val line1 = buffer.getLineOfOffset(to_current(start))
    1.29 +          val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
    1.30 +          val y = line_to_y(line1)
    1.31 +          val height = HEIGHT * (line2 - line1)
    1.32 +          gfx.setColor(Document_View.choose_color(document, command))
    1.33 +          gfx.fillRect(0, y, getWidth - 1, height)
    1.34 +        }
    1.35        }
    1.36 +      finally { gfx.setColor(saved_color) }
    1.37      }
    1.38  
    1.39      private def line_to_y(line: Int): Int =