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