# 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;