more standard names for protocol and markup elements;
authorwenzelm
Tue Feb 18 18:29:02 2014 +0100 (2014-02-18)
changeset 5555399409ccbe04a
parent 55552 e4907b74a347
child 55554 d77090e07000
more standard names for protocol and markup elements;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Tools/simplifier_trace.ML
src/Pure/Tools/simplifier_trace.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue Feb 18 17:26:13 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Tue Feb 18 18:29:02 2014 +0100
     1.3 @@ -164,6 +164,12 @@
     1.4    val command_timing: Properties.entry
     1.5    val loading_theory: string -> Properties.T
     1.6    val dest_loading_theory: Properties.T -> string option
     1.7 +  val simp_trace_logN: string
     1.8 +  val simp_trace_stepN: string
     1.9 +  val simp_trace_recurseN: string
    1.10 +  val simp_trace_hintN: string
    1.11 +  val simp_trace_ignoreN: string
    1.12 +  val simp_trace_cancel: serial -> Properties.T
    1.13    val no_output: Output.output * Output.output
    1.14    val default_output: T -> Output.output * Output.output
    1.15    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    1.16 @@ -516,6 +522,16 @@
    1.17    | dest_loading_theory _ = NONE;
    1.18  
    1.19  
    1.20 +(* simplifier trace *)
    1.21 +
    1.22 +val simp_trace_logN = "simp_trace_log";
    1.23 +val simp_trace_stepN = "simp_trace_step";
    1.24 +val simp_trace_recurseN = "simp_trace_recurse";
    1.25 +val simp_trace_hintN = "simp_trace_hint";
    1.26 +val simp_trace_ignoreN = "simp_trace_ignore";
    1.27 +
    1.28 +fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)];
    1.29 +
    1.30  
    1.31  (** print mode operations **)
    1.32  
     2.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 18 17:26:13 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 18:29:02 2014 +0100
     2.3 @@ -389,82 +389,26 @@
     2.4        }
     2.5    }
     2.6  
     2.7 +
     2.8    /* simplifier trace */
     2.9  
    2.10 -  val TEXT = "text"
    2.11 -  val Text = new Properties.String(TEXT)
    2.12 -
    2.13 -  val PARENT = "parent"
    2.14 -  val Parent = new Properties.Long(PARENT)
    2.15 +  val SIMP_TRACE = "simp_trace"
    2.16  
    2.17 -  val SUCCESS = "success"
    2.18 -  val Success = new Properties.Boolean(SUCCESS)
    2.19 +  val SIMP_TRACE_LOG = "simp_trace_log"
    2.20 +  val SIMP_TRACE_STEP = "simp_trace_step"
    2.21 +  val SIMP_TRACE_RECURSE = "simp_trace_recurse"
    2.22 +  val SIMP_TRACE_HINT = "simp_trace_hint"
    2.23 +  val SIMP_TRACE_IGNORE = "simp_trace_ignore"
    2.24  
    2.25 -  val MEMORY = "memory"
    2.26 -  val Memory = new Properties.Boolean(MEMORY)
    2.27 -
    2.28 -  val CANCEL_SIMP_TRACE = "simp_trace_cancel"
    2.29 -  object Cancel_Simp_Trace
    2.30 +  val SIMP_TRACE_CANCEL = "simp_trace_cancel"
    2.31 +  object Simp_Trace_Cancel
    2.32    {
    2.33      def unapply(props: Properties.T): Option[Long] =
    2.34        props match {
    2.35 -        case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
    2.36 +        case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
    2.37          case _ => None
    2.38        }
    2.39    }
    2.40 -
    2.41 -  val SIMP_TRACE = "simp_trace"
    2.42 -  object Simp_Trace
    2.43 -  {
    2.44 -    def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
    2.45 -      tree match {
    2.46 -        case XML.Elem(Markup(SIMP_TRACE, props), _) =>
    2.47 -          (props, props) match {
    2.48 -            case (Serial(serial), Name(name)) =>
    2.49 -              Simplifier_Trace.all_answers.find(_.name == name).map((serial, _))
    2.50 -            case _ =>
    2.51 -              None
    2.52 -          }
    2.53 -        case _ =>
    2.54 -          None
    2.55 -      }
    2.56 -  }
    2.57 -
    2.58 -  /* trace items from the prover */
    2.59 -
    2.60 -  object Simp_Trace_Item
    2.61 -  {
    2.62 -
    2.63 -    def unapply(tree: XML.Tree): Option[(String, Data)] =
    2.64 -      tree match {
    2.65 -        case XML.Elem(Markup(RESULT, Serial(serial)), List(
    2.66 -          XML.Elem(Markup(markup, props), content)
    2.67 -        )) if markup.startsWith("simp_trace_") =>
    2.68 -          (props, props) match {
    2.69 -            case (Text(text), Parent(parent)) =>
    2.70 -              Some((markup, Data(serial, markup, text, parent, props, content)))
    2.71 -            case _ =>
    2.72 -              None
    2.73 -          }
    2.74 -        case _ =>
    2.75 -          None
    2.76 -      }
    2.77 -
    2.78 -    val LOG = "simp_trace_log"
    2.79 -    val STEP = "simp_trace_step"
    2.80 -    val RECURSE = "simp_trace_recurse"
    2.81 -    val HINT = "simp_trace_hint"
    2.82 -    val IGNORE = "simp_trace_ignore"
    2.83 -
    2.84 -    case class Data(serial: Long, markup: String, text: String,
    2.85 -                    parent: Long, props: Properties.T, content: XML.Body)
    2.86 -    {
    2.87 -      def memory: Boolean =
    2.88 -        Memory.unapply(props) getOrElse true
    2.89 -    }
    2.90 -
    2.91 -  }
    2.92 -
    2.93  }
    2.94  
    2.95  
     3.1 --- a/src/Pure/Tools/simplifier_trace.ML	Tue Feb 18 17:26:13 2014 +0100
     3.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Tue Feb 18 18:29:02 2014 +0100
     3.3 @@ -146,14 +146,6 @@
     3.4  val memoryN = "memory"
     3.5  val successN = "success"
     3.6  
     3.7 -val logN = "simp_trace_log"
     3.8 -val stepN = "simp_trace_step"
     3.9 -val recurseN = "simp_trace_recurse"
    3.10 -val hintN = "simp_trace_hint"
    3.11 -val ignoreN = "simp_trace_ignore"
    3.12 -
    3.13 -val cancelN = "simp_trace_cancel"
    3.14 -
    3.15  type payload =
    3.16    {props: Properties.T,
    3.17     pretty: Pretty.T}
    3.18 @@ -171,7 +163,10 @@
    3.19        | Normal => triggered
    3.20        | Full => true)
    3.21  
    3.22 -    val markup' = if markup = stepN andalso not interactive then logN else markup
    3.23 +    val markup' =
    3.24 +      if markup = Markup.simp_trace_stepN andalso not interactive
    3.25 +      then Markup.simp_trace_logN
    3.26 +      else markup
    3.27    in
    3.28      if not eligible orelse depth > max_depth then NONE
    3.29      else
    3.30 @@ -195,10 +190,7 @@
    3.31  fun send_request (result_id, content) =
    3.32    let
    3.33      fun break () =
    3.34 -      (Output.protocol_message
    3.35 -         [(Markup.functionN, cancelN),
    3.36 -          (serialN, Markup.print_int result_id)]
    3.37 -         "";
    3.38 +      (Output.protocol_message (Markup.simp_trace_cancel result_id) "";
    3.39         Synchronized.change futures (Inttab.delete_safe result_id))
    3.40      val promise = Future.promise break : string future
    3.41    in
    3.42 @@ -279,7 +271,8 @@
    3.43        end
    3.44  
    3.45    in
    3.46 -    (case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
    3.47 +    (case mk_generic_result Markup.simp_trace_stepN text
    3.48 +        (thm_triggered orelse term_triggered) payload ctxt of
    3.49        NONE => Future.value (SOME ctxt)
    3.50      | SOME res => mk_promise res)
    3.51    end
    3.52 @@ -303,7 +296,7 @@
    3.53         breakpoints = breakpoints} (Context.Proof ctxt)
    3.54  
    3.55      val context' =
    3.56 -      (case mk_generic_result recurseN text true payload ctxt of
    3.57 +      (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
    3.58          NONE => put 0
    3.59        | SOME res => (output_result res; put (#1 res)))
    3.60    in Context.the_proof context' end
    3.61 @@ -342,7 +335,7 @@
    3.62          fun to_response "exit" = false
    3.63            | to_response "redo" =
    3.64                (Option.app output_result
    3.65 -                (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
    3.66 +                (mk_generic_result Markup.simp_trace_ignoreN "Ignore" true empty_payload ctxt');
    3.67                 true)
    3.68            | to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message"
    3.69        in
    3.70 @@ -351,7 +344,7 @@
    3.71          else Future.map to_response (send_request result)
    3.72        end
    3.73    in
    3.74 -    (case mk_generic_result hintN "Step failed" true payload ctxt' of
    3.75 +    (case mk_generic_result Markup.simp_trace_hintN "Step failed" true payload ctxt' of
    3.76        NONE => Future.value false
    3.77      | SOME res => mk_promise res)
    3.78    end
    3.79 @@ -362,7 +355,8 @@
    3.80        {props = [(successN, "true")],
    3.81         pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)}
    3.82    in
    3.83 -    Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt)
    3.84 +    Option.app output_result
    3.85 +      (mk_generic_result Markup.simp_trace_hintN "Successfully rewrote" true payload ctxt)
    3.86    end
    3.87  
    3.88  
    3.89 @@ -400,7 +394,7 @@
    3.90       trace_apply = simp_apply})
    3.91  
    3.92  val _ =
    3.93 -  Isabelle_Process.protocol_command "Document.simp_trace_reply"
    3.94 +  Isabelle_Process.protocol_command "Simplifier_Trace.reply"
    3.95      (fn [s, r] =>
    3.96        let
    3.97          val serial = Markup.parse_int s
     4.1 --- a/src/Pure/Tools/simplifier_trace.scala	Tue Feb 18 17:26:13 2014 +0100
     4.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Tue Feb 18 18:29:02 2014 +0100
     4.3 @@ -6,6 +6,7 @@
     4.4  
     4.5  package isabelle
     4.6  
     4.7 +
     4.8  import scala.actors.Actor._
     4.9  import scala.annotation.tailrec
    4.10  import scala.collection.immutable.SortedMap
    4.11 @@ -13,8 +14,42 @@
    4.12  
    4.13  object Simplifier_Trace
    4.14  {
    4.15 +  /* trace items from the prover */
    4.16  
    4.17 -  import Markup.Simp_Trace_Item
    4.18 +  val TEXT = "text"
    4.19 +  val Text = new Properties.String(TEXT)
    4.20 +
    4.21 +  val PARENT = "parent"
    4.22 +  val Parent = new Properties.Long(PARENT)
    4.23 +
    4.24 +  val SUCCESS = "success"
    4.25 +  val Success = new Properties.Boolean(SUCCESS)
    4.26 +
    4.27 +  val MEMORY = "memory"
    4.28 +  val Memory = new Properties.Boolean(MEMORY)
    4.29 +
    4.30 +  object Item
    4.31 +  {
    4.32 +    case class Data(
    4.33 +      serial: Long, markup: String, text: String,
    4.34 +      parent: Long, props: Properties.T, content: XML.Body)
    4.35 +    {
    4.36 +      def memory: Boolean = Memory.unapply(props) getOrElse true
    4.37 +    }
    4.38 +
    4.39 +    def unapply(tree: XML.Tree): Option[(String, Data)] =
    4.40 +      tree match {
    4.41 +        case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)),
    4.42 +          List(XML.Elem(Markup(markup, props), content)))
    4.43 +        if markup.startsWith("simp_trace_") =>  // FIXME proper comparison of string constants
    4.44 +          (props, props) match {
    4.45 +            case (Text(text), Parent(parent)) =>
    4.46 +              Some((markup, Data(serial, markup, text, parent, props, content)))
    4.47 +            case _ => None
    4.48 +          }
    4.49 +        case _ => None
    4.50 +      }
    4.51 +  }
    4.52  
    4.53  
    4.54    /* replies to the prover */
    4.55 @@ -23,7 +58,6 @@
    4.56  
    4.57    object Answer
    4.58    {
    4.59 -
    4.60      object step
    4.61      {
    4.62        val skip = Answer("skip", "Skip")
    4.63 @@ -44,11 +78,24 @@
    4.64        val default = exit
    4.65        val all = List(redo, exit)
    4.66      }
    4.67 -
    4.68    }
    4.69  
    4.70    val all_answers = Answer.step.all ++ Answer.hint_fail.all
    4.71  
    4.72 +  object Active
    4.73 +  {
    4.74 +    def unapply(tree: XML.Tree): Option[(Long, Answer)] =
    4.75 +      tree match {
    4.76 +        case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
    4.77 +          (props, props) match {
    4.78 +            case (Markup.Serial(serial), Markup.Name(name)) =>
    4.79 +              all_answers.find(_.name == name).map((serial, _))
    4.80 +            case _ => None
    4.81 +          }
    4.82 +        case _ => None
    4.83 +      }
    4.84 +  }
    4.85 +
    4.86  
    4.87    /* GUI interaction */
    4.88  
    4.89 @@ -64,7 +111,7 @@
    4.90    private object Stop
    4.91    case class Reply(session: Session, serial: Long, answer: Answer)
    4.92  
    4.93 -  case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer)
    4.94 +  case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
    4.95  
    4.96    case class Context(
    4.97      last_serial: Long = 0L,
    4.98 @@ -83,13 +130,13 @@
    4.99  
   4.100    }
   4.101  
   4.102 -  case class Trace(entries: List[Simp_Trace_Item.Data])
   4.103 +  case class Trace(entries: List[Item.Data])
   4.104  
   4.105    case class Index(text: String, content: XML.Body)
   4.106  
   4.107    object Index
   4.108    {
   4.109 -    def of_data(data: Simp_Trace_Item.Data): Index =
   4.110 +    def of_data(data: Item.Data): Index =
   4.111        Index(data.text, data.content)
   4.112    }
   4.113  
   4.114 @@ -128,7 +175,7 @@
   4.115  
   4.116      def do_reply(session: Session, serial: Long, answer: Answer)
   4.117      {
   4.118 -      session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name)
   4.119 +      session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
   4.120      }
   4.121  
   4.122      loop {
   4.123 @@ -140,14 +187,12 @@
   4.124            for ((serial, result) <- results.entries if serial > new_context.last_serial)
   4.125            {
   4.126              result match {
   4.127 -              case Simp_Trace_Item(markup, data) =>
   4.128 -                import Simp_Trace_Item._
   4.129 -
   4.130 +              case Item(markup, data) =>
   4.131                  memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
   4.132  
   4.133                  markup match {
   4.134  
   4.135 -                  case STEP =>
   4.136 +                  case Markup.SIMP_TRACE_STEP =>
   4.137                      val index = Index.of_data(data)
   4.138                      memory.get(index) match {
   4.139                        case Some(answer) if data.memory =>
   4.140 @@ -156,11 +201,11 @@
   4.141                          new_context += Question(data, Answer.step.all, Answer.step.default)
   4.142                      }
   4.143  
   4.144 -                  case HINT =>
   4.145 +                  case Markup.SIMP_TRACE_HINT =>
   4.146                      data.props match {
   4.147 -                      case Markup.Success(false) =>
   4.148 +                      case Success(false) =>
   4.149                          results.get(data.parent) match {
   4.150 -                          case Some(Simp_Trace_Item(STEP, _)) =>
   4.151 +                          case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
   4.152                              new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
   4.153                            case _ =>
   4.154                              // unknown, better send a default reply
   4.155 @@ -169,7 +214,7 @@
   4.156                        case _ =>
   4.157                      }
   4.158  
   4.159 -                  case IGNORE =>
   4.160 +                  case Markup.SIMP_TRACE_IGNORE =>
   4.161                      // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
   4.162                      // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
   4.163                      // to selectively purge the replies which have been memorized, going down from
   4.164 @@ -179,7 +224,7 @@
   4.165                      def purge(queue: Vector[Long]): Unit =
   4.166                        queue match {
   4.167                          case s +: rest =>
   4.168 -                          for (Simp_Trace_Item(STEP, data) <- results.get(s))
   4.169 +                          for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
   4.170                              memory -= Index.of_data(data)
   4.171                            val children = memory_children.getOrElse(s, Set.empty)
   4.172                            memory_children -= s
   4.173 @@ -208,7 +253,7 @@
   4.174            // current results.
   4.175  
   4.176            val items =
   4.177 -            for { (_, Simp_Trace_Item(_, data)) <- results.entries }
   4.178 +            for { (_, Item(_, data)) <- results.entries }
   4.179                yield data
   4.180  
   4.181            reply(Trace(items.toList))
   4.182 @@ -232,7 +277,7 @@
   4.183          case Reply(session, serial, answer) =>
   4.184            find_question(serial) match {
   4.185              case Some((id, Question(data, _, _))) =>
   4.186 -              if (data.markup == Markup.Simp_Trace_Item.STEP && data.memory)
   4.187 +              if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
   4.188                {
   4.189                  val index = Index.of_data(data)
   4.190                  memory += (index -> answer)
   4.191 @@ -256,10 +301,9 @@
   4.192  
   4.193    class Handler extends Session.Protocol_Handler
   4.194    {
   4.195 -    private def cancel(
   4.196 -      prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
   4.197 +    private def cancel(prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
   4.198        msg.properties match {
   4.199 -        case Markup.Cancel_Simp_Trace(serial) =>
   4.200 +        case Markup.Simp_Trace_Cancel(serial) =>
   4.201            manager ! Cancel(serial)
   4.202            true
   4.203          case _ =>
   4.204 @@ -272,8 +316,6 @@
   4.205        manager ! Stop
   4.206      }
   4.207  
   4.208 -    val functions = Map(
   4.209 -      Markup.CANCEL_SIMP_TRACE -> cancel _)
   4.210 +    val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)
   4.211    }
   4.212 -
   4.213  }
     5.1 --- a/src/Tools/jEdit/src/active.scala	Tue Feb 18 17:26:13 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/active.scala	Tue Feb 18 18:29:02 2014 +0100
     5.3 @@ -61,7 +61,7 @@
     5.4                      else text_area.setSelectedText(text)
     5.5                  }
     5.6  
     5.7 -              case Markup.Simp_Trace(serial, answer) =>
     5.8 +              case Simplifier_Trace.Active(serial, answer) =>
     5.9                  Simplifier_Trace.send_reply(PIDE.session, serial, answer)
    5.10  
    5.11                case Protocol.Dialog(id, serial, result) =>
     6.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Feb 18 17:26:13 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Feb 18 18:29:02 2014 +0100
     6.3 @@ -10,12 +10,9 @@
     6.4  import isabelle._
     6.5  
     6.6  import scala.annotation.tailrec
     6.7 -
     6.8  import scala.collection.immutable.SortedMap
     6.9 -
    6.10  import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
    6.11  import scala.swing.event.{Key, KeyPressed}
    6.12 -
    6.13  import scala.util.matching.Regex
    6.14  
    6.15  import java.awt.BorderLayout
    6.16 @@ -25,17 +22,15 @@
    6.17  
    6.18  import org.gjt.sp.jedit.View
    6.19  
    6.20 +
    6.21  private object Simplifier_Trace_Window
    6.22  {
    6.23 -
    6.24 -  import Markup.Simp_Trace_Item
    6.25 -
    6.26    sealed trait Trace_Tree
    6.27    {
    6.28      var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
    6.29      val serial: Long
    6.30      val parent: Option[Trace_Tree]
    6.31 -    var hints: List[Simp_Trace_Item.Data]
    6.32 +    var hints: List[Simplifier_Trace.Item.Data]
    6.33      def set_interesting(): Unit
    6.34    }
    6.35  
    6.36 @@ -43,17 +38,19 @@
    6.37    {
    6.38      val parent = None
    6.39      val hints = Nil
    6.40 -    def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
    6.41 +    def hints_=(xs: List[Simplifier_Trace.Item.Data]) =
    6.42 +      throw new IllegalStateException("Root_Tree.hints")
    6.43      def set_interesting() = ()
    6.44  
    6.45      def format(regex: Option[Regex]): XML.Body =
    6.46        Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
    6.47    }
    6.48  
    6.49 -  final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree
    6.50 +  final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
    6.51 +    extends Trace_Tree
    6.52    {
    6.53      val serial = data.serial
    6.54 -    var hints = List.empty[Simp_Trace_Item.Data]
    6.55 +    var hints = List.empty[Simplifier_Trace.Item.Data]
    6.56      var interesting: Boolean = false
    6.57  
    6.58      def set_interesting(): Unit =
    6.59 @@ -76,7 +73,7 @@
    6.60            Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
    6.61        }
    6.62  
    6.63 -      def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
    6.64 +      def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
    6.65          Pretty.block(Pretty.separate(
    6.66            XML.Text(data.text) ::
    6.67            data.content
    6.68 @@ -111,19 +108,19 @@
    6.69    }
    6.70  
    6.71    @tailrec
    6.72 -  def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
    6.73 +  def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
    6.74      rest match {
    6.75        case Nil =>
    6.76          ()
    6.77        case head :: tail =>
    6.78          lookup.get(head.parent) match {
    6.79            case Some(parent) =>
    6.80 -            if (head.markup == Simp_Trace_Item.HINT)
    6.81 +            if (head.markup == Markup.SIMP_TRACE_HINT)
    6.82              {
    6.83                parent.hints ::= head
    6.84                walk_trace(tail, lookup)
    6.85              }
    6.86 -            else if (head.markup == Simp_Trace_Item.IGNORE)
    6.87 +            else if (head.markup == Markup.SIMP_TRACE_IGNORE)
    6.88              {
    6.89                parent.parent match {
    6.90                  case None =>
    6.91 @@ -137,7 +134,7 @@
    6.92              {
    6.93                val entry = new Elem_Tree(head, Some(parent))
    6.94                parent.children += ((head.serial, entry))
    6.95 -              if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG)
    6.96 +              if (head.markup == Markup.SIMP_TRACE_STEP || head.markup == Markup.SIMP_TRACE_LOG)
    6.97                  entry.set_interesting()
    6.98                walk_trace(tail, lookup + (head.serial -> entry))
    6.99              }