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