src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Feb 04 09:04:59 2014 +0000
@@ -273,7 +273,8 @@
 
   /* messages */
 
-  val Serial = new Properties.Long("serial")
+  val SERIAL = "serial"
+  val Serial = new Properties.Long(SERIAL)
 
   val MESSAGE = "message"
 
@@ -386,6 +387,76 @@
         case _ => None
       }
   }
+
+  /* simplifier trace */
+
+  val TEXT = "text"
+  val Text = new Properties.String(TEXT)
+
+  val PARENT = "parent"
+  val Parent = new Properties.Long(PARENT)
+
+  val SUCCESS = "success"
+  val Success = new Properties.Boolean(SUCCESS)
+
+  val CANCEL_SIMP_TRACE = "simp_trace_cancel"
+  object Cancel_Simp_Trace
+  {
+    def unapply(props: Properties.T): Option[Long] =
+      props match {
+        case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
+        case _ => None
+      }
+  }
+
+  val SIMP_TRACE = "simp_trace"
+  object Simp_Trace
+  {
+    def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
+      tree match {
+        case XML.Elem(Markup(SIMP_TRACE, props), _) =>
+          (props, props) match {
+            case (Serial(serial), Name(name)) =>
+              Simplifier_Trace.all_answers.find(_.name == name).map((serial, _))
+            case _ =>
+              None
+          }
+        case _ =>
+          None
+      }
+  }
+
+  /* trace items from the prover */
+
+  object Simp_Trace_Item
+  {
+
+    def unapply(tree: XML.Tree): Option[(String, Data)] =
+      tree match {
+        case XML.Elem(Markup(RESULT, Serial(serial)), List(
+          XML.Elem(Markup(markup, props), content)
+        )) if markup.startsWith("simp_trace_") =>
+          (props, props) match {
+            case (Text(text), Parent(parent)) =>
+              Some((markup, Data(serial, markup, text, parent, props, content)))
+            case _ =>
+              None
+          }
+        case _ =>
+          None
+      }
+
+    val LOG = "simp_trace_log"
+    val STEP = "simp_trace_step"
+    val RECURSE = "simp_trace_recurse"
+    val HINT = "simp_trace_hint"
+    val IGNORE = "simp_trace_ignore"
+
+    case class Data(serial: Long, markup: String, text: String,
+                    parent: Long, props: Properties.T, content: XML.Body)
+
+  }
+
 }