# HG changeset patch
# User wenzelm
# Date 1232036558 -3600
# Node ID 71f00a2c6dbd32a9aba77b4985fcdc90f02c2123
# Parent  8fd3c1c7f0cb6391b747051cacbe87779550d784
Result.toString: XML output of status messages;

diff -r 8fd3c1c7f0cb -r 71f00a2c6dbd src/Pure/Tools/isabelle_process.scala
--- a/src/Pure/Tools/isabelle_process.scala	Thu Jan 15 15:51:50 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.scala	Thu Jan 15 17:22:38 2009 +0100
@@ -67,7 +67,8 @@
 
   class Result(val kind: Kind.Value, val props: Properties, val result: String) {
     override def toString = {
-      val res = XML.content(YXML.parse_failsafe(result)).mkString
+      val tree = YXML.parse_failsafe(result)
+      val res = if (kind == Kind.STATUS) tree.toString else XML.content(tree).mkString
       if (props == null) kind.toString + " [[" + res + "]]"
       else kind.toString + " " + props.toString + " [[" + res + "]]"
     }