src/Pure/PIDE/markup.scala
changeset 69557 e72360fef69a
parent 69320 fc221fa79741
child 69648 97ddaec3e2ae
--- a/src/Pure/PIDE/markup.scala	Mon Dec 31 12:02:31 2018 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Dec 31 13:07:24 2018 +0100
@@ -115,6 +115,8 @@
   val COMPLETION = "completion"
   val NO_COMPLETION = "no_completion"
 
+  val UPDATE = "update"
+
 
   /* position */