diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/Isar/token.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -128,18 +128,15 @@
   /* explode */
 
   def explode(keywords: Keyword.Keywords, inp: CharSequence): List[Token] =
-  {
-    val in: input.Reader[Char] = new input.CharSequenceReader(inp)
-    Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), in) match {
+    Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), Scan.char_reader(inp)) match {
       case Parsers.Success(tokens, _) => tokens
       case _ => error("Unexpected failure of tokenizing input:\n" + inp.toString)
     }
-  }
 
   def explode_line(keywords: Keyword.Keywords, inp: CharSequence, context: Scan.Line_Context)
     : (List[Token], Scan.Line_Context) =
   {
-    var in: input.Reader[Char] = new input.CharSequenceReader(inp)
+    var in: input.Reader[Char] = Scan.char_reader(inp)
     val toks = new mutable.ListBuffer[Token]
     var ctxt = context
     while (!in.atEnd) {
@@ -180,7 +177,7 @@
       val offset: Symbol.Offset,
       val file: String,
       val id: String)
-    extends scala.util.parsing.input.Position
+    extends input.Position
   {
     def column = 0
     def lineContents = ""
@@ -210,7 +207,7 @@
     override def toString: String = Position.here(position(), delimited = false)
   }
 
-  abstract class Reader extends scala.util.parsing.input.Reader[Token]
+  abstract class Reader extends input.Reader[Token]
 
   private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader
   {