1.1 --- a/src/Pure/PIDE/markup.scala	Mon Oct 30 13:18:44 2017 +0000
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Oct 30 17:06:02 2017 +0100
     1.3 @@ -392,13 +392,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* protocol functions */
     1.8 -
     1.9 -  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
    1.10 -
    1.11 -  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
    1.12 -
    1.13 -
    1.14    /* command indentation */
    1.15  
    1.16    object Command_Indent
    1.17 @@ -506,6 +499,9 @@
    1.18    val FUNCTION = "function"
    1.19    val Function = new Properties.String(FUNCTION)
    1.20  
    1.21 +  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
    1.22 +  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
    1.23 +
    1.24    val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
    1.25    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
    1.26