--- a/src/Pure/PIDE/markup.scala Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Nov 11 18:16:25 2014 +0100
@@ -100,6 +100,7 @@
/* position */
val LINE = "line"
+ val END_LINE = "line"
val OFFSET = "offset"
val END_OFFSET = "end_offset"
val FILE = "file"