--- 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"))