# HG changeset patch # User wenzelm # Date 1326650943 -3600 # Node ID 4aa84f84d5e8cc2bc32fb444ebc11cdfcb22a239 # Parent e88e980ed73578acffafc254db5b9a69484eb1cc more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages; diff -r e88e980ed735 -r 4aa84f84d5e8 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sun Jan 15 18:55:27 2012 +0100 +++ b/src/Pure/PIDE/protocol.scala Sun Jan 15 19:09:03 2012 +0100 @@ -43,6 +43,11 @@ /* command status */ + object Status + { + val init = Status() + } + sealed case class Status( private val finished: Boolean = false, private val failed: Boolean = false, @@ -52,6 +57,8 @@ def is_running: Boolean = forks != 0 def is_finished: Boolean = finished && forks == 0 def is_failed: Boolean = failed && forks == 0 + def + (that: Status): Status = + Status(finished || that.finished, failed || that.failed, forks + that.forks) } val command_status_markup: Set[String] = @@ -68,7 +75,7 @@ } def command_status(markups: List[Markup]): Status = - (Status() /: markups)(command_status(_, _)) + (Status.init /: markups)(command_status(_, _)) /* node status */ diff -r e88e980ed735 -r 4aa84f84d5e8 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Sun Jan 15 18:55:27 2012 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Sun Jan 15 19:09:03 2012 +0100 @@ -300,10 +300,9 @@ // gutter icons Isabelle_Rendering.gutter_message(snapshot, line_range) match { case Some(icon) => - val icn = icon.icon - val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10 - val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0) - icn.paintIcon(gutter, gfx, x0, y0) + val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10 + val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0) + icon.paintIcon(gutter, gfx, x0, y0) case None => } } @@ -355,6 +354,12 @@ private val WIDTH = 10 private val HEIGHT = 2 + private def line_to_y(line: Int): Int = + (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) + + private def y_to_line(y: Int): Int = + (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight + setPreferredSize(new Dimension(WIDTH, 0)) setRequestFocusEnabled(false) @@ -386,34 +391,22 @@ Isabelle.buffer_lock(buffer) { val snapshot = update_snapshot() - def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] = - { - try { - val line1 = buffer.getLineOfOffset(snapshot.convert(start)) - val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1 - Some((line1, line2)) - } - catch { case e: ArrayIndexOutOfBoundsException => None } - } for { - (command, start) <- snapshot.node.command_starts - if !command.is_ignored - (line1, line2) <- line_range(command, start) - val y = line_to_y(line1) - val height = HEIGHT * (line2 - line1) - color <- Isabelle_Rendering.overview_color(snapshot, command) + line <- 0 until buffer.getLineCount + range <- + try { + Some(proper_line_range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line))) + } + catch { case e: ArrayIndexOutOfBoundsException => None } + color <- Isabelle_Rendering.overview_color(snapshot, range) } { + val y = line_to_y(line) + val h = (line_to_y(line + 1) - y) max 2 gfx.setColor(color) - gfx.fillRect(0, y, getWidth - 1, height) + gfx.fillRect(0, y, getWidth - 1, h) } } } - - private def line_to_y(line: Int): Int = - (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) - - private def y_to_line(y: Int): Int = - (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight } diff -r e88e980ed735 -r 4aa84f84d5e8 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Sun Jan 15 18:55:27 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Sun Jan 15 19:09:03 2012 +0100 @@ -10,6 +10,7 @@ import isabelle._ import java.awt.Color +import javax.swing.Icon import org.lobobrowser.util.gui.ColorFactory import org.gjt.sp.jedit.syntax.{Token => JEditToken} @@ -32,7 +33,7 @@ val running1_color = new Color(97, 0, 97, 100) val light_color = new Color(240, 240, 240) - val regular_color = new Color(192, 192, 192) + val writeln_color = new Color(192, 192, 192) val warning_color = new Color(255, 140, 0) val error_color = new Color(178, 34, 34) val error1_color = new Color(178, 34, 34, 50) @@ -45,33 +46,41 @@ val keyword1_color = get_color("#006699") val keyword2_color = get_color("#009966") - class Icon(val priority: Int, val icon: javax.swing.Icon) - { - def >= (that: Icon): Boolean = this.priority >= that.priority - } - val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png")) - val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png")) - val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png")) + private val writeln_pri = 1 + private val warning_pri = 2 + private val legacy_pri = 3 + private val error_pri = 4 /* command overview */ - def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] = + def overview_color(snapshot: Document.Snapshot, range: Text.Range): Option[Color] = { if (snapshot.is_outdated) None else { - val state = snapshot.state.command_state(snapshot.version, command) - val status = Protocol.command_status(state.status) + val results = + snapshot.cumulate_markup[(Protocol.Status, Int)]( + range, (Protocol.Status.init, 0), + Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR), + { + case ((status, pri), Text.Info(_, XML.Elem(markup, _))) => + if (markup.name == Isabelle_Markup.WARNING) (status, pri max warning_pri) + else if (markup.name == Isabelle_Markup.ERROR) (status, pri max error_pri) + else (Protocol.command_status(status, markup), pri) + }) + if (results.isEmpty) None + else { + val (status, pri) = + ((Protocol.Status.init, 0) /: results) { + case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) } - if (status.is_unprocessed) Some(unprocessed_color) - else if (status.is_running) Some(running_color) - else if (status.is_finished) { - if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color) - else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color) + if (pri == warning_pri) Some(warning_color) + else if (pri == error_pri) Some(error_color) + else if (status.is_unprocessed) Some(unprocessed_color) + else if (status.is_running) Some(running_color) + else if (status.is_failed) Some(error_color) else None } - else if (status.is_failed) Some(error_color) - else None } } @@ -94,32 +103,59 @@ if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2))) } + private val gutter_icons = Map( + warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"), + legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"), + error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png")) + def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] = - snapshot.select_markup(range, - Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), - { - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) => - body match { - case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon - case _ => warning_icon - } - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon - }).map(_.info).toList.sortWith(_ >= _).headOption + { + val results = + snapshot.cumulate_markup[Int](range, 0, + Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), + { + case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) => + body match { + case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri + case _ => pri max warning_pri + } + case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) => + pri max error_pri + }) + val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 } + gutter_icons.get(pri) + } + + private val squiggly_colors = Map( + writeln_pri -> writeln_color, + warning_pri -> warning_color, + error_pri -> error_color) def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = - snapshot.select_markup(range, - Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), - { - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color - }) + { + val results = + snapshot.cumulate_markup[Int](range, 0, + Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), + { + case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) => + name match { + case Isabelle_Markup.WRITELN => pri max writeln_pri + case Isabelle_Markup.WARNING => pri max warning_pri + case Isabelle_Markup.ERROR => pri max error_pri + case _ => pri + } + }) + for { + Text.Info(r, pri) <- results + color <- squiggly_colors.get(pri) + } yield Text.Info(r, color) + } def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = for { Text.Info(r, result) <- snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])]( - range, (Some(Protocol.Status()), None), + range, (Some(Protocol.Status.init), None), Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE), { case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))