# HG changeset patch
# User wenzelm
# Date 1230587021 -3600
# Node ID 7dc7a75033ea53c879f5c3e26709d974f4e92ba8
# Parent  e002f7b63e3cc288958d1f8e8e33b786b4f8fcf1
added POSITION_PROPERTIES;

diff -r e002f7b63e3c -r 7dc7a75033ea 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"