src/Pure/Isar/outer_syntax.scala
changeset 59319 677615cba30d
parent 59122 c1dbcde94cd2
child 59684 86a76300137e
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jan 07 18:09:11 2015 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Jan 08 20:56:39 2015 +0100
     1.3 @@ -194,7 +194,7 @@
     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 +        if (span.nonEmpty && span.head.is_command && !span.exists(_.is_error)) {
     1.9            val name = span.head.source
    1.10            val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
    1.11            Command_Span.Command_Span(name, pos)
    1.12 @@ -206,8 +206,8 @@
    1.13  
    1.14      def flush()
    1.15      {
    1.16 -      if (!content.isEmpty) { ship(content.toList); content.clear }
    1.17 -      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
    1.18 +      if (content.nonEmpty) { ship(content.toList); content.clear }
    1.19 +      if (improper.nonEmpty) { ship(improper.toList); improper.clear }
    1.20      }
    1.21  
    1.22      for (tok <- toks) {