# HG changeset patch
# User wenzelm
# Date 1202672985 -3600
# Node ID 43bcb30a6d9736e66f89d5663967c331200b01ad
# Parent  88bb26089ef56cd1b499c6606a30bfa52522a2ac
added position_properties;

diff -r 88bb26089ef5 -r 43bcb30a6d97 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Feb 10 20:49:42 2008 +0100
+++ b/src/Pure/General/markup.ML	Sun Feb 10 20:49:45 2008 +0100
@@ -22,6 +22,7 @@
   val lineN: string
   val columnN: string
   val fileN: string
+  val position_properties: string list
   val positionN: string val position: T
   val indentN: string
   val blockN: string val block: int -> T
@@ -109,6 +110,7 @@
 val fileN = "file";
 val idN = "id";
 
+val position_properties = [lineN, columnN, fileN, idN];
 val (positionN, position) = markup_elem "position";