diff -r 240cb0cfba5c -r 90eaac98b3fa src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Mon Mar 07 13:45:09 2022 +0100
+++ b/src/Pure/General/scan.scala	Mon Mar 07 16:01:54 2022 +0100
@@ -61,9 +61,8 @@
           var count = 0
           var finished = false
           while (!finished && i < end && count < max_count) {
-            val n = matcher(i, end)
-            val sym = in.source.subSequence(i, i + n).toString
-            if (pred(sym)) { i += n; count += 1 }
+            val sym = matcher.match_symbol(i)
+            if (pred(sym)) { i += sym.length; count += 1 }
             else finished = true
           }
           if (count < min_count) Failure("bad input", in)
@@ -151,8 +150,8 @@
         var d = depth
         var finished = false
         while (!finished && i < end) {
-          val n = matcher(i, end)
-          val sym = in.source.subSequence(i, i + n).toString
+          val sym = matcher.match_symbol(i)
+          val n = sym.length
           if (Symbol.is_open(sym)) { i += n; d += 1 }
           else if (Symbol.is_close(sym) && d > 0) { i += n; d -= 1; if (d == 0) finished = true }
           else if (d > 0) i += n