# HG changeset patch
# User wenzelm
# Date 1509379562 -3600
# Node ID 91a21a5631ae1705c6401d0a2cdb47a32e046f51
# Parent  c78ff0aeba4c2bdbc72c24f4e39b59f728006b64
proper order of initialization (amending 9953ae603a23);

diff -r c78ff0aeba4c -r 91a21a5631ae src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Oct 30 13:18:44 2017 +0000
+++ b/src/Pure/PIDE/markup.scala	Mon Oct 30 17:06:02 2017 +0100
@@ -392,13 +392,6 @@
   }
 
 
-  /* protocol functions */
-
-  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
-
-  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
-
-
   /* command indentation */
 
   object Command_Indent
@@ -506,6 +499,9 @@
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)
 
+  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
+  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
+
   val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))