added POSITION_PROPERTIES;
authorwenzelm
Mon, 29 Dec 2008 22:43:41 +0100
changeset 29205 7dc7a75033ea
parent 29204 e002f7b63e3c
child 29252 ea97aa6aeba2
added POSITION_PROPERTIES;
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"