# HG changeset patch
# User wenzelm
# Date 1392744542 -3600
# Node ID 99409ccbe04ab10143e2e95e4809a930c86cfb3b
# Parent  e4907b74a3475153c6a030609ae85e1820745eb8
more standard names for protocol and markup elements;

diff -r e4907b74a347 -r 99409ccbe04a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 18 18:29:02 2014 +0100
@@ -164,6 +164,12 @@
   val command_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
+  val simp_trace_logN: string
+  val simp_trace_stepN: string
+  val simp_trace_recurseN: string
+  val simp_trace_hintN: string
+  val simp_trace_ignoreN: string
+  val simp_trace_cancel: serial -> Properties.T
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -516,6 +522,16 @@
   | dest_loading_theory _ = NONE;
 
 
+(* simplifier trace *)
+
+val simp_trace_logN = "simp_trace_log";
+val simp_trace_stepN = "simp_trace_step";
+val simp_trace_recurseN = "simp_trace_recurse";
+val simp_trace_hintN = "simp_trace_hint";
+val simp_trace_ignoreN = "simp_trace_ignore";
+
+fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)];
+
 
 (** print mode operations **)
 
diff -r e4907b74a347 -r 99409ccbe04a 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
-    }
-
-  }
-
 }
 
 
diff -r e4907b74a347 -r 99409ccbe04a src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML	Tue Feb 18 18:29:02 2014 +0100
@@ -146,14 +146,6 @@
 val memoryN = "memory"
 val successN = "success"
 
-val logN = "simp_trace_log"
-val stepN = "simp_trace_step"
-val recurseN = "simp_trace_recurse"
-val hintN = "simp_trace_hint"
-val ignoreN = "simp_trace_ignore"
-
-val cancelN = "simp_trace_cancel"
-
 type payload =
   {props: Properties.T,
    pretty: Pretty.T}
@@ -171,7 +163,10 @@
       | Normal => triggered
       | Full => true)
 
-    val markup' = if markup = stepN andalso not interactive then logN else markup
+    val markup' =
+      if markup = Markup.simp_trace_stepN andalso not interactive
+      then Markup.simp_trace_logN
+      else markup
   in
     if not eligible orelse depth > max_depth then NONE
     else
@@ -195,10 +190,7 @@
 fun send_request (result_id, content) =
   let
     fun break () =
-      (Output.protocol_message
-         [(Markup.functionN, cancelN),
-          (serialN, Markup.print_int result_id)]
-         "";
+      (Output.protocol_message (Markup.simp_trace_cancel result_id) "";
        Synchronized.change futures (Inttab.delete_safe result_id))
     val promise = Future.promise break : string future
   in
@@ -279,7 +271,8 @@
       end
 
   in
-    (case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
+    (case mk_generic_result Markup.simp_trace_stepN text
+        (thm_triggered orelse term_triggered) payload ctxt of
       NONE => Future.value (SOME ctxt)
     | SOME res => mk_promise res)
   end
@@ -303,7 +296,7 @@
        breakpoints = breakpoints} (Context.Proof ctxt)
 
     val context' =
-      (case mk_generic_result recurseN text true payload ctxt of
+      (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
         NONE => put 0
       | SOME res => (output_result res; put (#1 res)))
   in Context.the_proof context' end
@@ -342,7 +335,7 @@
         fun to_response "exit" = false
           | to_response "redo" =
               (Option.app output_result
-                (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
+                (mk_generic_result Markup.simp_trace_ignoreN "Ignore" true empty_payload ctxt');
                true)
           | to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message"
       in
@@ -351,7 +344,7 @@
         else Future.map to_response (send_request result)
       end
   in
-    (case mk_generic_result hintN "Step failed" true payload ctxt' of
+    (case mk_generic_result Markup.simp_trace_hintN "Step failed" true payload ctxt' of
       NONE => Future.value false
     | SOME res => mk_promise res)
   end
@@ -362,7 +355,8 @@
       {props = [(successN, "true")],
        pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)}
   in
-    Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt)
+    Option.app output_result
+      (mk_generic_result Markup.simp_trace_hintN "Successfully rewrote" true payload ctxt)
   end
 
 
@@ -400,7 +394,7 @@
      trace_apply = simp_apply})
 
 val _ =
-  Isabelle_Process.protocol_command "Document.simp_trace_reply"
+  Isabelle_Process.protocol_command "Simplifier_Trace.reply"
     (fn [s, r] =>
       let
         val serial = Markup.parse_int s
diff -r e4907b74a347 -r 99409ccbe04a src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala	Tue Feb 18 18:29:02 2014 +0100
@@ -6,6 +6,7 @@
 
 package isabelle
 
+
 import scala.actors.Actor._
 import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
@@ -13,8 +14,42 @@
 
 object Simplifier_Trace
 {
+  /* trace items from the prover */
 
-  import Markup.Simp_Trace_Item
+  val TEXT = "text"
+  val Text = new Properties.String(TEXT)
+
+  val PARENT = "parent"
+  val Parent = new Properties.Long(PARENT)
+
+  val SUCCESS = "success"
+  val Success = new Properties.Boolean(SUCCESS)
+
+  val MEMORY = "memory"
+  val Memory = new Properties.Boolean(MEMORY)
+
+  object Item
+  {
+    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
+    }
+
+    def unapply(tree: XML.Tree): Option[(String, Data)] =
+      tree match {
+        case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)),
+          List(XML.Elem(Markup(markup, props), content)))
+        if markup.startsWith("simp_trace_") =>  // FIXME proper comparison of string constants
+          (props, props) match {
+            case (Text(text), Parent(parent)) =>
+              Some((markup, Data(serial, markup, text, parent, props, content)))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
 
 
   /* replies to the prover */
@@ -23,7 +58,6 @@
 
   object Answer
   {
-
     object step
     {
       val skip = Answer("skip", "Skip")
@@ -44,11 +78,24 @@
       val default = exit
       val all = List(redo, exit)
     }
-
   }
 
   val all_answers = Answer.step.all ++ Answer.hint_fail.all
 
+  object Active
+  {
+    def unapply(tree: XML.Tree): Option[(Long, Answer)] =
+      tree match {
+        case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
+          (props, props) match {
+            case (Markup.Serial(serial), Markup.Name(name)) =>
+              all_answers.find(_.name == name).map((serial, _))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
 
   /* GUI interaction */
 
@@ -64,7 +111,7 @@
   private object Stop
   case class Reply(session: Session, serial: Long, answer: Answer)
 
-  case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer)
+  case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
 
   case class Context(
     last_serial: Long = 0L,
@@ -83,13 +130,13 @@
 
   }
 
-  case class Trace(entries: List[Simp_Trace_Item.Data])
+  case class Trace(entries: List[Item.Data])
 
   case class Index(text: String, content: XML.Body)
 
   object Index
   {
-    def of_data(data: Simp_Trace_Item.Data): Index =
+    def of_data(data: Item.Data): Index =
       Index(data.text, data.content)
   }
 
@@ -128,7 +175,7 @@
 
     def do_reply(session: Session, serial: Long, answer: Answer)
     {
-      session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name)
+      session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
     }
 
     loop {
@@ -140,14 +187,12 @@
           for ((serial, result) <- results.entries if serial > new_context.last_serial)
           {
             result match {
-              case Simp_Trace_Item(markup, data) =>
-                import Simp_Trace_Item._
-
+              case Item(markup, data) =>
                 memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
 
                 markup match {
 
-                  case STEP =>
+                  case Markup.SIMP_TRACE_STEP =>
                     val index = Index.of_data(data)
                     memory.get(index) match {
                       case Some(answer) if data.memory =>
@@ -156,11 +201,11 @@
                         new_context += Question(data, Answer.step.all, Answer.step.default)
                     }
 
-                  case HINT =>
+                  case Markup.SIMP_TRACE_HINT =>
                     data.props match {
-                      case Markup.Success(false) =>
+                      case Success(false) =>
                         results.get(data.parent) match {
-                          case Some(Simp_Trace_Item(STEP, _)) =>
+                          case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
                             new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
                           case _ =>
                             // unknown, better send a default reply
@@ -169,7 +214,7 @@
                       case _ =>
                     }
 
-                  case IGNORE =>
+                  case Markup.SIMP_TRACE_IGNORE =>
                     // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
                     // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
                     // to selectively purge the replies which have been memorized, going down from
@@ -179,7 +224,7 @@
                     def purge(queue: Vector[Long]): Unit =
                       queue match {
                         case s +: rest =>
-                          for (Simp_Trace_Item(STEP, data) <- results.get(s))
+                          for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
                             memory -= Index.of_data(data)
                           val children = memory_children.getOrElse(s, Set.empty)
                           memory_children -= s
@@ -208,7 +253,7 @@
           // current results.
 
           val items =
-            for { (_, Simp_Trace_Item(_, data)) <- results.entries }
+            for { (_, Item(_, data)) <- results.entries }
               yield data
 
           reply(Trace(items.toList))
@@ -232,7 +277,7 @@
         case Reply(session, serial, answer) =>
           find_question(serial) match {
             case Some((id, Question(data, _, _))) =>
-              if (data.markup == Markup.Simp_Trace_Item.STEP && data.memory)
+              if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
               {
                 val index = Index.of_data(data)
                 memory += (index -> answer)
@@ -256,10 +301,9 @@
 
   class Handler extends Session.Protocol_Handler
   {
-    private def cancel(
-      prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
+    private def cancel(prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
       msg.properties match {
-        case Markup.Cancel_Simp_Trace(serial) =>
+        case Markup.Simp_Trace_Cancel(serial) =>
           manager ! Cancel(serial)
           true
         case _ =>
@@ -272,8 +316,6 @@
       manager ! Stop
     }
 
-    val functions = Map(
-      Markup.CANCEL_SIMP_TRACE -> cancel _)
+    val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)
   }
-
 }
diff -r e4907b74a347 -r 99409ccbe04a src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Tools/jEdit/src/active.scala	Tue Feb 18 18:29:02 2014 +0100
@@ -61,7 +61,7 @@
                     else text_area.setSelectedText(text)
                 }
 
-              case Markup.Simp_Trace(serial, answer) =>
+              case Simplifier_Trace.Active(serial, answer) =>
                 Simplifier_Trace.send_reply(PIDE.session, serial, answer)
 
               case Protocol.Dialog(id, serial, result) =>
diff -r e4907b74a347 -r 99409ccbe04a src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Feb 18 18:29:02 2014 +0100
@@ -10,12 +10,9 @@
 import isabelle._
 
 import scala.annotation.tailrec
-
 import scala.collection.immutable.SortedMap
-
 import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
 import scala.swing.event.{Key, KeyPressed}
-
 import scala.util.matching.Regex
 
 import java.awt.BorderLayout
@@ -25,17 +22,15 @@
 
 import org.gjt.sp.jedit.View
 
+
 private object Simplifier_Trace_Window
 {
-
-  import Markup.Simp_Trace_Item
-
   sealed trait Trace_Tree
   {
     var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
     val serial: Long
     val parent: Option[Trace_Tree]
-    var hints: List[Simp_Trace_Item.Data]
+    var hints: List[Simplifier_Trace.Item.Data]
     def set_interesting(): Unit
   }
 
@@ -43,17 +38,19 @@
   {
     val parent = None
     val hints = Nil
-    def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
+    def hints_=(xs: List[Simplifier_Trace.Item.Data]) =
+      throw new IllegalStateException("Root_Tree.hints")
     def set_interesting() = ()
 
     def format(regex: Option[Regex]): XML.Body =
       Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
   }
 
-  final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree
+  final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
+    extends Trace_Tree
   {
     val serial = data.serial
-    var hints = List.empty[Simp_Trace_Item.Data]
+    var hints = List.empty[Simplifier_Trace.Item.Data]
     var interesting: Boolean = false
 
     def set_interesting(): Unit =
@@ -76,7 +73,7 @@
           Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
       }
 
-      def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
+      def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
         Pretty.block(Pretty.separate(
           XML.Text(data.text) ::
           data.content
@@ -111,19 +108,19 @@
   }
 
   @tailrec
-  def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
+  def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
     rest match {
       case Nil =>
         ()
       case head :: tail =>
         lookup.get(head.parent) match {
           case Some(parent) =>
-            if (head.markup == Simp_Trace_Item.HINT)
+            if (head.markup == Markup.SIMP_TRACE_HINT)
             {
               parent.hints ::= head
               walk_trace(tail, lookup)
             }
-            else if (head.markup == Simp_Trace_Item.IGNORE)
+            else if (head.markup == Markup.SIMP_TRACE_IGNORE)
             {
               parent.parent match {
                 case None =>
@@ -137,7 +134,7 @@
             {
               val entry = new Elem_Tree(head, Some(parent))
               parent.children += ((head.serial, entry))
-              if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG)
+              if (head.markup == Markup.SIMP_TRACE_STEP || head.markup == Markup.SIMP_TRACE_LOG)
                 entry.set_interesting()
               walk_trace(tail, lookup + (head.serial -> entry))
             }