src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 18:29:02 2014 +0100
@@ -389,82 +389,26 @@
       }
   }
 
+
   /* simplifier trace */
 
-  val TEXT = "text"
-  val Text = new Properties.String(TEXT)
-
-  val PARENT = "parent"
-  val Parent = new Properties.Long(PARENT)
+  val SIMP_TRACE = "simp_trace"
 
-  val SUCCESS = "success"
-  val Success = new Properties.Boolean(SUCCESS)
+  val SIMP_TRACE_LOG = "simp_trace_log"
+  val SIMP_TRACE_STEP = "simp_trace_step"
+  val SIMP_TRACE_RECURSE = "simp_trace_recurse"
+  val SIMP_TRACE_HINT = "simp_trace_hint"
+  val SIMP_TRACE_IGNORE = "simp_trace_ignore"
 
-  val MEMORY = "memory"
-  val Memory = new Properties.Boolean(MEMORY)
-
-  val CANCEL_SIMP_TRACE = "simp_trace_cancel"
-  object Cancel_Simp_Trace
+  val SIMP_TRACE_CANCEL = "simp_trace_cancel"
+  object Simp_Trace_Cancel
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
-        case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
+        case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
         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)
-    {
-      def memory: Boolean =
-        Memory.unapply(props) getOrElse true
-    }
-
-  }
-
 }