# HG changeset patch
# User wenzelm
# Date 1614889145 -3600
# Node ID 894f29abe5fc7dfdf6722a7a8ce3e1d2e60d00f1
# Parent  77ef8bef0593a844435cd7c67493b8579ab7840e
clarified signature --- fewer warnings;

diff -r 77ef8bef0593 -r 894f29abe5fc src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Mar 04 21:04:27 2021 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Mar 04 21:19:05 2021 +0100
@@ -186,10 +186,10 @@
   private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) =
   {
     val token = Token.Parsers.token(bootstrap_keywords)
-    def make_tokens(in: Reader[Char]): Stream[Token] =
+    def make_tokens(in: Reader[Char]): LazyList[Token] =
       token(in) match {
         case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
-        case _ => Stream.empty
+        case _ => LazyList.empty
       }
 
     val all_tokens = make_tokens(reader)
diff -r 77ef8bef0593 -r 894f29abe5fc src/Pure/Thy/thy_syntax.scala
--- 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))
     }