src/Pure/PIDE/markup.scala
changeset 56733 f7700146678d
parent 56623 4675df68450e
child 56743 81370dfadb1d
--- a/src/Pure/PIDE/markup.scala	Fri Apr 25 23:29:54 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Apr 25 23:42:25 2014 +0200
@@ -365,8 +365,6 @@
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)
 
-  val Flush: Properties.T = List((FUNCTION, "flush"))
-
   val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))