# HG changeset patch
# User wenzelm
# Date 1218109482 -7200
# Node ID e0ee3cc240fe74eba1721a21b377effa23b5c835
# Parent  f49f6275cefa36f655d830f9a791966551b514bf
advance: single argument (again);
added range;
tuned;

diff -r f49f6275cefa -r e0ee3cc240fe src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Thu Aug 07 13:44:36 2008 +0200
+++ b/src/Pure/General/position.ML	Thu Aug 07 13:44:42 2008 +0200
@@ -15,19 +15,20 @@
   val line_file: int -> string -> T
   val line: int -> T
   val file: string -> T
-  val advance: Symbol.symbol list -> T -> T
+  val advance: Symbol.symbol -> T -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
   val of_properties: Markup.property list -> T
   val properties_of: T -> Markup.property list
   val default_properties: T -> Markup.property list -> Markup.property list
+  val report: Markup.T -> T -> unit
   val str_of: T -> string
+  type range = T * T
+  val encode_range: range -> T
+  val range: T -> T -> range
   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
-  val report: Markup.T -> T -> unit
 end;
 
 structure Position: POSITION =
@@ -60,7 +61,7 @@
       if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
       then (m, n + 1) else (m, n);
 
-fun advance syms (Pos (SOME count, props)) = Pos (SOME (fold advance_count syms count), props)
+fun advance sym (Pos (SOME count, props)) = Pos (SOME (advance_count sym count), props)
   | advance _ pos = pos;
 
 
@@ -92,6 +93,10 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
+fun report markup pos =
+  if pos = none then ()
+  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) "");
+
 
 (* str_of *)
 
@@ -109,22 +114,6 @@
   end;
 
 
-(* thread data *)
-
-local val tag = Universal.tag () : T Universal.tag in
-
-fun thread_data () = the_default none (Multithreading.get_data tag);
-
-fun setmp_thread_data pos f x =
-  if ! Output.debugging then f x
-  else Library.setmp_thread_data tag (thread_data ()) pos f x;
-
-fun setmp_thread_data_seq pos f seq =
-  setmp_thread_data pos f seq |> Seq.wrap (fn pull => setmp_thread_data pos pull ());
-
-end;
-
-
 (* range *)
 
 type range = T * T;
@@ -136,11 +125,22 @@
     | SOME (m, n) => [(Markup.end_lineN, string_of_int m), (Markup.end_columnN, string_of_int n)])
   in Pos (count, props') end;
 
+fun range pos pos' = (encode_range (pos, pos'), pos');
 
-(* report markup *)
+
+(* thread data *)
+
+local val tag = Universal.tag () : T Universal.tag in
 
-fun report markup pos =
-  if pos = none then ()
-  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) "");
+fun thread_data () = the_default none (Multithreading.get_data tag);
+
+fun setmp_thread_data pos f x =
+  if ! Output.debugging then f x
+  else Library.setmp_thread_data tag (thread_data ()) pos f x;
+
+fun setmp_thread_data_seq pos f x =
+  setmp_thread_data pos f x |> Seq.wrap (fn pull => setmp_thread_data pos pull ());
 
 end;
+
+end;