--- 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
}
--- 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, _))))