src/Pure/PIDE/document.scala
changeset 37072 9105c8237c7a
parent 37071 dd3540a489f7
child 37073 5e42e36a6693
equal deleted inserted replaced
37071:dd3540a489f7 37072:9105c8237c7a
    83     def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    83     def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    84     {
    84     {
    85       commands.iterator.find(is_unparsed) match {
    85       commands.iterator.find(is_unparsed) match {
    86         case Some(first_unparsed) =>
    86         case Some(first_unparsed) =>
    87           val first =
    87           val first =
    88             commands.rev_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
    88             commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
    89           val last =
    89           val last =
    90             commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
    90             commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
    91           val range =
    91           val range =
    92             commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
    92             commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
    93 
    93