Document_View: select gutter message icons from markup over line range, not full range results;
tuned;
--- a/src/Pure/PIDE/isar_document.scala Tue Sep 07 23:53:27 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Tue Sep 07 23:59:14 2010 +0200
@@ -56,21 +56,6 @@
}
- /* result messages */
-
- def is_warning(msg: XML.Tree): Boolean =
- msg match {
- case XML.Elem(Markup(Markup.WARNING, _), _) => true
- case _ => false
- }
-
- def is_error(msg: XML.Tree): Boolean =
- msg match {
- case XML.Elem(Markup(Markup.ERROR, _), _) => true
- case _ => false
- }
-
-
/* reported positions */
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
--- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Sep 07 23:53:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Sep 07 23:59:14 2010 +0200
@@ -245,7 +245,6 @@
for {
Text.Info(range, Some(color)) <-
snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
- if color != null
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
@@ -299,20 +298,17 @@
val line_range = proper_line_range(start(i), end(i))
// gutter icons
- val cmds = snapshot.node.command_range(snapshot.revert(line_range))
- val states = cmds.map(p => snapshot.state(p._1)).toStream
- val opt_icon =
- if (states.exists(_.results.exists(p => Isar_Document.is_error(p._2))))
- Some(Isabelle_Markup.error_icon)
- else if (states.exists(_.results.exists(p => Isar_Document.is_warning(p._2))))
- Some(Isabelle_Markup.warning_icon)
- else None
- opt_icon match {
- case Some(icon) if icon.getIconWidth > 0 && icon.getIconHeight > 0 =>
- 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 _ =>
+ val icons =
+ (for (Text.Info(_, Some(icon)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
+ yield icon).toList.sortWith(_ >= _)
+ icons match {
+ case 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)
+ case Nil =>
}
}
}
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Tue Sep 07 23:53:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Tue Sep 07 23:59:14 2010 +0200
@@ -27,8 +27,12 @@
val error_color = new Color(255, 80, 80)
val bad_color = new Color(255, 204, 153, 100)
- val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
- val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
+ class Icon(val priority: Int, val icon: javax.swing.Icon)
+ {
+ def >= (that: Icon): Boolean = this.priority >= that.priority
+ }
+ val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
+ val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
/* command status */
@@ -77,6 +81,12 @@
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
}
+ val gutter_message: Markup_Tree.Select[Icon] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+ }
+
val background: Markup_Tree.Select[Color] =
{
case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color