diff -r f4c07fdd1d48 -r 4a8431c73cf2 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Jan 09 13:58:31 2011 +0100
+++ b/src/Pure/General/markup.scala	Sun Jan 09 16:03:56 2011 +0100
@@ -100,14 +100,11 @@
   val LINE = "line"
   val COLUMN = "column"
   val OFFSET = "offset"
-  val END_LINE = "end_line"
-  val END_COLUMN = "end_column"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
-  val POSITION_PROPERTIES =
-    Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
+  val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
 
   val POSITION = "position"