src/Pure/General/markup.ML

   val lineN: string
   val columnN: string
   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
   val breakN: string val break: int -> T
   val fbreakN: string val fbreak: T

 val idN = "id";
 
 val position_properties = [lineN, columnN, fileN, idN];
 val (positionN, position) = markup_elem "position";
 
+val (locationN, location) = markup_elem "location";
+
 
 (* pretty printing *)
 
 val indentN = "indent";
 val (blockN, block) = markup_int "block" indentN;