more explicit Markup.information for messages produced by "auto" tools;
authorwenzelm
Sat Jul 13 13:25:42 2013 +0200 (2013-07-13 ago)
changeset 5264334c29356930e
parent 52642 84eb792224a8
child 52644 cea207576f81
more explicit Markup.information for messages produced by "auto" tools;
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/Tools/try0.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Tools/proof_general.ML
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 13 12:39:45 2013 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 13 13:25:42 2013 +0200
     1.3 @@ -240,8 +240,8 @@
     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 cons (Pretty.str "") o single
     1.8 -        o Pretty.mark Markup.intensify
     1.9 +        o Pretty.chunks o single
    1.10 +        o Pretty.mark Markup.information
    1.11        else
    1.12          print o Pretty.string_of
    1.13      val pprint_a = pprint Output.urgent_message
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Jul 13 12:39:45 2013 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Jul 13 13:25:42 2013 +0200
     2.3 @@ -140,9 +140,7 @@
     2.4           state
     2.5           |> outcome_code = someN
     2.6              ? Proof.goal_message (fn () =>
     2.7 -                  [Pretty.str "",
     2.8 -                   Pretty.mark Markup.intensify (Pretty.str (message ()))]
     2.9 -                  |> Pretty.chunks))
    2.10 +                  Pretty.mark Markup.information (Pretty.str (message ()))))
    2.11        end
    2.12      else if blocking then
    2.13        let
     3.1 --- a/src/HOL/Tools/try0.ML	Sat Jul 13 12:39:45 2013 +0200
     3.2 +++ b/src/HOL/Tools/try0.ML	Sat Jul 13 13:25:42 2013 +0200
     3.3 @@ -140,13 +140,12 @@
     3.4            Active.sendback_markup
     3.5                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
     3.6                  else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
     3.7 -          "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
     3.8 +          "\n(" ^ space_implode "; " (map time_string xs) ^ ")."
     3.9        in
    3.10          (true, (s, st |> (if mode = Auto_Try then
    3.11                              Proof.goal_message
    3.12 -                                (fn () => Pretty.chunks [Pretty.str "",
    3.13 -                                          Pretty.markup Markup.intensify
    3.14 -                                                        [Pretty.str message]])
    3.15 +                                (fn () => Pretty.markup Markup.information
    3.16 +                                                        [Pretty.str message])
    3.17                            else
    3.18                              tap (fn _ => Output.urgent_message message))))
    3.19        end
     4.1 --- a/src/Pure/PIDE/markup.ML	Sat Jul 13 12:39:45 2013 +0200
     4.2 +++ b/src/Pure/PIDE/markup.ML	Sat Jul 13 13:25:42 2013 +0200
     4.3 @@ -133,6 +133,7 @@
     4.4    val no_reportN: string val no_report: T
     4.5    val badN: string val bad: T
     4.6    val intensifyN: string val intensify: T
     4.7 +  val informationN: string val information: T
     4.8    val browserN: string
     4.9    val graphviewN: string
    4.10    val sendbackN: string
    4.11 @@ -440,6 +441,7 @@
    4.12  val (badN, bad) = markup_elem "bad";
    4.13  
    4.14  val (intensifyN, intensify) = markup_elem "intensify";
    4.15 +val (informationN, information) = markup_elem "information";
    4.16  
    4.17  
    4.18  (* active areas *)
     5.1 --- a/src/Pure/PIDE/markup.scala	Sat Jul 13 12:39:45 2013 +0200
     5.2 +++ b/src/Pure/PIDE/markup.scala	Sat Jul 13 13:25:42 2013 +0200
     5.3 @@ -293,6 +293,7 @@
     5.4    val BAD = "bad"
     5.5  
     5.6    val INTENSIFY = "intensify"
     5.7 +  val INFORMATION = "information"
     5.8  
     5.9  
    5.10    /* active areas */
     6.1 --- a/src/Pure/Tools/proof_general.ML	Sat Jul 13 12:39:45 2013 +0200
     6.2 +++ b/src/Pure/Tools/proof_general.ML	Sat Jul 13 13:25:42 2013 +0200
     6.3 @@ -230,6 +230,7 @@
     6.4                else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
     6.5                else if name = Markup.sendbackN then (special "W", special "X")
     6.6                else if name = Markup.intensifyN then (special "0", special "1")
     6.7 +              else if name = Markup.informationN then ("\n" ^ special "0", special "1")
     6.8                else if name = Markup.tfreeN then (special "C", special "A")
     6.9                else if name = Markup.tvarN then (special "D", special "A")
    6.10                else if name = Markup.freeN then (special "E", special "A")
     7.1 --- a/src/Tools/jEdit/etc/options	Sat Jul 13 12:39:45 2013 +0200
     7.2 +++ b/src/Tools/jEdit/etc/options	Sat Jul 13 13:25:42 2013 +0200
     7.3 @@ -51,6 +51,7 @@
     7.4  option error_message_color : string = "FFC1C1FF"
     7.5  option bad_color : string = "FF6A6A64"
     7.6  option intensify_color : string = "FFCC6664"
     7.7 +option information_color : string = "FFCC6632"
     7.8  option quoted_color : string = "8B8B8B19"
     7.9  option antiquoted_color : string = "FFC83219"
    7.10  option highlight_color : string = "50505032"
     8.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 12:39:45 2013 +0200
     8.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 13:25:42 2013 +0200
     8.3 @@ -132,6 +132,7 @@
     8.4    val error_message_color = color_value("error_message_color")
     8.5    val bad_color = color_value("bad_color")
     8.6    val intensify_color = color_value("intensify_color")
     8.7 +  val information_color = color_value("information_color")
     8.8    val quoted_color = color_value("quoted_color")
     8.9    val antiquoted_color = color_value("antiquoted_color")
    8.10    val highlight_color = color_value("highlight_color")
    8.11 @@ -469,8 +470,8 @@
    8.12  
    8.13    private val background1_include =
    8.14      Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
    8.15 -      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
    8.16 -      active_include
    8.17 +      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
    8.18 +      Markup.INFORMATION ++ active_include
    8.19  
    8.20    def background1(range: Text.Range): Stream[Text.Info[Color]] =
    8.21    {
    8.22 @@ -488,6 +489,8 @@
    8.23                  (None, Some(bad_color))
    8.24                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    8.25                  (None, Some(intensify_color))
    8.26 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
    8.27 +                (None, Some(information_color))
    8.28                case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    8.29                  command_state.results.get(serial) match {
    8.30                    case Some(Protocol.Dialog_Result(res)) if res == result =>
     9.1 --- a/src/Tools/quickcheck.ML	Sat Jul 13 12:39:45 2013 +0200
     9.2 +++ b/src/Tools/quickcheck.ML	Sat Jul 13 13:25:42 2013 +0200
     9.3 @@ -553,8 +553,7 @@
     9.4              (genuineN,
     9.5               state
     9.6               |> (if auto then
     9.7 -                   Proof.goal_message (K (Pretty.chunks [Pretty.str "",
     9.8 -                       Pretty.mark Markup.intensify msg]))
     9.9 +                   Proof.goal_message (K (Pretty.mark Markup.information msg))
    9.10                   else
    9.11                     tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
    9.12            else
    10.1 --- a/src/Tools/solve_direct.ML	Sat Jul 13 12:39:45 2013 +0200
    10.2 +++ b/src/Tools/solve_direct.ML	Sat Jul 13 13:25:42 2013 +0200
    10.3 @@ -85,8 +85,7 @@
    10.4              (if mode = Auto_Try then
    10.5                 Proof.goal_message
    10.6                   (fn () =>
    10.7 -                   Pretty.chunks
    10.8 -                    [Pretty.str "", Pretty.markup Markup.intensify (message results)])
    10.9 +                   Pretty.markup Markup.information (message results))
   10.10               else
   10.11                 tap (fn _ =>
   10.12                   Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))