# HG changeset patch
# User wenzelm
# Date 1217883308 -7200
# Node ID 3703dbd0cdea5404574d9572fc203b9d83250757
# Parent  044901e02cc67627c1a1d978aca43444309ddcfa
added encode_range;
tuned;

diff -r 044901e02cc6 -r 3703dbd0cdea src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Aug 04 22:55:04 2008 +0200
+++ b/src/Pure/General/position.ML	Mon Aug 04 22:55:08 2008 +0200
@@ -8,7 +8,6 @@
 signature POSITION =
 sig
   type T
-  type range = T * T
   val line_of: T -> int option
   val column_of: T -> int option
   val file_of: T -> string option
@@ -26,6 +25,8 @@
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
   val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
+  type range = T * T
+  val encode_range: range -> T
 end;
 
 structure Position: POSITION =
@@ -34,7 +35,6 @@
 (* datatype position *)
 
 datatype T = Pos of (int * int) option * Markup.property list;
-type range = T * T
 
 fun line_of (Pos (SOME (m, _), _)) = SOME m
   | line_of _ = NONE;
@@ -119,4 +119,16 @@
 
 end;
 
+
+(* range *)
+
+type range = T * T;
+
+fun encode_range (Pos (count, props), Pos (end_count, _)) =
+  let val props' = props |> fold_rev (AList.update op =)
+    (case end_count of
+      NONE => []
+    | SOME (m, n) => [(Markup.end_lineN, string_of_int m), (Markup.end_columnN, string_of_int n)])
+  in Pos (count, props') end;
+
 end;