--- a/src/Pure/PIDE/markup.ML Tue Jul 30 19:53:06 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Tue Jul 30 21:22:37 2013 +0200
@@ -142,6 +142,7 @@
val padding_command: Properties.entry
val dialogN: string val dialog: serial -> string -> T
val functionN: string
+ val flush: Properties.T
val assign_update: Properties.T
val removed_versions: Properties.T
val protocol_handler: string -> Properties.T
@@ -463,6 +464,8 @@
val functionN = "function"
+val flush = [(functionN, "flush")];
+
val assign_update = [(functionN, "assign_update")];
val removed_versions = [(functionN, "removed_versions")];