# HG changeset patch
# User wenzelm
# Date 1419364002 -3600
# Node ID 830bb7ddb3ab54637409f568ab8db5d70b3c0e01
# Parent  ec83638b6bfb25c1f86477251b04cc9316510613
explicit message channels for "state", "information";
separate state_message_color;

diff -r ec83638b6bfb -r 830bb7ddb3ab src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- 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 ^ "\")"))
 
diff -r ec83638b6bfb -r 830bb7ddb3ab src/HOL/Tools/Nitpick/nitpick.ML
--- 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
diff -r ec83638b6bfb -r 830bb7ddb3ab src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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
diff -r ec83638b6bfb -r 830bb7ddb3ab src/HOL/Tools/try0.ML
--- 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;
 
diff -r ec83638b6bfb -r 830bb7ddb3ab src/HOL/ex/Cartouche_Examples.thy
--- 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 ());
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Pure/General/output.ML
--- 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]);
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Pure/Isar/proof.ML
--- 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
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Pure/Isar/proof_display.ML
--- 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;
 
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Pure/Isar/toplevel.ML
--- 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));
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Pure/PIDE/markup.ML
--- 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 *)
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Pure/PIDE/markup.scala
--- 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 */
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Pure/PIDE/protocol.scala
--- 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 =
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Pure/System/isabelle_process.ML
--- 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);
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Tools/jEdit/etc/options
--- 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"
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Tools/jEdit/src/rendering.scala
--- 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 }
 
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Tools/quickcheck.ML
--- 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
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Tools/solve_direct.ML
--- 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 ();
diff -r ec83638b6bfb -r 830bb7ddb3ab src/Tools/try.ML
--- 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 ()}