# HG changeset patch
# User wenzelm
# Date 1294585436 -3600
# Node ID 4a8431c73cf231eb7eed5f6db275abc56792c0fd
# Parent  f4c07fdd1d48d06a0b85f3c56878abb9bfaf9490
discontinued unused end_line, end_column;

diff -r f4c07fdd1d48 -r 4a8431c73cf2 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Jan 09 13:58:31 2011 +0100
+++ b/src/Pure/General/markup.ML	Sun Jan 09 16:03:56 2011 +0100
@@ -22,8 +22,6 @@
   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 idN: string
@@ -187,13 +185,11 @@
 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, end_offsetN, fileN, idN];
+val position_properties' = [end_offsetN, fileN, idN];
 val position_properties = [lineN, columnN, offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";
diff -r f4c07fdd1d48 -r 4a8431c73cf2 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Jan 09 13:58:31 2011 +0100
+++ b/src/Pure/General/markup.scala	Sun Jan 09 16:03:56 2011 +0100
@@ -100,14 +100,11 @@
   val LINE = "line"
   val COLUMN = "column"
   val OFFSET = "offset"
-  val END_LINE = "end_line"
-  val END_COLUMN = "end_column"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
-  val POSITION_PROPERTIES =
-    Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
+  val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
 
   val POSITION = "position"
 
diff -r f4c07fdd1d48 -r 4a8431c73cf2 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun Jan 09 13:58:31 2011 +0100
+++ b/src/Pure/General/position.ML	Sun Jan 09 16:03:56 2011 +0100
@@ -163,13 +163,11 @@
 val no_range = (none, none);
 
 fun encode_range (Pos (count, props), Pos ((i, j, k), _)) =
-  let val props' = props |> fold_rev Properties.put
-    (value Markup.end_lineN i @ value Markup.end_columnN j @ value Markup.end_offsetN k)
+  let val props' = props |> fold Properties.put (value Markup.end_offsetN k)
   in Pos (count, props') end;
 
 fun reset_range (Pos (count, props)) =
-  let val props' = props |> fold Properties.remove
-    [Markup.end_lineN, Markup.end_columnN, Markup.end_offsetN]
+  let val props' = props |> Properties.remove Markup.end_offsetN
   in Pos (count, props') end;
 
 fun range pos pos' = (encode_range (pos, pos'), pos');
diff -r f4c07fdd1d48 -r 4a8431c73cf2 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sun Jan 09 13:58:31 2011 +0100
+++ b/src/Pure/General/position.scala	Sun Jan 09 16:03:56 2011 +0100
@@ -12,7 +12,6 @@
   type T = List[(String, String)]
 
   val Line = new Markup.Int_Property(Markup.LINE)
-  val End_Line = new Markup.Int_Property(Markup.END_LINE)
   val Offset = new Markup.Int_Property(Markup.OFFSET)
   val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
   val File = new Markup.Property(Markup.FILE)
diff -r f4c07fdd1d48 -r 4a8431c73cf2 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sun Jan 09 13:58:31 2011 +0100
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sun Jan 09 16:03:56 2011 +0100
@@ -12,7 +12,7 @@
 fun position_of (loc: PolyML.location) =
   let
     val {file = text, startLine = line, startPosition = offset,
-      endLine = end_line, endPosition = end_offset} = loc;
+      endLine = _, endPosition = end_offset} = loc;
     val loc_props =
       (case YXML.parse text of
         XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
@@ -20,7 +20,6 @@
   in
     Position.value Markup.lineN line @
     Position.value Markup.offsetN offset @
-    Position.value Markup.end_lineN end_line @
     Position.value Markup.end_offsetN end_offset @
     loc_props
   end |> Position.of_properties;