# HG changeset patch
# User wenzelm
# Date 1217957346 -7200
# Node ID d4c5ddf98869161447866f8f738de691d05fd3e0
# Parent  7420e78f1541e2f0e0aae87423e47d2d7299a0ad
advance: operate on symbol list (less overhead);

diff -r 7420e78f1541 -r d4c5ddf98869 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 05 19:29:02 2008 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 05 19:29:06 2008 +0200
@@ -15,7 +15,7 @@
   val line_file: int -> string -> T
   val line: int -> T
   val file: string -> T
-  val advance: Symbol.symbol -> T -> T
+  val advance: Symbol.symbol list -> T -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
   val of_properties: Markup.property list -> T
@@ -53,10 +53,14 @@
 val file = line_file 1;
 
 
-fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
-  | advance s (pos as Pos (SOME (m, n), props)) =
+(* advance position *)
+
+fun advance_count "\n" (m, _) = (m + 1, 1)
+  | advance_count s (m, n) =
       if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
-      then Pos (SOME (m, n + 1), props) else pos
+      then (m, n + 1) else (m, n);
+
+fun advance syms (Pos (SOME count, props)) = Pos (SOME (fold advance_count syms count), props)
   | advance _ pos = pos;