author | wenzelm |
Mon, 29 Dec 2008 22:43:41 +0100 | |
changeset 29205 | 7dc7a75033ea |
parent 29204 | e002f7b63e3c |
child 29252 | ea97aa6aeba2 |
--- a/src/Pure/General/markup.scala Mon Dec 29 22:36:56 2008 +0100 +++ b/src/Pure/General/markup.scala Mon Dec 29 22:43:41 2008 +0100 @@ -25,6 +25,8 @@ val FILE = "file" val ID = "id" + val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID) + val POSITION = "position" val LOCATION = "location"