src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Tue Feb 11 09:29:46 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Feb 11 11:30:33 2014 +0100
@@ -399,6 +399,9 @@
   val SUCCESS = "success"
   val Success = new Properties.Boolean(SUCCESS)
 
+  val MEMORY = "memory"
+  val Memory = new Properties.Boolean(MEMORY)
+
   val CANCEL_SIMP_TRACE = "simp_trace_cancel"
   object Cancel_Simp_Trace
   {
@@ -454,6 +457,10 @@
 
     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
+    }
 
   }