# HG changeset patch
# User wenzelm
# Date 1367243262 -7200
# Node ID 517f232e867d4f01870a20c57bcdc266e925327c
# Parent  6b82042690b5de671f851782519ed97fcd3599f0
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";

diff -r 6b82042690b5 -r 517f232e867d src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Apr 29 14:07:03 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Apr 29 15:47:42 2013 +0200
@@ -218,18 +218,7 @@
 
   /* command timing */
 
-  object Command_Timing
-  {
-    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
-      props match {
-        case (FUNCTION, "command_timing") :: args =>
-          (args, args) match {
-            case (Position.Id(id), Timing_Properties(timing)) => Some((id, timing))
-            case _ => None
-          }
-        case _ => None
-      }
-  }
+  val COMMAND_TIMING = "command_timing"
 
 
   /* toplevel */
diff -r 6b82042690b5 -r 517f232e867d src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Apr 29 14:07:03 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Apr 29 15:47:42 2013 +0200
@@ -84,6 +84,22 @@
     (Status.init /: markups)(command_status(_, _))
 
 
+  /* command timing */
+
+  object Command_Timing
+  {
+    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
+      props match {
+        case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
+          (args, args) match {
+            case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
+
   /* node status */
 
   sealed case class Node_Status(
diff -r 6b82042690b5 -r 517f232e867d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Apr 29 14:07:03 2013 +0200
+++ b/src/Pure/System/session.scala	Mon Apr 29 15:47:42 2013 +0200
@@ -322,7 +322,7 @@
         case Position.Id(state_id) if !output.is_protocol =>
           accumulate(state_id, output.message)
 
-        case Markup.Command_Timing(state_id, timing) if output.is_protocol =>
+        case Protocol.Command_Timing(state_id, timing) if output.is_protocol =>
           val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
           accumulate(state_id, prover.get.xml_cache.elem(message))