explicit message channels for "state", "information";
separate state_message_color;
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Tue Dec 23 20:46:42 2014 +0100
@@ -58,7 +58,7 @@
(* method setup *)
fun print_cert cert =
- (writeln o Markup.markup Markup.information)
+ Output.information
("To repeat this proof with a certificate use this command:\n" ^
Active.sendback_markup [] ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Dec 23 20:46:42 2014 +0100
@@ -238,8 +238,7 @@
val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T)
fun pprint print prt =
if mode = Auto_Try then
- Synchronized.change outcome
- (Queue.enqueue (Pretty.string_of (Pretty.mark Markup.information prt)))
+ Synchronized.change outcome (Queue.enqueue (Pretty.string_of prt))
else
print (Pretty.string_of prt)
val pprint_a = pprint writeln
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Dec 23 20:46:42 2014 +0100
@@ -213,9 +213,7 @@
in
if mode = Auto_Try then
let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
- (outcome_code,
- if outcome_code = someN then [Markup.markup Markup.information (message ())]
- else [])
+ (outcome_code, if outcome_code = someN then [message ()] else [])
end
else if blocking then
let
--- a/src/HOL/Tools/try0.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/HOL/Tools/try0.ML Tue Dec 23 20:46:42 2014 +0100
@@ -147,10 +147,7 @@
[(_, ms)] => " (" ^ time_string ms ^ ")."
| xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
in
- (true,
- (name,
- if mode = Auto_Try then [Markup.markup Markup.information message]
- else (writeln message; [])))
+ (true, (name, if mode = Auto_Try then [message] else (writeln message; [])))
end)
end;
--- a/src/HOL/ex/Cartouche_Examples.thy Tue Dec 23 16:00:38 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue Dec 23 20:46:42 2014 +0100
@@ -266,7 +266,7 @@
text \<open>Input source with position information:\<close>
ML \<open>
val s: Input.source = \<open>abc123def456\<close>;
- writeln (Markup.markup Markup.information ("Look here!" ^ Position.here (Input.pos_of s)));
+ Output.information ("Look here!" ^ Position.here (Input.pos_of s));
\<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
--- a/src/Pure/General/output.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Pure/General/output.ML Tue Dec 23 20:46:42 2014 +0100
@@ -26,6 +26,8 @@
val physical_writeln: output -> unit
exception Protocol_Message of Properties.T
val writelns: string list -> unit
+ val state: string -> unit
+ val information: string -> unit
val error_message': serial * string -> unit
val error_message: string -> unit
val system_message: string -> unit
@@ -40,6 +42,8 @@
sig
include OUTPUT
val writeln_fn: (output list -> unit) Unsynchronized.ref
+ val state_fn: (output list -> unit) Unsynchronized.ref
+ val information_fn: (output list -> unit) Unsynchronized.ref
val tracing_fn: (output list -> unit) Unsynchronized.ref
val warning_fn: (output list -> unit) Unsynchronized.ref
val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
@@ -94,6 +98,8 @@
exception Protocol_Message of Properties.T;
val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
+val state_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
+val information_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
val error_message_fn =
@@ -107,6 +113,8 @@
fun writelns ss = ! writeln_fn (map output ss);
fun writeln s = writelns [s];
+fun state s = ! state_fn [output s];
+fun information s = ! information_fn [output s];
fun tracing s = ! tracing_fn [output s];
fun warning s = ! warning_fn [output s];
fun error_message' (i, s) = ! error_message_fn (i, [output s]);
--- a/src/Pure/Isar/proof.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Pure/Isar/proof.ML Tue Dec 23 20:46:42 2014 +0100
@@ -1046,8 +1046,7 @@
else if int then
Proof_Display.string_of_rule ctxt "Successful" th
|> Markup.markup Markup.text_fold
- |> Markup.markup Markup.state
- |> writeln
+ |> Output.state
else ();
val test_proof =
local_skip_proof true
--- a/src/Pure/Isar/proof_display.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Pure/Isar/proof_display.ML Tue Dec 23 20:46:42 2014 +0100
@@ -148,11 +148,11 @@
fun print_results do_print pos ctxt ((kind, name), facts) =
if not do_print orelse kind = "" then ()
else if name = "" then
- (Pretty.writeln o Pretty.mark Markup.state)
+ (Output.state o Pretty.string_of)
(Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
pretty_facts ctxt facts))
else
- (Pretty.writeln o Pretty.mark Markup.state)
+ (Output.state o Pretty.string_of)
(case facts of
[fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
Proof_Context.pretty_fact ctxt fact])
@@ -182,7 +182,7 @@
fun print_consts do_print pos ctxt pred cs =
if not do_print orelse null cs then ()
- else Pretty.writeln (Pretty.mark Markup.state (pretty_consts pos ctxt pred cs));
+ else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
end;
--- a/src/Pure/Isar/toplevel.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Tue Dec 23 20:46:42 2014 +0100
@@ -200,7 +200,7 @@
Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
| SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
-val print_state = pretty_state #> Pretty.markup_chunks Markup.state #> Pretty.writeln;
+val print_state = pretty_state #> Pretty.chunks #> Pretty.string_of #> Output.state;
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
@@ -387,7 +387,7 @@
val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
val _ =
if begin then
- Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
+ Output.state (Pretty.string_of (Pretty.chunks (Local_Theory.pretty lthy)))
else ();
in Theory (gthy, SOME lthy) end
| _ => raise UNDEF));
--- a/src/Pure/PIDE/markup.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Dec 23 20:46:42 2014 +0100
@@ -140,7 +140,6 @@
val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
val subgoalsN: string
val proof_stateN: string val proof_state: int -> T
- val stateN: string val state: T
val goalN: string val goal: T
val subgoalN: string val subgoal: string -> T
val taskN: string
@@ -157,6 +156,8 @@
val statusN: string
val resultN: string
val writelnN: string
+ val stateN: string
+ val informationN: string
val tracingN: string
val warningN: string
val errorN: string
@@ -167,7 +168,6 @@
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
@@ -516,7 +516,6 @@
val subgoalsN = "subgoals";
val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
-val (stateN, state) = markup_elem "state";
val (goalN, goal) = markup_elem "goal";
val (subgoalN, subgoal) = markup_string "subgoal" nameN;
@@ -544,6 +543,8 @@
val statusN = "status";
val resultN = "result";
val writelnN = "writeln";
+val stateN = "state"
+val informationN = "information";
val tracingN = "tracing";
val warningN = "warning";
val errorN = "error";
@@ -558,7 +559,6 @@
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 Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Dec 23 20:46:42 2014 +0100
@@ -311,7 +311,6 @@
val SUBGOALS = "subgoals"
val PROOF_STATE = "proof_state"
- val STATE = "state"
val GOAL = "goal"
val SUBGOAL = "subgoal"
@@ -352,6 +351,8 @@
val REPORT = "report"
val RESULT = "result"
val WRITELN = "writeln"
+ val STATE = "state"
+ val INFORMATION = "information"
val TRACING = "tracing"
val WARNING = "warning"
val ERROR = "error"
@@ -362,13 +363,20 @@
val EXIT = "exit"
val WRITELN_MESSAGE = "writeln_message"
+ val STATE_MESSAGE = "state_message"
+ val INFORMATION_MESSAGE = "information_message"
val TRACING_MESSAGE = "tracing_message"
val WARNING_MESSAGE = "warning_message"
val ERROR_MESSAGE = "error_message"
- val messages =
- Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
- WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
+ val messages = Map(
+ WRITELN -> WRITELN_MESSAGE,
+ STATE -> STATE_MESSAGE,
+ INFORMATION -> INFORMATION_MESSAGE,
+ TRACING -> TRACING_MESSAGE,
+ WARNING -> WARNING_MESSAGE,
+ ERROR -> ERROR_MESSAGE)
+
val message: String => String = messages.withDefault((s: String) => s)
val Return_Code = new Properties.Int("return_code")
@@ -380,7 +388,6 @@
val BAD = "bad"
val INTENSIFY = "intensify"
- val INFORMATION = "information"
/* active areas */
--- a/src/Pure/PIDE/protocol.scala Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Dec 23 20:46:42 2014 +0100
@@ -227,12 +227,17 @@
case _ => false
}
- def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
+ def is_state(msg: XML.Tree): Boolean =
msg match {
- case XML.Elem(Markup(Markup.WRITELN, _),
- List(XML.Elem(markup, _))) => markup.name == name
- case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
- List(XML.Elem(markup, _))) => markup.name == name
+ case XML.Elem(Markup(Markup.STATE, _), _) => true
+ case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true
+ case _ => false
+ }
+
+ def is_information(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
+ case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
case _ => false
}
@@ -259,8 +264,6 @@
case _ => false
}
- def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
- def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
def is_inlined(msg: XML.Tree): Boolean =
--- a/src/Pure/System/isabelle_process.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML Tue Dec 23 20:46:42 2014 +0100
@@ -118,6 +118,8 @@
Output.result_fn :=
(fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
+ Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s);
+ Output.information_fn := (fn s => standard_message (serial_props ()) Markup.informationN s);
Output.tracing_fn :=
(fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
--- a/src/Tools/jEdit/etc/options Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Tools/jEdit/etc/options Tue Dec 23 20:46:42 2014 +0100
@@ -90,6 +90,7 @@
option warning_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
option writeln_message_color : string = "F0F0F0FF"
+option state_message_color : string = "F0E4E4FF"
option information_message_color : string = "DCEAF3FF"
option tracing_message_color : string = "F0F8FFFF"
option warning_message_color : string = "EEE8AAFF"
--- a/src/Tools/jEdit/src/rendering.scala Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Tue Dec 23 20:46:42 2014 +0100
@@ -27,18 +27,27 @@
/* message priorities */
- private val writeln_pri = 1
- 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 state_pri = 1
+ private val writeln_pri = 2
+ private val information_pri = 3
+ private val tracing_pri = 4
+ private val warning_pri = 5
+ private val legacy_pri = 6
+ private val error_pri = 7
private val message_pri = Map(
- Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
- Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri,
- Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri,
- Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
+ Markup.STATE -> state_pri,
+ Markup.STATE_MESSAGE -> state_pri,
+ Markup.WRITELN -> writeln_pri,
+ Markup.WRITELN_MESSAGE -> writeln_pri,
+ Markup.INFORMATION -> information_pri,
+ Markup.INFORMATION_MESSAGE -> information_pri,
+ Markup.TRACING -> tracing_pri,
+ Markup.TRACING_MESSAGE -> tracing_pri,
+ Markup.WARNING -> warning_pri,
+ Markup.WARNING_MESSAGE -> warning_pri,
+ Markup.ERROR -> error_pri,
+ Markup.ERROR_MESSAGE -> error_pri)
/* popup window bounds */
@@ -152,7 +161,8 @@
Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
private val tooltip_message_elements =
- Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+ Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING,
+ Markup.ERROR, Markup.BAD)
private val tooltip_descriptions =
Map(
@@ -172,21 +182,21 @@
Markup.Elements(tooltip_descriptions.keySet)
private val gutter_elements =
- Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR)
private val squiggly_elements =
- Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR)
private val line_background_elements =
- Markup.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
- Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
- Markup.INFORMATION)
+ Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
+ Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
private val separator_elements =
Markup.Elements(Markup.SEPARATOR)
private val background_elements =
Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
+ Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
active_elements
@@ -224,6 +234,7 @@
val warning_color = color_value("warning_color")
val error_color = color_value("error_color")
val writeln_message_color = color_value("writeln_message_color")
+ val state_message_color = color_value("state_message_color")
val information_message_color = color_value("information_message_color")
val tracing_message_color = color_value("tracing_message_color")
val warning_message_color = color_value("warning_message_color")
@@ -448,18 +459,17 @@
snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
range, Nil, Rendering.tooltip_message_elements, _ =>
{
- case (msgs, Text.Info(info_range,
- XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
- if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
- val entry: Command.Results.Entry =
- (serial -> XML.Elem(Markup(Markup.message(name), props), body))
- Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
-
case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
if !body.isEmpty =>
val entry: Command.Results.Entry = (Document_ID.make(), msg)
Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
+ case (msgs, Text.Info(info_range,
+ XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) =>
+ val entry: Command.Results.Entry =
+ (serial -> XML.Elem(Markup(Markup.message(name), props), body))
+ Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
+
case _ => None
}).flatMap(_.info)
if (results.isEmpty) None
@@ -588,11 +598,7 @@
val results =
snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ =>
{
- case (pri, Text.Info(_, elem)) =>
- if (Protocol.is_information(elem))
- Some(pri max Rendering.information_pri)
- else
- Some(pri max Rendering.message_pri(elem.name))
+ case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
})
for {
Text.Info(r, pri) <- results
@@ -605,6 +611,7 @@
private lazy val message_colors = Map(
Rendering.writeln_pri -> writeln_message_color,
+ Rendering.state_pri -> state_message_color,
Rendering.information_pri -> information_message_color,
Rendering.tracing_pri -> tracing_message_color,
Rendering.warning_pri -> warning_message_color,
@@ -615,11 +622,7 @@
val results =
snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ =>
{
- case (pri, Text.Info(_, elem)) =>
- if (elem.name == Markup.INFORMATION)
- Some(pri max Rendering.information_pri)
- else
- Some(pri max Rendering.message_pri(elem.name))
+ case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
})
val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
--- a/src/Tools/quickcheck.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Tools/quickcheck.ML Tue Dec 23 20:46:42 2014 +0100
@@ -555,12 +555,11 @@
NONE => (unknownN, [])
| SOME results =>
let
- val msg = pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)
+ val msg =
+ Pretty.string_of
+ (pretty_counterex ctxt auto (Option.map (the o get_first response_of) results))
in
- if is_some results then
- (genuineN,
- if auto then [Pretty.string_of (Pretty.mark Markup.information msg)]
- else (writeln (Pretty.string_of msg); []))
+ if is_some results then (genuineN, if auto then [msg] else (writeln msg; []))
else (noneN, [])
end)
end
--- a/src/Tools/solve_direct.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Tools/solve_direct.ML Tue Dec 23 20:46:42 2014 +0100
@@ -76,9 +76,8 @@
(case try seek_against_goal () of
SOME (SOME results) =>
(someN,
- if mode = Auto_Try then
- [Pretty.string_of (Pretty.markup Markup.information (message results))]
- else (writeln (Pretty.string_of (Pretty.chunks (message results))); []))
+ let val msg = Pretty.string_of (Pretty.chunks (message results))
+ in if mode = Auto_Try then [msg] else (writeln msg; []) end)
| SOME NONE =>
(if mode = Normal then writeln "No proof found."
else ();
--- a/src/Tools/try.ML Tue Dec 23 16:00:38 2014 +0100
+++ b/src/Tools/try.ML Tue Dec 23 20:46:42 2014 +0100
@@ -111,7 +111,7 @@
in
if auto_time_limit > 0.0 then
(case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
- (true, (_, outcome)) => List.app writeln outcome
+ (true, (_, outcome)) => List.app Output.information outcome
| _ => ())
else ()
end handle exn => if Exn.is_interrupt exn then reraise exn else ()}