src/Pure/Thy/thy_syntax.scala
changeset 38878 1d5b3175fd30
parent 38569 9d480f6a2589
child 40454 2516ea25a54b
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 30 20:11:21 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 30 20:12:43 2010 +0200
     1.3 @@ -77,9 +77,11 @@
     1.4        commands.iterator.find(_.is_unparsed) match {
     1.5          case Some(first_unparsed) =>
     1.6            val first =
     1.7 -            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
     1.8 +            commands.reverse_iterator(first_unparsed).
     1.9 +              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
    1.10            val last =
    1.11 -            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
    1.12 +            commands.iterator(first_unparsed).
    1.13 +              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
    1.14            val range =
    1.15              commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
    1.16