# HG changeset patch # User wenzelm # Date 1373714742 -7200 # Node ID 34c29356930e924ed0c1c575047997059bc4a01f # Parent 84eb792224a80f3103971857cddbcf00269b6164 more explicit Markup.information for messages produced by "auto" tools; diff -r 84eb792224a8 -r 34c29356930e src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 13 12:39:45 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 13 13:25:42 2013 +0200 @@ -240,8 +240,8 @@ fun pprint print = if mode = Auto_Try then Unsynchronized.change state_ref o Proof.goal_message o K - o Pretty.chunks o cons (Pretty.str "") o single - o Pretty.mark Markup.intensify + o Pretty.chunks o single + o Pretty.mark Markup.information else print o Pretty.string_of val pprint_a = pprint Output.urgent_message diff -r 84eb792224a8 -r 34c29356930e src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Jul 13 12:39:45 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Jul 13 13:25:42 2013 +0200 @@ -140,9 +140,7 @@ state |> outcome_code = someN ? Proof.goal_message (fn () => - [Pretty.str "", - Pretty.mark Markup.intensify (Pretty.str (message ()))] - |> Pretty.chunks)) + Pretty.mark Markup.information (Pretty.str (message ())))) end else if blocking then let diff -r 84eb792224a8 -r 34c29356930e src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Sat Jul 13 12:39:45 2013 +0200 +++ b/src/HOL/Tools/try0.ML Sat Jul 13 13:25:42 2013 +0200 @@ -140,13 +140,12 @@ Active.sendback_markup ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^ - "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" + "\n(" ^ space_implode "; " (map time_string xs) ^ ")." in (true, (s, st |> (if mode = Auto_Try then Proof.goal_message - (fn () => Pretty.chunks [Pretty.str "", - Pretty.markup Markup.intensify - [Pretty.str message]]) + (fn () => Pretty.markup Markup.information + [Pretty.str message]) else tap (fn _ => Output.urgent_message message)))) end diff -r 84eb792224a8 -r 34c29356930e src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Jul 13 12:39:45 2013 +0200 +++ b/src/Pure/PIDE/markup.ML Sat Jul 13 13:25:42 2013 +0200 @@ -133,6 +133,7 @@ val no_reportN: string val no_report: T val badN: string val bad: T val intensifyN: string val intensify: T + val informationN: string val information: T val browserN: string val graphviewN: string val sendbackN: string @@ -440,6 +441,7 @@ val (badN, bad) = markup_elem "bad"; val (intensifyN, intensify) = markup_elem "intensify"; +val (informationN, information) = markup_elem "information"; (* active areas *) diff -r 84eb792224a8 -r 34c29356930e src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Jul 13 12:39:45 2013 +0200 +++ b/src/Pure/PIDE/markup.scala Sat Jul 13 13:25:42 2013 +0200 @@ -293,6 +293,7 @@ val BAD = "bad" val INTENSIFY = "intensify" + val INFORMATION = "information" /* active areas */ diff -r 84eb792224a8 -r 34c29356930e src/Pure/Tools/proof_general.ML --- a/src/Pure/Tools/proof_general.ML Sat Jul 13 12:39:45 2013 +0200 +++ b/src/Pure/Tools/proof_general.ML Sat Jul 13 13:25:42 2013 +0200 @@ -230,6 +230,7 @@ else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") else if name = Markup.sendbackN then (special "W", special "X") else if name = Markup.intensifyN then (special "0", special "1") + else if name = Markup.informationN then ("\n" ^ special "0", special "1") else if name = Markup.tfreeN then (special "C", special "A") else if name = Markup.tvarN then (special "D", special "A") else if name = Markup.freeN then (special "E", special "A") diff -r 84eb792224a8 -r 34c29356930e src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Jul 13 12:39:45 2013 +0200 +++ b/src/Tools/jEdit/etc/options Sat Jul 13 13:25:42 2013 +0200 @@ -51,6 +51,7 @@ option error_message_color : string = "FFC1C1FF" option bad_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" +option information_color : string = "FFCC6632" option quoted_color : string = "8B8B8B19" option antiquoted_color : string = "FFC83219" option highlight_color : string = "50505032" diff -r 84eb792224a8 -r 34c29356930e src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Sat Jul 13 12:39:45 2013 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Sat Jul 13 13:25:42 2013 +0200 @@ -132,6 +132,7 @@ val error_message_color = color_value("error_message_color") val bad_color = color_value("bad_color") val intensify_color = color_value("intensify_color") + val information_color = color_value("information_color") val quoted_color = color_value("quoted_color") val antiquoted_color = color_value("antiquoted_color") val highlight_color = color_value("highlight_color") @@ -469,8 +470,8 @@ private val background1_include = Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE + - Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++ - active_include + Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY + + Markup.INFORMATION ++ active_include def background1(range: Text.Range): Stream[Text.Info[Color]] = { @@ -488,6 +489,8 @@ (None, Some(bad_color)) case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => (None, Some(intensify_color)) + case (_, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) => + (None, Some(information_color)) case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => command_state.results.get(serial) match { case Some(Protocol.Dialog_Result(res)) if res == result => diff -r 84eb792224a8 -r 34c29356930e src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sat Jul 13 12:39:45 2013 +0200 +++ b/src/Tools/quickcheck.ML Sat Jul 13 13:25:42 2013 +0200 @@ -553,8 +553,7 @@ (genuineN, state |> (if auto then - Proof.goal_message (K (Pretty.chunks [Pretty.str "", - Pretty.mark Markup.intensify msg])) + Proof.goal_message (K (Pretty.mark Markup.information msg)) else tap (fn _ => Output.urgent_message (Pretty.string_of msg)))) else diff -r 84eb792224a8 -r 34c29356930e src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Sat Jul 13 12:39:45 2013 +0200 +++ b/src/Tools/solve_direct.ML Sat Jul 13 13:25:42 2013 +0200 @@ -85,8 +85,7 @@ (if mode = Auto_Try then Proof.goal_message (fn () => - Pretty.chunks - [Pretty.str "", Pretty.markup Markup.intensify (message results)]) + Pretty.markup Markup.information (message results)) else tap (fn _ => Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))