# HG changeset patch
# User wenzelm
# Date 1217883304 -7200
# Node ID 044901e02cc67627c1a1d978aca43444309ddcfa
# Parent  dcec1c564f05a1084330056b4dfc9f9f5d415789
added end_line, end_column properties;

diff -r dcec1c564f05 -r 044901e02cc6 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Aug 04 22:55:00 2008 +0200
+++ b/src/Pure/General/markup.ML	Mon Aug 04 22:55:04 2008 +0200
@@ -22,6 +22,8 @@
   val property_internal: property
   val lineN: string
   val columnN: string
+  val end_lineN: string
+  val end_columnN: string
   val fileN: string
   val position_properties: string list
   val positionN: string val position: T
@@ -120,10 +122,12 @@
 
 val lineN = "line";
 val columnN = "column";
+val end_lineN = "end_line";
+val end_columnN = "end_column";
 val fileN = "file";
 val idN = "id";
 
-val position_properties = [lineN, columnN, fileN, idN];
+val position_properties = [lineN, columnN, end_lineN, end_columnN, fileN, idN];
 val (positionN, position) = markup_elem "position";
 
 val (locationN, location) = markup_elem "location";