--- a/src/Pure/General/markup.ML Tue Mar 11 20:30:46 2008 +0100
+++ b/src/Pure/General/markup.ML Tue Mar 11 22:31:07 2008 +0100
@@ -24,6 +24,7 @@
val fileN: string
val position_properties: string list
val positionN: string val position: T
+ val locationN: string val location: T
val indentN: string
val blockN: string val block: int -> T
val widthN: string
@@ -113,6 +114,8 @@
val position_properties = [lineN, columnN, fileN, idN];
val (positionN, position) = markup_elem "position";
+val (locationN, location) = markup_elem "location";
+
(* pretty printing *)