1.1 --- a/src/Pure/General/position.ML	Mon Aug 04 22:55:04 2008 +0200
     1.2 +++ b/src/Pure/General/position.ML	Mon Aug 04 22:55:08 2008 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  signature POSITION =
     1.5  sig
     1.6    type T
     1.7 -  type range = T * T
     1.8    val line_of: T -> int option
     1.9    val column_of: T -> int option
    1.10    val file_of: T -> string option
    1.11 @@ -26,6 +25,8 @@
    1.12    val thread_data: unit -> T
    1.13    val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
    1.14    val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
    1.15 +  type range = T * T
    1.16 +  val encode_range: range -> T
    1.17  end;
    1.18  
    1.19  structure Position: POSITION =
    1.20 @@ -34,7 +35,6 @@
    1.21  (* datatype position *)
    1.22  
    1.23  datatype T = Pos of (int * int) option * Markup.property list;
    1.24 -type range = T * T
    1.25  
    1.26  fun line_of (Pos (SOME (m, _), _)) = SOME m
    1.27    | line_of _ = NONE;
    1.28 @@ -119,4 +119,16 @@
    1.29  
    1.30  end;
    1.31  
    1.32 +
    1.33 +(* range *)
    1.34 +
    1.35 +type range = T * T;
    1.36 +
    1.37 +fun encode_range (Pos (count, props), Pos (end_count, _)) =
    1.38 +  let val props' = props |> fold_rev (AList.update op =)
    1.39 +    (case end_count of
    1.40 +      NONE => []
    1.41 +    | SOME (m, n) => [(Markup.end_lineN, string_of_int m), (Markup.end_columnN, string_of_int n)])
    1.42 +  in Pos (count, props') end;
    1.43 +
    1.44  end;