# 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 *)