# HG changeset patch
# User wenzelm
# Date 1399049687 -7200
# Node ID 853f1bcc37551ad7ce9f33a69f2c0c876b1ac4d3
# Parent  8872e0776e97b87f9a2590be7a58371d3ae36616
avoid deprecated Scala syntax;

diff -r 8872e0776e97 -r 853f1bcc3755 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri May 02 14:15:23 2014 +0200
+++ b/src/Pure/General/scan.scala	Fri May 02 18:54:47 2014 +0200
@@ -458,7 +458,7 @@
     class Paged_Reader(override val offset: Int) extends Byte_Reader
     {
       override lazy val source: CharSequence = restricted_seq
-      def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\032'
+      def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\u001a'
       def rest: Paged_Reader = if (seq.isDefinedAt(offset)) new Paged_Reader(offset + 1) else this
       def pos: InputPosition = new OffsetPosition(source, offset)
       def atEnd: Boolean = !seq.isDefinedAt(offset)