src/Pure/General/markup.scala
changeset 43710 7270ae921cf2
parent 43673 29eb1cd29961
child 43721 fad8634cee62
     1.1 --- a/src/Pure/General/markup.scala	Fri Jul 08 16:13:34 2011 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Fri Jul 08 17:04:38 2011 +0200
     1.3 @@ -114,20 +114,18 @@
     1.4    /* position */
     1.5  
     1.6    val LINE = "line"
     1.7 -  val COLUMN = "column"
     1.8    val OFFSET = "offset"
     1.9    val END_OFFSET = "end_offset"
    1.10    val FILE = "file"
    1.11    val ID = "id"
    1.12  
    1.13    val DEF_LINE = "def_line"
    1.14 -  val DEF_COLUMN = "def_column"
    1.15    val DEF_OFFSET = "def_offset"
    1.16    val DEF_END_OFFSET = "def_end_offset"
    1.17    val DEF_FILE = "def_file"
    1.18    val DEF_ID = "def_id"
    1.19  
    1.20 -  val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
    1.21 +  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
    1.22    val POSITION = "position"
    1.23  
    1.24