--- a/src/Pure/PIDE/markup.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Nov 11 18:16:25 2014 +0100
@@ -47,6 +47,7 @@
val completionN: string val completion: T
val no_completionN: string val no_completion: T
val lineN: string
+ val end_lineN: string
val offsetN: string
val end_offsetN: string
val fileN: string
@@ -329,8 +330,11 @@
(* position *)
val lineN = "line";
+val end_lineN = "end_line";
+
val offsetN = "offset";
val end_offsetN = "end_offset";
+
val fileN = "file";
val idN = "id";