proper order of initialization (amending 9953ae603a23);
authorwenzelm
Mon, 30 Oct 2017 17:06:02 +0100
changeset 66942 91a21a5631ae
parent 66938 c78ff0aeba4c
child 66943 351aaaa9bacd
proper order of initialization (amending 9953ae603a23);
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"))