# HG changeset patch
# User wenzelm
# Date 1373716693 -7200
# Node ID cea207576f8132c29043f700ca327466170bf7df
# Parent  34c29356930e924ed0c1c575047997059bc4a01f
gutter icon for information messages;
avoid redundant Pretty.chunks to keep Markup.information node topmost;

diff -r 34c29356930e -r cea207576f81 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 13 13:25:42 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 13 13:58:13 2013 +0200
@@ -240,7 +240,6 @@
     fun pprint print =
       if mode = Auto_Try then
         Unsynchronized.change state_ref o Proof.goal_message o K
-        o Pretty.chunks o single
         o Pretty.mark Markup.information
       else
         print o Pretty.string_of
diff -r 34c29356930e -r cea207576f81 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Jul 13 13:25:42 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Jul 13 13:58:13 2013 +0200
@@ -76,18 +76,9 @@
 
 section "Icons"
 
-(* jEdit/Tango *)
-(*
-option tooltip_close_icon : string = "16x16/actions/document-close.png"
-option tooltip_detach_icon : string = "16x16/actions/window-new.png"
-option gutter_warning_icon : string = "16x16/status/dialog-information.png"
-option gutter_legacy_icon : string = "16x16/status/dialog-warning.png"
-option gutter_error_icon : string = "16x16/status/dialog-error.png"
-*)
-
-(* IntelliJ IDEA *)
 option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
 option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
+option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
 option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
 option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
 option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
diff -r 34c29356930e -r cea207576f81 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 13:25:42 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 13:58:13 2013 +0200
@@ -28,10 +28,11 @@
   /* message priorities */
 
   private val writeln_pri = 1
-  private val tracing_pri = 2
-  private val warning_pri = 3
-  private val legacy_pri = 4
-  private val error_pri = 5
+  private val information_pri = 2
+  private val tracing_pri = 3
+  private val warning_pri = 4
+  private val legacy_pri = 5
+  private val error_pri = 6
 
   private val message_pri = Map(
     Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
@@ -384,15 +385,21 @@
 
 
   private lazy val gutter_icons = Map(
+    Rendering.information_pri -> Rendering.load_icon(options.string("gutter_information_icon")),
     Rendering.warning_pri -> Rendering.load_icon(options.string("gutter_warning_icon")),
     Rendering.legacy_pri -> Rendering.load_icon(options.string("gutter_legacy_icon")),
     Rendering.error_pri -> Rendering.load_icon(options.string("gutter_error_icon")))
 
+  private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+
   def gutter_message(range: Text.Range): Option[Icon] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)), _ =>
+      snapshot.cumulate_markup[Int](range, 0, Some(gutter_elements), _ =>
         {
+          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
+              List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
+            pri max Rendering.information_pri
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
             body match {
               case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
@@ -412,11 +419,12 @@
     Rendering.warning_pri -> warning_color,
     Rendering.error_pri -> error_color)
 
+  private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+
   def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0,
-        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)), _ =>
+      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
         {
           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
           if name == Markup.WRITELN ||
diff -r 34c29356930e -r cea207576f81 src/Tools/try.ML
--- a/src/Tools/try.ML	Sat Jul 13 13:25:42 2013 +0200
+++ b/src/Tools/try.ML	Sat Jul 13 13:58:13 2013 +0200
@@ -130,7 +130,7 @@
                     (try o TimeLimit.timeLimit (seconds auto_time_limit))
                       (fn () => tool true state) () of
                     SOME (true, (_, state')) =>
-                      Pretty.writeln (Pretty.chunks (Proof.pretty_goal_messages state'))
+                      List.app Pretty.writeln (Proof.pretty_goal_messages state')
                   | _ => ())
               | NONE => ())
             else ()