--- a/src/Pure/PIDE/markup.ML Sun Feb 23 20:24:33 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Sun Feb 23 21:11:59 2014 +0100
@@ -37,8 +37,7 @@
val get_entity_kind: T -> string option
val defN: string
val refN: string
- val totalN: string
- val completionN: string
+ val completionN: string val completion: T
val lineN: string
val offsetN: string
val end_offsetN: string
@@ -287,8 +286,7 @@
(* completion *)
-val totalN = "total";
-val completionN = "completion";
+val (completionN, completion) = markup_elem "completion";
(* position *)