Result.toString: XML output of status messages;
authorwenzelm
Thu, 15 Jan 2009 17:22:38 +0100
changeset 29506 71f00a2c6dbd
parent 29500 8fd3c1c7f0cb
child 29507 1684a9c4554f
Result.toString: XML output of status messages;
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 + "]]"
     }