src/Pure/Isar/outer_syntax.scala
changeset 57910 a50837b637dc
parent 57907 7fc36b4c7cce
child 57911 dcb758188aa6
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 13:18:17 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 14:15:58 2014 +0200
     1.3 @@ -161,8 +161,11 @@
     1.4      def ship(span: List[Token])
     1.5      {
     1.6        val kind =
     1.7 -        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
     1.8 -          Command_Span.Command_Span(span.head.source)
     1.9 +        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
    1.10 +          val name = span.head.source
    1.11 +          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length))
    1.12 +          Command_Span.Command_Span(name, pos)
    1.13 +        }
    1.14          else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    1.15          else Command_Span.Malformed_Span
    1.16        result += Command_Span.Span(kind, span)