src/Pure/Isar/outer_syntax.scala
changeset 64616 dc3ec40fe41b
parent 63867 fb46c031c841
child 65383 089f2edefb77
     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            }