src/Pure/PIDE/markup.scala
changeset 55555 99409ccbe04a
parent 55553 4a5f65df29fa
child 55615 bf4bbe72f740
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 18 17:26:13 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 18:29:02 2014 +0100
     1.3 @@ -389,82 +389,26 @@
     1.4        }
     1.5    }
     1.6  
     1.7 +
     1.8    /* simplifier trace */
     1.9  
    1.10 -  val TEXT = "text"
    1.11 -  val Text = new Properties.String(TEXT)
    1.12 -
    1.13 -  val PARENT = "parent"
    1.14 -  val Parent = new Properties.Long(PARENT)
    1.15 +  val SIMP_TRACE = "simp_trace"
    1.16  
    1.17 -  val SUCCESS = "success"
    1.18 -  val Success = new Properties.Boolean(SUCCESS)
    1.19 +  val SIMP_TRACE_LOG = "simp_trace_log"
    1.20 +  val SIMP_TRACE_STEP = "simp_trace_step"
    1.21 +  val SIMP_TRACE_RECURSE = "simp_trace_recurse"
    1.22 +  val SIMP_TRACE_HINT = "simp_trace_hint"
    1.23 +  val SIMP_TRACE_IGNORE = "simp_trace_ignore"
    1.24  
    1.25 -  val MEMORY = "memory"
    1.26 -  val Memory = new Properties.Boolean(MEMORY)
    1.27 -
    1.28 -  val CANCEL_SIMP_TRACE = "simp_trace_cancel"
    1.29 -  object Cancel_Simp_Trace
    1.30 +  val SIMP_TRACE_CANCEL = "simp_trace_cancel"
    1.31 +  object Simp_Trace_Cancel
    1.32    {
    1.33      def unapply(props: Properties.T): Option[Long] =
    1.34        props match {
    1.35 -        case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
    1.36 +        case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
    1.37          case _ => None
    1.38        }
    1.39    }
    1.40 -
    1.41 -  val SIMP_TRACE = "simp_trace"
    1.42 -  object Simp_Trace
    1.43 -  {
    1.44 -    def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
    1.45 -      tree match {
    1.46 -        case XML.Elem(Markup(SIMP_TRACE, props), _) =>
    1.47 -          (props, props) match {
    1.48 -            case (Serial(serial), Name(name)) =>
    1.49 -              Simplifier_Trace.all_answers.find(_.name == name).map((serial, _))
    1.50 -            case _ =>
    1.51 -              None
    1.52 -          }
    1.53 -        case _ =>
    1.54 -          None
    1.55 -      }
    1.56 -  }
    1.57 -
    1.58 -  /* trace items from the prover */
    1.59 -
    1.60 -  object Simp_Trace_Item
    1.61 -  {
    1.62 -
    1.63 -    def unapply(tree: XML.Tree): Option[(String, Data)] =
    1.64 -      tree match {
    1.65 -        case XML.Elem(Markup(RESULT, Serial(serial)), List(
    1.66 -          XML.Elem(Markup(markup, props), content)
    1.67 -        )) if markup.startsWith("simp_trace_") =>
    1.68 -          (props, props) match {
    1.69 -            case (Text(text), Parent(parent)) =>
    1.70 -              Some((markup, Data(serial, markup, text, parent, props, content)))
    1.71 -            case _ =>
    1.72 -              None
    1.73 -          }
    1.74 -        case _ =>
    1.75 -          None
    1.76 -      }
    1.77 -
    1.78 -    val LOG = "simp_trace_log"
    1.79 -    val STEP = "simp_trace_step"
    1.80 -    val RECURSE = "simp_trace_recurse"
    1.81 -    val HINT = "simp_trace_hint"
    1.82 -    val IGNORE = "simp_trace_ignore"
    1.83 -
    1.84 -    case class Data(serial: Long, markup: String, text: String,
    1.85 -                    parent: Long, props: Properties.T, content: XML.Body)
    1.86 -    {
    1.87 -      def memory: Boolean =
    1.88 -        Memory.unapply(props) getOrElse true
    1.89 -    }
    1.90 -
    1.91 -  }
    1.92 -
    1.93  }
    1.94  
    1.95