--- 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
--- 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
--- 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
--- 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 *)
--- 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 */
--- 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")
--- 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"
--- 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 =>
--- 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
--- 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))))))