more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
authorwenzelm
Sun Jan 15 19:09:03 2012 +0100 (2012-01-15 ago)
changeset 462274aa84f84d5e8
parent 46226 e88e980ed735
child 46228 302d3ecff25d
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_rendering.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sun Jan 15 18:55:27 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Jan 15 19:09:03 2012 +0100
     1.3 @@ -43,6 +43,11 @@
     1.4  
     1.5    /* command status */
     1.6  
     1.7 +  object Status
     1.8 +  {
     1.9 +    val init = Status()
    1.10 +  }
    1.11 +
    1.12    sealed case class Status(
    1.13      private val finished: Boolean = false,
    1.14      private val failed: Boolean = false,
    1.15 @@ -52,6 +57,8 @@
    1.16      def is_running: Boolean = forks != 0
    1.17      def is_finished: Boolean = finished && forks == 0
    1.18      def is_failed: Boolean = failed && forks == 0
    1.19 +    def + (that: Status): Status =
    1.20 +      Status(finished || that.finished, failed || that.failed, forks + that.forks)
    1.21    }
    1.22  
    1.23    val command_status_markup: Set[String] =
    1.24 @@ -68,7 +75,7 @@
    1.25      }
    1.26  
    1.27    def command_status(markups: List[Markup]): Status =
    1.28 -    (Status() /: markups)(command_status(_, _))
    1.29 +    (Status.init /: markups)(command_status(_, _))
    1.30  
    1.31  
    1.32    /* node status */
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jan 15 18:55:27 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Jan 15 19:09:03 2012 +0100
     2.3 @@ -300,10 +300,9 @@
     2.4                  // gutter icons
     2.5                  Isabelle_Rendering.gutter_message(snapshot, line_range) match {
     2.6                    case Some(icon) =>
     2.7 -                    val icn = icon.icon
     2.8 -                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
     2.9 -                    val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
    2.10 -                    icn.paintIcon(gutter, gfx, x0, y0)
    2.11 +                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
    2.12 +                    val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
    2.13 +                    icon.paintIcon(gutter, gfx, x0, y0)
    2.14                    case None =>
    2.15                  }
    2.16                }
    2.17 @@ -355,6 +354,12 @@
    2.18      private val WIDTH = 10
    2.19      private val HEIGHT = 2
    2.20  
    2.21 +    private def line_to_y(line: Int): Int =
    2.22 +      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
    2.23 +
    2.24 +    private def y_to_line(y: Int): Int =
    2.25 +      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
    2.26 +
    2.27      setPreferredSize(new Dimension(WIDTH, 0))
    2.28  
    2.29      setRequestFocusEnabled(false)
    2.30 @@ -386,34 +391,22 @@
    2.31        Isabelle.buffer_lock(buffer) {
    2.32          val snapshot = update_snapshot()
    2.33  
    2.34 -        def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
    2.35 -        {
    2.36 -          try {
    2.37 -            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
    2.38 -            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
    2.39 -            Some((line1, line2))
    2.40 -          }
    2.41 -          catch { case e: ArrayIndexOutOfBoundsException => None }
    2.42 -        }
    2.43          for {
    2.44 -          (command, start) <- snapshot.node.command_starts
    2.45 -          if !command.is_ignored
    2.46 -          (line1, line2) <- line_range(command, start)
    2.47 -          val y = line_to_y(line1)
    2.48 -          val height = HEIGHT * (line2 - line1)
    2.49 -          color <- Isabelle_Rendering.overview_color(snapshot, command)
    2.50 +          line <- 0 until buffer.getLineCount
    2.51 +          range <-
    2.52 +            try {
    2.53 +              Some(proper_line_range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line)))
    2.54 +            }
    2.55 +            catch { case e: ArrayIndexOutOfBoundsException => None }
    2.56 +          color <- Isabelle_Rendering.overview_color(snapshot, range)
    2.57          } {
    2.58 +          val y = line_to_y(line)
    2.59 +          val h = (line_to_y(line + 1) - y) max 2
    2.60            gfx.setColor(color)
    2.61 -          gfx.fillRect(0, y, getWidth - 1, height)
    2.62 +          gfx.fillRect(0, y, getWidth - 1, h)
    2.63          }
    2.64        }
    2.65      }
    2.66 -
    2.67 -    private def line_to_y(line: Int): Int =
    2.68 -      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
    2.69 -
    2.70 -    private def y_to_line(y: Int): Int =
    2.71 -      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
    2.72    }
    2.73  
    2.74  
     3.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Jan 15 18:55:27 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Jan 15 19:09:03 2012 +0100
     3.3 @@ -10,6 +10,7 @@
     3.4  import isabelle._
     3.5  
     3.6  import java.awt.Color
     3.7 +import javax.swing.Icon
     3.8  
     3.9  import org.lobobrowser.util.gui.ColorFactory
    3.10  import org.gjt.sp.jedit.syntax.{Token => JEditToken}
    3.11 @@ -32,7 +33,7 @@
    3.12    val running1_color = new Color(97, 0, 97, 100)
    3.13  
    3.14    val light_color = new Color(240, 240, 240)
    3.15 -  val regular_color = new Color(192, 192, 192)
    3.16 +  val writeln_color = new Color(192, 192, 192)
    3.17    val warning_color = new Color(255, 140, 0)
    3.18    val error_color = new Color(178, 34, 34)
    3.19    val error1_color = new Color(178, 34, 34, 50)
    3.20 @@ -45,33 +46,41 @@
    3.21    val keyword1_color = get_color("#006699")
    3.22    val keyword2_color = get_color("#009966")
    3.23  
    3.24 -  class Icon(val priority: Int, val icon: javax.swing.Icon)
    3.25 -  {
    3.26 -    def >= (that: Icon): Boolean = this.priority >= that.priority
    3.27 -  }
    3.28 -  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png"))
    3.29 -  val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png"))
    3.30 -  val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
    3.31 +  private val writeln_pri = 1
    3.32 +  private val warning_pri = 2
    3.33 +  private val legacy_pri = 3
    3.34 +  private val error_pri = 4
    3.35  
    3.36  
    3.37    /* command overview */
    3.38  
    3.39 -  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    3.40 +  def overview_color(snapshot: Document.Snapshot, range: Text.Range): Option[Color] =
    3.41    {
    3.42      if (snapshot.is_outdated) None
    3.43      else {
    3.44 -      val state = snapshot.state.command_state(snapshot.version, command)
    3.45 -      val status = Protocol.command_status(state.status)
    3.46 +      val results =
    3.47 +        snapshot.cumulate_markup[(Protocol.Status, Int)](
    3.48 +          range, (Protocol.Status.init, 0),
    3.49 +          Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
    3.50 +          {
    3.51 +            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
    3.52 +              if (markup.name == Isabelle_Markup.WARNING) (status, pri max warning_pri)
    3.53 +              else if (markup.name == Isabelle_Markup.ERROR) (status, pri max error_pri)
    3.54 +              else (Protocol.command_status(status, markup), pri)
    3.55 +          })
    3.56 +      if (results.isEmpty) None
    3.57 +      else {
    3.58 +        val (status, pri) =
    3.59 +          ((Protocol.Status.init, 0) /: results) {
    3.60 +            case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
    3.61  
    3.62 -      if (status.is_unprocessed) Some(unprocessed_color)
    3.63 -      else if (status.is_running) Some(running_color)
    3.64 -      else if (status.is_finished) {
    3.65 -        if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color)
    3.66 -        else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color)
    3.67 +        if (pri == warning_pri) Some(warning_color)
    3.68 +        else if (pri == error_pri) Some(error_color)
    3.69 +        else if (status.is_unprocessed) Some(unprocessed_color)
    3.70 +        else if (status.is_running) Some(running_color)
    3.71 +        else if (status.is_failed) Some(error_color)
    3.72          else None
    3.73        }
    3.74 -      else if (status.is_failed) Some(error_color)
    3.75 -      else None
    3.76      }
    3.77    }
    3.78  
    3.79 @@ -94,32 +103,59 @@
    3.80      if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
    3.81    }
    3.82  
    3.83 +  private val gutter_icons = Map(
    3.84 +    warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
    3.85 +    legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
    3.86 +    error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
    3.87 +
    3.88    def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
    3.89 -    snapshot.select_markup(range,
    3.90 -      Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
    3.91 -      {
    3.92 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
    3.93 -          body match {
    3.94 -            case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
    3.95 -            case _ => warning_icon
    3.96 -          }
    3.97 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
    3.98 -      }).map(_.info).toList.sortWith(_ >= _).headOption
    3.99 +  {
   3.100 +    val results =
   3.101 +      snapshot.cumulate_markup[Int](range, 0,
   3.102 +        Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
   3.103 +        {
   3.104 +          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
   3.105 +            body match {
   3.106 +              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri
   3.107 +              case _ => pri max warning_pri
   3.108 +            }
   3.109 +          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
   3.110 +            pri max error_pri
   3.111 +        })
   3.112 +    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   3.113 +    gutter_icons.get(pri)
   3.114 +  }
   3.115 +
   3.116 +  private val squiggly_colors = Map(
   3.117 +    writeln_pri -> writeln_color,
   3.118 +    warning_pri -> warning_color,
   3.119 +    error_pri -> error_color)
   3.120  
   3.121    def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   3.122 -    snapshot.select_markup(range,
   3.123 -      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
   3.124 -      {
   3.125 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
   3.126 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
   3.127 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
   3.128 -      })
   3.129 +  {
   3.130 +    val results =
   3.131 +      snapshot.cumulate_markup[Int](range, 0,
   3.132 +        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
   3.133 +        {
   3.134 +          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
   3.135 +            name match {
   3.136 +              case Isabelle_Markup.WRITELN => pri max writeln_pri
   3.137 +              case Isabelle_Markup.WARNING => pri max warning_pri
   3.138 +              case Isabelle_Markup.ERROR => pri max error_pri
   3.139 +              case _ => pri
   3.140 +            }
   3.141 +        })
   3.142 +    for {
   3.143 +      Text.Info(r, pri) <- results
   3.144 +      color <- squiggly_colors.get(pri)
   3.145 +    } yield Text.Info(r, color)
   3.146 +  }
   3.147  
   3.148    def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   3.149      for {
   3.150        Text.Info(r, result) <-
   3.151          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   3.152 -          range, (Some(Protocol.Status()), None),
   3.153 +          range, (Some(Protocol.Status.init), None),
   3.154            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
   3.155            {
   3.156              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))