# HG changeset patch
# User wenzelm
# Date 1482227120 -3600
# Node ID dc3ec40fe41b2771cac81fd3c67c4a450ab0a940
# Parent  fd0d6de380c67f2d2d4d72d4f293ad5786cb2bc3
tuned;

diff -r fd0d6de380c6 -r dc3ec40fe41b src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Dec 20 10:44:36 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 20 10:45:20 2016 +0100
@@ -154,8 +154,8 @@
               val name = cmd.source
               val offset =
                 (0 /: span.takeWhile(_ != cmd)) {
-                  case (i, tok) => i + Symbol.iterator(tok.source).length }
-              val end_offset = offset + Symbol.iterator(name).length
+                  case (i, tok) => i + Symbol.length(tok.source) }
+              val end_offset = offset + Symbol.length(name)
               val pos = Position.Range(Text.Range(offset, end_offset) + 1)
               Command_Span.Command_Span(name, pos)
           }
diff -r fd0d6de380c6 -r dc3ec40fe41b src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Dec 20 10:44:36 2016 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Dec 20 10:45:20 2016 +0100
@@ -337,8 +337,7 @@
     val toks_yxml =
     {
       import XML.Encode._
-      val encode_tok: T[Token] =
-        (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
+      val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
       YXML.string_of_body(list(encode_tok)(toks))
     }