src/Pure/PIDE/markup.scala
changeset 55390 36550a4eac5e
parent 55316 885500f4aa6a
child 55505 2a1ca7f6607b
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 11 09:29:46 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 11 11:30:33 2014 +0100
     1.3 @@ -399,6 +399,9 @@
     1.4    val SUCCESS = "success"
     1.5    val Success = new Properties.Boolean(SUCCESS)
     1.6  
     1.7 +  val MEMORY = "memory"
     1.8 +  val Memory = new Properties.Boolean(MEMORY)
     1.9 +
    1.10    val CANCEL_SIMP_TRACE = "simp_trace_cancel"
    1.11    object Cancel_Simp_Trace
    1.12    {
    1.13 @@ -454,6 +457,10 @@
    1.14  
    1.15      case class Data(serial: Long, markup: String, text: String,
    1.16                      parent: Long, props: Properties.T, content: XML.Body)
    1.17 +    {
    1.18 +      def memory: Boolean =
    1.19 +        Memory.unapply(props) getOrElse true
    1.20 +    }
    1.21  
    1.22    }
    1.23