# HG changeset patch
# User wenzelm
# Date 1274446399 -7200
# Node ID 1ce1b19f78f41f5736d702db2cc48ec4c7c5920b
# Parent  35d45feccbc6f31692ba057a1ae1bb4cde25a11b
more abstract view on prover output messages;

diff -r 35d45feccbc6 -r 1ce1b19f78f4 src/Pure/General/output.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/output.scala	Fri May 21 14:53:19 2010 +0200
@@ -0,0 +1,24 @@
+/*  Title:      Pure/General/output.scala
+    Author:     Makarius
+
+Prover output messages.
+*/
+
+package isabelle
+
+
+object Output
+{
+  object Message
+  {
+    def apply(name: String, atts: XML.Attributes, body: List[XML.Tree]): XML.Tree =
+      XML.Elem(Markup.MESSAGE, (Markup.CLASS, name) :: atts, body)
+
+    def unapply(tree: XML.Tree): Option[(String, XML.Attributes, List[XML.Tree])] =
+      tree match {
+        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, name) :: atts, body) =>
+          Some(name, atts, body)
+        case _ => None
+      }
+  }
+}
diff -r 35d45feccbc6 -r 1ce1b19f78f4 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri May 21 12:59:44 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Fri May 21 14:53:19 2010 +0200
@@ -84,7 +84,7 @@
 
   class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
   {
-    def message = XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(kind)) :: props, body)
+    def message = Output.Message(Kind.markup(kind), props, body)
 
     override def toString: String =
     {
diff -r 35d45feccbc6 -r 1ce1b19f78f4 src/Pure/build-jars
--- a/src/Pure/build-jars	Fri May 21 12:59:44 2010 +0200
+++ b/src/Pure/build-jars	Fri May 21 14:53:19 2010 +0200
@@ -26,6 +26,7 @@
   General/exn.scala
   General/linear_set.scala
   General/markup.scala
+  General/output.scala
   General/position.scala
   General/pretty.scala
   General/scan.scala