src/Pure/Isar/outer_syntax.scala

 */
 
 package isabelle
 
 
-import scala.util.parsing.input.{Reader, CharSequenceReader}
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 
 object Outer_Syntax

 
     Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
   }
 
 
-  /* token language */
-
-  def scan(input: CharSequence): List[Token] =
-  {
-    val in: Reader[Char] = new CharSequenceReader(input)
-    Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(keywords)), in) match {
-      case Token.Parsers.Success(tokens, _) => tokens
-      case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
-    }
-  }
-
-  def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
-  {
-    var in: Reader[Char] = new CharSequenceReader(input)
-    val toks = new mutable.ListBuffer[Token]
-    var ctxt = context
-    while (!in.atEnd) {
-      Token.Parsers.parse(Token.Parsers.token_line(keywords, ctxt), in) match {
-        case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
-        case Token.Parsers.NoSuccess(_, rest) =>
-          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
-      }
-    }
-    (toks.toList, ctxt)
-  }
-
-
   /* command spans */
 
   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   {
     val result = new mutable.ListBuffer[Command_Span.Span]

 
     result.toList
   }
 
   def parse_spans(input: CharSequence): List[Command_Span.Span] =
-    parse_spans(scan(input))
+    parse_spans(Token.explode(keywords, input))
 
 
   /* overall document structure */
 
   def heading_level(command: Command): Option[Int] =