--- a/src/Pure/PIDE/markup.ML Fri Apr 25 23:29:54 2014 +0200
+++ b/src/Pure/PIDE/markup.ML Fri Apr 25 23:42:25 2014 +0200
@@ -172,7 +172,6 @@
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
@@ -557,8 +556,6 @@
val functionN = "function"
-val flush = [(functionN, "flush")];
-
val assign_update = [(functionN, "assign_update")];
val removed_versions = [(functionN, "removed_versions")];