src/Pure/General/markup.scala

--- 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"