tuned;
authorwenzelm
Tue Dec 20 10:45:20 2016 +0100 (2016-12-20)
changeset 64616dc3ec40fe41b
parent 64615 fd0d6de380c6
child 64617 01e50039edc9
tuned;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Dec 20 10:44:36 2016 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 20 10:45:20 2016 +0100
     1.3 @@ -154,8 +154,8 @@
     1.4                val name = cmd.source
     1.5                val offset =
     1.6                  (0 /: span.takeWhile(_ != cmd)) {
     1.7 -                  case (i, tok) => i + Symbol.iterator(tok.source).length }
     1.8 -              val end_offset = offset + Symbol.iterator(name).length
     1.9 +                  case (i, tok) => i + Symbol.length(tok.source) }
    1.10 +              val end_offset = offset + Symbol.length(name)
    1.11                val pos = Position.Range(Text.Range(offset, end_offset) + 1)
    1.12                Command_Span.Command_Span(name, pos)
    1.13            }
     2.1 --- a/src/Pure/PIDE/protocol.scala	Tue Dec 20 10:44:36 2016 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Dec 20 10:45:20 2016 +0100
     2.3 @@ -337,8 +337,7 @@
     2.4      val toks_yxml =
     2.5      {
     2.6        import XML.Encode._
     2.7 -      val encode_tok: T[Token] =
     2.8 -        (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
     2.9 +      val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
    2.10        YXML.string_of_body(list(encode_tok)(toks))
    2.11      }
    2.12