# HG changeset patch
# User wenzelm
# Date 1208012447 -7200
# Node ID ff317b19e24ed7f3dce65fc8ea89fac425fc7ffe
# Parent  90c0b075c0d3417ab20e6999dd0c6709890c814e
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);

diff -r 90c0b075c0d3 -r ff317b19e24e src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 12 17:00:47 2008 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 12 17:00:47 2008 +0200
@@ -46,8 +46,9 @@
 val path = file o Path.implode o Path.expand;
 
 fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
-  | advance sym (pos as Pos (SOME (m, n), props)) =
-      if Symbol.is_regular sym then Pos (SOME (m, n + 1), props) else pos
+  | advance s (pos as Pos (SOME (m, n), props)) =
+      if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
+      then Pos (SOME (m, n + 1), props) else pos
   | advance _ pos = pos;