gutter icon for information messages;
authorwenzelm
Sat Jul 13 13:58:13 2013 +0200 (2013-07-13 ago)
changeset 52644cea207576f81
parent 52643 34c29356930e
child 52645 e8c1c5612677
gutter icon for information messages;
avoid redundant Pretty.chunks to keep Markup.information node topmost;
src/HOL/Tools/Nitpick/nitpick.ML
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
src/Tools/try.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 13 13:25:42 2013 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 13 13:58:13 2013 +0200
     1.3 @@ -240,7 +240,6 @@
     1.4      fun pprint print =
     1.5        if mode = Auto_Try then
     1.6          Unsynchronized.change state_ref o Proof.goal_message o K
     1.7 -        o Pretty.chunks o single
     1.8          o Pretty.mark Markup.information
     1.9        else
    1.10          print o Pretty.string_of
     2.1 --- a/src/Tools/jEdit/etc/options	Sat Jul 13 13:25:42 2013 +0200
     2.2 +++ b/src/Tools/jEdit/etc/options	Sat Jul 13 13:58:13 2013 +0200
     2.3 @@ -76,18 +76,9 @@
     2.4  
     2.5  section "Icons"
     2.6  
     2.7 -(* jEdit/Tango *)
     2.8 -(*
     2.9 -option tooltip_close_icon : string = "16x16/actions/document-close.png"
    2.10 -option tooltip_detach_icon : string = "16x16/actions/window-new.png"
    2.11 -option gutter_warning_icon : string = "16x16/status/dialog-information.png"
    2.12 -option gutter_legacy_icon : string = "16x16/status/dialog-warning.png"
    2.13 -option gutter_error_icon : string = "16x16/status/dialog-error.png"
    2.14 -*)
    2.15 -
    2.16 -(* IntelliJ IDEA *)
    2.17  option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
    2.18  option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
    2.19 +option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
    2.20  option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
    2.21  option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
    2.22  option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 13:25:42 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 13:58:13 2013 +0200
     3.3 @@ -28,10 +28,11 @@
     3.4    /* message priorities */
     3.5  
     3.6    private val writeln_pri = 1
     3.7 -  private val tracing_pri = 2
     3.8 -  private val warning_pri = 3
     3.9 -  private val legacy_pri = 4
    3.10 -  private val error_pri = 5
    3.11 +  private val information_pri = 2
    3.12 +  private val tracing_pri = 3
    3.13 +  private val warning_pri = 4
    3.14 +  private val legacy_pri = 5
    3.15 +  private val error_pri = 6
    3.16  
    3.17    private val message_pri = Map(
    3.18      Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
    3.19 @@ -384,15 +385,21 @@
    3.20  
    3.21  
    3.22    private lazy val gutter_icons = Map(
    3.23 +    Rendering.information_pri -> Rendering.load_icon(options.string("gutter_information_icon")),
    3.24      Rendering.warning_pri -> Rendering.load_icon(options.string("gutter_warning_icon")),
    3.25      Rendering.legacy_pri -> Rendering.load_icon(options.string("gutter_legacy_icon")),
    3.26      Rendering.error_pri -> Rendering.load_icon(options.string("gutter_error_icon")))
    3.27  
    3.28 +  private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    3.29 +
    3.30    def gutter_message(range: Text.Range): Option[Icon] =
    3.31    {
    3.32      val results =
    3.33 -      snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)), _ =>
    3.34 +      snapshot.cumulate_markup[Int](range, 0, Some(gutter_elements), _ =>
    3.35          {
    3.36 +          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
    3.37 +              List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
    3.38 +            pri max Rendering.information_pri
    3.39            case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
    3.40              body match {
    3.41                case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
    3.42 @@ -412,11 +419,12 @@
    3.43      Rendering.warning_pri -> warning_color,
    3.44      Rendering.error_pri -> error_color)
    3.45  
    3.46 +  private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    3.47 +
    3.48    def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
    3.49    {
    3.50      val results =
    3.51 -      snapshot.cumulate_markup[Int](range, 0,
    3.52 -        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)), _ =>
    3.53 +      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
    3.54          {
    3.55            case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
    3.56            if name == Markup.WRITELN ||
     4.1 --- a/src/Tools/try.ML	Sat Jul 13 13:25:42 2013 +0200
     4.2 +++ b/src/Tools/try.ML	Sat Jul 13 13:58:13 2013 +0200
     4.3 @@ -130,7 +130,7 @@
     4.4                      (try o TimeLimit.timeLimit (seconds auto_time_limit))
     4.5                        (fn () => tool true state) () of
     4.6                      SOME (true, (_, state')) =>
     4.7 -                      Pretty.writeln (Pretty.chunks (Proof.pretty_goal_messages state'))
     4.8 +                      List.app Pretty.writeln (Proof.pretty_goal_messages state')
     4.9                    | _ => ())
    4.10                | NONE => ())
    4.11              else ()