src/Pure/Thy/thy_syntax.scala
changeset 73368 894f29abe5fc
parent 73359 d8a0e996614b
equal deleted inserted replaced
73367:77ef8bef0593 73368:894f29abe5fc
    25     else {
    25     else {
    26       val has_overlay = overlays.commands
    26       val has_overlay = overlays.commands
    27       val visible = new mutable.ListBuffer[Command]
    27       val visible = new mutable.ListBuffer[Command]
    28       val visible_overlay = new mutable.ListBuffer[Command]
    28       val visible_overlay = new mutable.ListBuffer[Command]
    29       @tailrec
    29       @tailrec
    30       def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]): Unit =
    30       def check_ranges(ranges: List[Text.Range], commands: LazyList[(Command, Text.Offset)]): Unit =
    31       {
    31       {
    32         (ranges, commands) match {
    32         (ranges, commands) match {
    33           case (range :: more_ranges, (command, offset) #:: more_commands) =>
    33           case (range :: more_ranges, (command, offset) #:: more_commands) =>
    34             val command_range = command.range + offset
    34             val command_range = command.range + offset
    35             range compare command_range match {
    35             range compare command_range match {
    53         }
    53         }
    54       }
    54       }
    55 
    55 
    56       val commands =
    56       val commands =
    57         (if (overlays.is_empty) node.command_iterator(perspective.range)
    57         (if (overlays.is_empty) node.command_iterator(perspective.range)
    58          else node.command_iterator()).toStream
    58          else node.command_iterator()).to(LazyList)
    59       check_ranges(perspective.ranges, commands)
    59       check_ranges(perspective.ranges, commands)
    60       (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
    60       (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
    61     }
    61     }
    62   }
    62   }
    63 
    63