--- a/src/Pure/Thy/thy_syntax.scala Thu Mar 04 21:04:27 2021 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Thu Mar 04 21:19:05 2021 +0100
@@ -27,7 +27,7 @@
val visible = new mutable.ListBuffer[Command]
val visible_overlay = new mutable.ListBuffer[Command]
@tailrec
- def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]): Unit =
+ def check_ranges(ranges: List[Text.Range], commands: LazyList[(Command, Text.Offset)]): Unit =
{
(ranges, commands) match {
case (range :: more_ranges, (command, offset) #:: more_commands) =>
@@ -55,7 +55,7 @@
val commands =
(if (overlays.is_empty) node.command_iterator(perspective.range)
- else node.command_iterator()).toStream
+ else node.command_iterator()).to(LazyList)
check_ranges(perspective.ranges, commands)
(Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
}