explicit message channels for "state", "information";
authorwenzelm
Tue Dec 23 20:46:42 2014 +0100 (2014-12-23 ago)
changeset 59184830bb7ddb3ab
parent 59183 ec83638b6bfb
child 59185 08ff767a82bf
explicit message channels for "state", "information";
separate state_message_color;
src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/try0.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/output.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/System/isabelle_process.ML
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Tue Dec 23 16:00:38 2014 +0100
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Tue Dec 23 20:46:42 2014 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4  (* method setup *)
     1.5  
     1.6  fun print_cert cert =
     1.7 -  (writeln o Markup.markup Markup.information)
     1.8 +  Output.information
     1.9      ("To repeat this proof with a certificate use this command:\n" ^
    1.10        Active.sendback_markup [] ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
    1.11  
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 23 16:00:38 2014 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 23 20:46:42 2014 +0100
     2.3 @@ -238,8 +238,7 @@
     2.4      val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T)
     2.5      fun pprint print prt =
     2.6        if mode = Auto_Try then
     2.7 -        Synchronized.change outcome
     2.8 -          (Queue.enqueue (Pretty.string_of (Pretty.mark Markup.information prt)))
     2.9 +        Synchronized.change outcome (Queue.enqueue (Pretty.string_of prt))
    2.10        else
    2.11          print (Pretty.string_of prt)
    2.12      val pprint_a = pprint writeln
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Dec 23 16:00:38 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Dec 23 20:46:42 2014 +0100
     3.3 @@ -213,9 +213,7 @@
     3.4    in
     3.5      if mode = Auto_Try then
     3.6        let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
     3.7 -        (outcome_code,
     3.8 -          if outcome_code = someN then [Markup.markup Markup.information (message ())]
     3.9 -          else [])
    3.10 +        (outcome_code, if outcome_code = someN then [message ()] else [])
    3.11        end
    3.12      else if blocking then
    3.13        let
     4.1 --- a/src/HOL/Tools/try0.ML	Tue Dec 23 16:00:38 2014 +0100
     4.2 +++ b/src/HOL/Tools/try0.ML	Tue Dec 23 20:46:42 2014 +0100
     4.3 @@ -147,10 +147,7 @@
     4.4              [(_, ms)] => " (" ^ time_string ms ^ ")."
     4.5            | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
     4.6        in
     4.7 -        (true,
     4.8 -          (name,
     4.9 -            if mode = Auto_Try then [Markup.markup Markup.information message]
    4.10 -            else (writeln message; [])))
    4.11 +        (true, (name, if mode = Auto_Try then [message] else (writeln message; [])))
    4.12        end)
    4.13    end;
    4.14  
     5.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Tue Dec 23 16:00:38 2014 +0100
     5.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Dec 23 20:46:42 2014 +0100
     5.3 @@ -266,7 +266,7 @@
     5.4  text \<open>Input source with position information:\<close>
     5.5  ML \<open>
     5.6    val s: Input.source = \<open>abc123def456\<close>;
     5.7 -  writeln (Markup.markup Markup.information ("Look here!" ^ Position.here (Input.pos_of s)));
     5.8 +  Output.information ("Look here!" ^ Position.here (Input.pos_of s));
     5.9  
    5.10    \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
    5.11      if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
     6.1 --- a/src/Pure/General/output.ML	Tue Dec 23 16:00:38 2014 +0100
     6.2 +++ b/src/Pure/General/output.ML	Tue Dec 23 20:46:42 2014 +0100
     6.3 @@ -26,6 +26,8 @@
     6.4    val physical_writeln: output -> unit
     6.5    exception Protocol_Message of Properties.T
     6.6    val writelns: string list -> unit
     6.7 +  val state: string -> unit
     6.8 +  val information: string -> unit
     6.9    val error_message': serial * string -> unit
    6.10    val error_message: string -> unit
    6.11    val system_message: string -> unit
    6.12 @@ -40,6 +42,8 @@
    6.13  sig
    6.14    include OUTPUT
    6.15    val writeln_fn: (output list -> unit) Unsynchronized.ref
    6.16 +  val state_fn: (output list -> unit) Unsynchronized.ref
    6.17 +  val information_fn: (output list -> unit) Unsynchronized.ref
    6.18    val tracing_fn: (output list -> unit) Unsynchronized.ref
    6.19    val warning_fn: (output list -> unit) Unsynchronized.ref
    6.20    val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    6.21 @@ -94,6 +98,8 @@
    6.22  exception Protocol_Message of Properties.T;
    6.23  
    6.24  val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
    6.25 +val state_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    6.26 +val information_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    6.27  val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    6.28  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    6.29  val error_message_fn =
    6.30 @@ -107,6 +113,8 @@
    6.31  
    6.32  fun writelns ss = ! writeln_fn (map output ss);
    6.33  fun writeln s = writelns [s];
    6.34 +fun state s = ! state_fn [output s];
    6.35 +fun information s = ! information_fn [output s];
    6.36  fun tracing s = ! tracing_fn [output s];
    6.37  fun warning s = ! warning_fn [output s];
    6.38  fun error_message' (i, s) = ! error_message_fn (i, [output s]);
     7.1 --- a/src/Pure/Isar/proof.ML	Tue Dec 23 16:00:38 2014 +0100
     7.2 +++ b/src/Pure/Isar/proof.ML	Tue Dec 23 20:46:42 2014 +0100
     7.3 @@ -1046,8 +1046,7 @@
     7.4        else if int then
     7.5          Proof_Display.string_of_rule ctxt "Successful" th
     7.6          |> Markup.markup Markup.text_fold
     7.7 -        |> Markup.markup Markup.state
     7.8 -        |> writeln
     7.9 +        |> Output.state
    7.10        else ();
    7.11      val test_proof =
    7.12        local_skip_proof true
     8.1 --- a/src/Pure/Isar/proof_display.ML	Tue Dec 23 16:00:38 2014 +0100
     8.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Dec 23 20:46:42 2014 +0100
     8.3 @@ -148,11 +148,11 @@
     8.4  fun print_results do_print pos ctxt ((kind, name), facts) =
     8.5    if not do_print orelse kind = "" then ()
     8.6    else if name = "" then
     8.7 -    (Pretty.writeln o Pretty.mark Markup.state)
     8.8 +    (Output.state o Pretty.string_of)
     8.9        (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
    8.10          pretty_facts ctxt facts))
    8.11    else
    8.12 -    (Pretty.writeln o Pretty.mark Markup.state)
    8.13 +    (Output.state o Pretty.string_of)
    8.14        (case facts of
    8.15          [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
    8.16            Proof_Context.pretty_fact ctxt fact])
    8.17 @@ -182,7 +182,7 @@
    8.18  
    8.19  fun print_consts do_print pos ctxt pred cs =
    8.20    if not do_print orelse null cs then ()
    8.21 -  else Pretty.writeln (Pretty.mark Markup.state (pretty_consts pos ctxt pred cs));
    8.22 +  else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
    8.23  
    8.24  end;
    8.25  
     9.1 --- a/src/Pure/Isar/toplevel.ML	Tue Dec 23 16:00:38 2014 +0100
     9.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Dec 23 20:46:42 2014 +0100
     9.3 @@ -200,7 +200,7 @@
     9.4        Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
     9.5    | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
     9.6  
     9.7 -val print_state = pretty_state #> Pretty.markup_chunks Markup.state #> Pretty.writeln;
     9.8 +val print_state = pretty_state #> Pretty.chunks #> Pretty.string_of #> Output.state;
     9.9  
    9.10  fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
    9.11  
    9.12 @@ -387,7 +387,7 @@
    9.13            val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
    9.14            val _ =
    9.15              if begin then
    9.16 -              Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
    9.17 +              Output.state (Pretty.string_of (Pretty.chunks (Local_Theory.pretty lthy)))
    9.18              else ();
    9.19          in Theory (gthy, SOME lthy) end
    9.20      | _ => raise UNDEF));
    10.1 --- a/src/Pure/PIDE/markup.ML	Tue Dec 23 16:00:38 2014 +0100
    10.2 +++ b/src/Pure/PIDE/markup.ML	Tue Dec 23 20:46:42 2014 +0100
    10.3 @@ -140,7 +140,6 @@
    10.4    val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
    10.5    val subgoalsN: string
    10.6    val proof_stateN: string val proof_state: int -> T
    10.7 -  val stateN: string val state: T
    10.8    val goalN: string val goal: T
    10.9    val subgoalN: string val subgoal: string -> T
   10.10    val taskN: string
   10.11 @@ -157,6 +156,8 @@
   10.12    val statusN: string
   10.13    val resultN: string
   10.14    val writelnN: string
   10.15 +  val stateN: string
   10.16 +  val informationN: string
   10.17    val tracingN: string
   10.18    val warningN: string
   10.19    val errorN: string
   10.20 @@ -167,7 +168,6 @@
   10.21    val no_reportN: string val no_report: T
   10.22    val badN: string val bad: T
   10.23    val intensifyN: string val intensify: T
   10.24 -  val informationN: string val information: T
   10.25    val browserN: string
   10.26    val graphviewN: string
   10.27    val sendbackN: string
   10.28 @@ -516,7 +516,6 @@
   10.29  val subgoalsN = "subgoals";
   10.30  val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
   10.31  
   10.32 -val (stateN, state) = markup_elem "state";
   10.33  val (goalN, goal) = markup_elem "goal";
   10.34  val (subgoalN, subgoal) = markup_string "subgoal" nameN;
   10.35  
   10.36 @@ -544,6 +543,8 @@
   10.37  val statusN = "status";
   10.38  val resultN = "result";
   10.39  val writelnN = "writeln";
   10.40 +val stateN = "state"
   10.41 +val informationN = "information";
   10.42  val tracingN = "tracing";
   10.43  val warningN = "warning";
   10.44  val errorN = "error";
   10.45 @@ -558,7 +559,6 @@
   10.46  val (badN, bad) = markup_elem "bad";
   10.47  
   10.48  val (intensifyN, intensify) = markup_elem "intensify";
   10.49 -val (informationN, information) = markup_elem "information";
   10.50  
   10.51  
   10.52  (* active areas *)
    11.1 --- a/src/Pure/PIDE/markup.scala	Tue Dec 23 16:00:38 2014 +0100
    11.2 +++ b/src/Pure/PIDE/markup.scala	Tue Dec 23 20:46:42 2014 +0100
    11.3 @@ -311,7 +311,6 @@
    11.4    val SUBGOALS = "subgoals"
    11.5    val PROOF_STATE = "proof_state"
    11.6  
    11.7 -  val STATE = "state"
    11.8    val GOAL = "goal"
    11.9    val SUBGOAL = "subgoal"
   11.10  
   11.11 @@ -352,6 +351,8 @@
   11.12    val REPORT = "report"
   11.13    val RESULT = "result"
   11.14    val WRITELN = "writeln"
   11.15 +  val STATE = "state"
   11.16 +  val INFORMATION = "information"
   11.17    val TRACING = "tracing"
   11.18    val WARNING = "warning"
   11.19    val ERROR = "error"
   11.20 @@ -362,13 +363,20 @@
   11.21    val EXIT = "exit"
   11.22  
   11.23    val WRITELN_MESSAGE = "writeln_message"
   11.24 +  val STATE_MESSAGE = "state_message"
   11.25 +  val INFORMATION_MESSAGE = "information_message"
   11.26    val TRACING_MESSAGE = "tracing_message"
   11.27    val WARNING_MESSAGE = "warning_message"
   11.28    val ERROR_MESSAGE = "error_message"
   11.29  
   11.30 -  val messages =
   11.31 -    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
   11.32 -        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
   11.33 +  val messages = Map(
   11.34 +    WRITELN -> WRITELN_MESSAGE,
   11.35 +    STATE -> STATE_MESSAGE,
   11.36 +    INFORMATION -> INFORMATION_MESSAGE,
   11.37 +    TRACING -> TRACING_MESSAGE,
   11.38 +    WARNING -> WARNING_MESSAGE,
   11.39 +    ERROR -> ERROR_MESSAGE)
   11.40 +
   11.41    val message: String => String = messages.withDefault((s: String) => s)
   11.42  
   11.43    val Return_Code = new Properties.Int("return_code")
   11.44 @@ -380,7 +388,6 @@
   11.45    val BAD = "bad"
   11.46  
   11.47    val INTENSIFY = "intensify"
   11.48 -  val INFORMATION = "information"
   11.49  
   11.50  
   11.51    /* active areas */
    12.1 --- a/src/Pure/PIDE/protocol.scala	Tue Dec 23 16:00:38 2014 +0100
    12.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Dec 23 20:46:42 2014 +0100
    12.3 @@ -227,12 +227,17 @@
    12.4        case _ => false
    12.5      }
    12.6  
    12.7 -  def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
    12.8 +  def is_state(msg: XML.Tree): Boolean =
    12.9      msg match {
   12.10 -      case XML.Elem(Markup(Markup.WRITELN, _),
   12.11 -        List(XML.Elem(markup, _))) => markup.name == name
   12.12 -      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
   12.13 -        List(XML.Elem(markup, _))) => markup.name == name
   12.14 +      case XML.Elem(Markup(Markup.STATE, _), _) => true
   12.15 +      case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true
   12.16 +      case _ => false
   12.17 +    }
   12.18 +
   12.19 +  def is_information(msg: XML.Tree): Boolean =
   12.20 +    msg match {
   12.21 +      case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
   12.22 +      case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
   12.23        case _ => false
   12.24      }
   12.25  
   12.26 @@ -259,8 +264,6 @@
   12.27        case _ => false
   12.28      }
   12.29  
   12.30 -  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
   12.31 -  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
   12.32    def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
   12.33  
   12.34    def is_inlined(msg: XML.Tree): Boolean =
    13.1 --- a/src/Pure/System/isabelle_process.ML	Tue Dec 23 16:00:38 2014 +0100
    13.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Dec 23 20:46:42 2014 +0100
    13.3 @@ -118,6 +118,8 @@
    13.4      Output.result_fn :=
    13.5        (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
    13.6      Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
    13.7 +    Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s);
    13.8 +    Output.information_fn := (fn s => standard_message (serial_props ()) Markup.informationN s);
    13.9      Output.tracing_fn :=
   13.10        (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
   13.11      Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
    14.1 --- a/src/Tools/jEdit/etc/options	Tue Dec 23 16:00:38 2014 +0100
    14.2 +++ b/src/Tools/jEdit/etc/options	Tue Dec 23 20:46:42 2014 +0100
    14.3 @@ -90,6 +90,7 @@
    14.4  option warning_color : string = "FF8C00FF"
    14.5  option error_color : string = "B22222FF"
    14.6  option writeln_message_color : string = "F0F0F0FF"
    14.7 +option state_message_color : string = "F0E4E4FF"
    14.8  option information_message_color : string = "DCEAF3FF"
    14.9  option tracing_message_color : string = "F0F8FFFF"
   14.10  option warning_message_color : string = "EEE8AAFF"
    15.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Dec 23 16:00:38 2014 +0100
    15.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Dec 23 20:46:42 2014 +0100
    15.3 @@ -27,18 +27,27 @@
    15.4  
    15.5    /* message priorities */
    15.6  
    15.7 -  private val writeln_pri = 1
    15.8 -  private val information_pri = 2
    15.9 -  private val tracing_pri = 3
   15.10 -  private val warning_pri = 4
   15.11 -  private val legacy_pri = 5
   15.12 -  private val error_pri = 6
   15.13 +  private val state_pri = 1
   15.14 +  private val writeln_pri = 2
   15.15 +  private val information_pri = 3
   15.16 +  private val tracing_pri = 4
   15.17 +  private val warning_pri = 5
   15.18 +  private val legacy_pri = 6
   15.19 +  private val error_pri = 7
   15.20  
   15.21    private val message_pri = Map(
   15.22 -    Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
   15.23 -    Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri,
   15.24 -    Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri,
   15.25 -    Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
   15.26 +    Markup.STATE -> state_pri,
   15.27 +    Markup.STATE_MESSAGE -> state_pri,
   15.28 +    Markup.WRITELN -> writeln_pri,
   15.29 +    Markup.WRITELN_MESSAGE -> writeln_pri,
   15.30 +    Markup.INFORMATION -> information_pri,
   15.31 +    Markup.INFORMATION_MESSAGE -> information_pri,
   15.32 +    Markup.TRACING -> tracing_pri,
   15.33 +    Markup.TRACING_MESSAGE -> tracing_pri,
   15.34 +    Markup.WARNING -> warning_pri,
   15.35 +    Markup.WARNING_MESSAGE -> warning_pri,
   15.36 +    Markup.ERROR -> error_pri,
   15.37 +    Markup.ERROR_MESSAGE -> error_pri)
   15.38  
   15.39  
   15.40    /* popup window bounds */
   15.41 @@ -152,7 +161,8 @@
   15.42        Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
   15.43  
   15.44    private val tooltip_message_elements =
   15.45 -    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
   15.46 +    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING,
   15.47 +      Markup.ERROR, Markup.BAD)
   15.48  
   15.49    private val tooltip_descriptions =
   15.50      Map(
   15.51 @@ -172,21 +182,21 @@
   15.52      Markup.Elements(tooltip_descriptions.keySet)
   15.53  
   15.54    private val gutter_elements =
   15.55 -    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   15.56 +    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR)
   15.57  
   15.58    private val squiggly_elements =
   15.59 -    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   15.60 +    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR)
   15.61  
   15.62    private val line_background_elements =
   15.63 -    Markup.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
   15.64 -      Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
   15.65 -      Markup.INFORMATION)
   15.66 +    Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
   15.67 +      Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
   15.68  
   15.69    private val separator_elements =
   15.70      Markup.Elements(Markup.SEPARATOR)
   15.71  
   15.72    private val background_elements =
   15.73      Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
   15.74 +      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
   15.75        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
   15.76        Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
   15.77        active_elements
   15.78 @@ -224,6 +234,7 @@
   15.79    val warning_color = color_value("warning_color")
   15.80    val error_color = color_value("error_color")
   15.81    val writeln_message_color = color_value("writeln_message_color")
   15.82 +  val state_message_color = color_value("state_message_color")
   15.83    val information_message_color = color_value("information_message_color")
   15.84    val tracing_message_color = color_value("tracing_message_color")
   15.85    val warning_message_color = color_value("warning_message_color")
   15.86 @@ -448,18 +459,17 @@
   15.87        snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
   15.88          range, Nil, Rendering.tooltip_message_elements, _ =>
   15.89          {
   15.90 -          case (msgs, Text.Info(info_range,
   15.91 -            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   15.92 -          if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
   15.93 -            val entry: Command.Results.Entry =
   15.94 -              (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   15.95 -            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   15.96 -
   15.97            case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
   15.98            if !body.isEmpty =>
   15.99              val entry: Command.Results.Entry = (Document_ID.make(), msg)
  15.100              Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
  15.101  
  15.102 +          case (msgs, Text.Info(info_range,
  15.103 +            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) =>
  15.104 +            val entry: Command.Results.Entry =
  15.105 +              (serial -> XML.Elem(Markup(Markup.message(name), props), body))
  15.106 +            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
  15.107 +
  15.108            case _ => None
  15.109          }).flatMap(_.info)
  15.110      if (results.isEmpty) None
  15.111 @@ -588,11 +598,7 @@
  15.112      val results =
  15.113        snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ =>
  15.114          {
  15.115 -          case (pri, Text.Info(_, elem)) =>
  15.116 -            if (Protocol.is_information(elem))
  15.117 -              Some(pri max Rendering.information_pri)
  15.118 -            else
  15.119 -              Some(pri max Rendering.message_pri(elem.name))
  15.120 +          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
  15.121          })
  15.122      for {
  15.123        Text.Info(r, pri) <- results
  15.124 @@ -605,6 +611,7 @@
  15.125  
  15.126    private lazy val message_colors = Map(
  15.127      Rendering.writeln_pri -> writeln_message_color,
  15.128 +    Rendering.state_pri -> state_message_color,
  15.129      Rendering.information_pri -> information_message_color,
  15.130      Rendering.tracing_pri -> tracing_message_color,
  15.131      Rendering.warning_pri -> warning_message_color,
  15.132 @@ -615,11 +622,7 @@
  15.133      val results =
  15.134        snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ =>
  15.135          {
  15.136 -          case (pri, Text.Info(_, elem)) =>
  15.137 -            if (elem.name == Markup.INFORMATION)
  15.138 -              Some(pri max Rendering.information_pri)
  15.139 -            else
  15.140 -              Some(pri max Rendering.message_pri(elem.name))
  15.141 +          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
  15.142          })
  15.143      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
  15.144  
    16.1 --- a/src/Tools/quickcheck.ML	Tue Dec 23 16:00:38 2014 +0100
    16.2 +++ b/src/Tools/quickcheck.ML	Tue Dec 23 20:46:42 2014 +0100
    16.3 @@ -555,12 +555,11 @@
    16.4        NONE => (unknownN, [])
    16.5      | SOME results =>
    16.6          let
    16.7 -          val msg = pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)
    16.8 +          val msg =
    16.9 +            Pretty.string_of
   16.10 +              (pretty_counterex ctxt auto (Option.map (the o get_first response_of) results))
   16.11          in
   16.12 -          if is_some results then
   16.13 -            (genuineN,
   16.14 -              if auto then [Pretty.string_of (Pretty.mark Markup.information msg)]
   16.15 -              else (writeln (Pretty.string_of msg); []))
   16.16 +          if is_some results then (genuineN, if auto then [msg] else (writeln msg; []))
   16.17            else (noneN, [])
   16.18          end)
   16.19    end
    17.1 --- a/src/Tools/solve_direct.ML	Tue Dec 23 16:00:38 2014 +0100
    17.2 +++ b/src/Tools/solve_direct.ML	Tue Dec 23 20:46:42 2014 +0100
    17.3 @@ -76,9 +76,8 @@
    17.4      (case try seek_against_goal () of
    17.5        SOME (SOME results) =>
    17.6          (someN,
    17.7 -          if mode = Auto_Try then
    17.8 -            [Pretty.string_of (Pretty.markup Markup.information (message results))]
    17.9 -          else (writeln (Pretty.string_of (Pretty.chunks (message results))); []))
   17.10 +          let val msg = Pretty.string_of (Pretty.chunks (message results))
   17.11 +          in if mode = Auto_Try then [msg] else (writeln msg; []) end)
   17.12      | SOME NONE =>
   17.13          (if mode = Normal then writeln "No proof found."
   17.14           else ();
    18.1 --- a/src/Tools/try.ML	Tue Dec 23 16:00:38 2014 +0100
    18.2 +++ b/src/Tools/try.ML	Tue Dec 23 20:46:42 2014 +0100
    18.3 @@ -111,7 +111,7 @@
    18.4              in
    18.5                if auto_time_limit > 0.0 then
    18.6                  (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
    18.7 -                  (true, (_, outcome)) => List.app writeln outcome
    18.8 +                  (true, (_, outcome)) => List.app Output.information outcome
    18.9                  | _ => ())
   18.10                else ()
   18.11              end handle exn => if Exn.is_interrupt exn then reraise exn else ()}