# HG changeset patch
# User wenzelm
# Date 1274465445 -7200
# Node ID d93b849cbecd3196bf3161b9067a0ce04d1c501c
# Parent  f8e24980af057bad16beffde69c55f64f09c3f07
simplified message markup, using plain XML.Elem directly;

diff -r f8e24980af05 -r d93b849cbecd src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Fri May 21 18:10:19 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-/*  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 f8e24980af05 -r d93b849cbecd src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Fri May 21 18:10:19 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Fri May 21 20:10:45 2010 +0200
@@ -74,7 +74,7 @@
   {
     val changed: State =
       message match {
-        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
+        case XML.Elem(Markup.STATUS, _, elems) =>
           (this /: elems)((state, elem) =>
             elem match {
               case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
diff -r f8e24980af05 -r d93b849cbecd src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri May 21 18:10:19 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Fri May 21 20:10:45 2010 +0200
@@ -84,7 +84,7 @@
 
   class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
   {
-    def message = Output.Message(Kind.markup(kind), props, body)
+    def message = XML.Elem(Kind.markup(kind), props, body)
 
     override def toString: String =
     {
diff -r f8e24980af05 -r d93b849cbecd src/Pure/build-jars
--- a/src/Pure/build-jars	Fri May 21 18:10:19 2010 +0200
+++ b/src/Pure/build-jars	Fri May 21 20:10:45 2010 +0200
@@ -26,7 +26,6 @@
   General/exn.scala
   General/linear_set.scala
   General/markup.scala
-  General/output.scala
   General/position.scala
   General/pretty.scala
   General/scan.scala
diff -r f8e24980af05 -r d93b849cbecd src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 18:10:19 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 20:10:45 2010 +0200
@@ -61,8 +61,8 @@
     val show_tracing = tracing.selected
     val show_debug = debug.selected
     document.current_state(cmd).results filter {
-      case Output.Message(Markup.TRACING, _, _) => show_tracing
-      case Output.Message(Markup.DEBUG, _, _) => show_debug
+      case XML.Elem(Markup.TRACING, _, _) => show_tracing
+      case XML.Elem(Markup.DEBUG, _, _) => show_debug
       case _ => true
     }
   }