src/Pure/General/markup.scala
changeset 43710 7270ae921cf2
parent 43673 29eb1cd29961
child 43721 fad8634cee62
--- a/src/Pure/General/markup.scala	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/Pure/General/markup.scala	Fri Jul 08 17:04:38 2011 +0200
@@ -114,20 +114,18 @@
   /* position */
 
   val LINE = "line"
-  val COLUMN = "column"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
-  val DEF_COLUMN = "def_column"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
-  val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
+  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   val POSITION = "position"