--- /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
+ }
+ }
+}
--- 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 =
{
--- 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