src/Pure/PIDE/markup.scala
changeset 52800 1baa5d19ac44
parent 52697 6fb98a20c349
child 52854 92932931bd82
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Jul 30 19:53:06 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Jul 30 21:22:37 2013 +0200
     1.3 @@ -315,6 +315,8 @@
     1.4    val FUNCTION = "function"
     1.5    val Function = new Properties.String(FUNCTION)
     1.6  
     1.7 +  val Flush: Properties.T = List((FUNCTION, "flush"))
     1.8 +
     1.9    val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
    1.10    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
    1.11