# HG changeset patch
# User wenzelm
# Date 1205271067 -3600
# Node ID 2246d8bbe89da7a5b5bcfc84457bcde16a896b87
# Parent  3def1a1fea4ea7ad991edc9f4fd8e678beac56e4
added location;

diff -r 3def1a1fea4e -r 2246d8bbe89d src/Pure/General/markup.ML
--- 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 *)