--- a/src/Pure/PIDE/markup.ML Mon Dec 31 12:02:31 2018 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Dec 31 13:07:24 2018 +0100
@@ -45,6 +45,7 @@
val refN: string
val completionN: string val completion: T
val no_completionN: string val no_completion: T
+ val updateN: string val update: T
val lineN: string
val end_lineN: string
val offsetN: string
@@ -336,6 +337,8 @@
val (completionN, completion) = markup_elem "completion";
val (no_completionN, no_completion) = markup_elem "no_completion";
+val (updateN, update) = markup_elem "update";
+
(* position *)