# HG changeset patch
# User wenzelm
# Date 1218216539 -7200
# Node ID bdea6e17cbe3642dd1244db9f8413608daf84581
# Parent  29ad1d91a5a3e20bfe8a0377f380eb1876bb111c
added offset/end_offset;

diff -r 29ad1d91a5a3 -r bdea6e17cbe3 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Aug 08 16:54:33 2008 +0200
+++ b/src/Pure/General/markup.ML	Fri Aug 08 19:28:59 2008 +0200
@@ -22,8 +22,10 @@
   val property_internal: property
   val lineN: string
   val columnN: string
+  val offsetN: string
   val end_lineN: string
   val end_columnN: string
+  val end_offsetN: string
   val fileN: string
   val position_properties': string list
   val position_properties: string list
@@ -128,13 +130,15 @@
 
 val lineN = "line";
 val columnN = "column";
+val offsetN = "offset";
 val end_lineN = "end_line";
 val end_columnN = "end_column";
+val end_offsetN = "end_offset";
 val fileN = "file";
 val idN = "id";
 
-val position_properties' = [end_lineN, end_columnN, fileN, idN];
-val position_properties = [lineN, columnN] @ position_properties';
+val position_properties' = [end_lineN, end_columnN, end_offsetN, fileN, idN];
+val position_properties = [lineN, columnN, offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";