more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
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, _))))