| changeset 52800 | 1baa5d19ac44 |
| parent 52697 | 6fb98a20c349 |
| child 52854 | 92932931bd82 |
--- a/src/Pure/PIDE/markup.scala Tue Jul 30 19:53:06 2013 +0200 +++ b/src/Pure/PIDE/markup.scala Tue Jul 30 21:22:37 2013 +0200 @@ -315,6 +315,8 @@ 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"))