src/Pure/General/scan.scala
changeset 73340 0ffcad1f6130
parent 73136 ca17e9ebfdf1
child 73357 31d4274f32de
--- a/src/Pure/General/scan.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/scan.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -478,7 +478,7 @@
       def pos: InputPosition = new OffsetPosition(source, offset)
       def atEnd: Boolean = !seq.isDefinedAt(offset)
       override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n)
-      def close { buffered_stream.close }
+      def close: Unit = buffered_stream.close
     }
     new Paged_Reader(0)
   }