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"))