src/Pure/General/markup.scala
changeset 41483 4a8431c73cf2
parent 40848 8662b9b1f123
child 42136 826168ae0213
--- 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"