diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Isar/token.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -7,6 +7,10 @@
 package isabelle
 
 
+import scala.collection.mutable
+import scala.util.parsing.input
+
+
 object Token
 {
   /* tokens */
@@ -121,6 +125,34 @@
   }
 
 
+  /* 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 {
+      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)
+    val toks = new mutable.ListBuffer[Token]
+    var ctxt = context
+    while (!in.atEnd) {
+      Parsers.parse(Parsers.token_line(keywords, ctxt), in) match {
+        case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
+        case Parsers.NoSuccess(_, rest) =>
+          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
+      }
+    }
+    (toks.toList, ctxt)
+  }
+
+
   /* token reader */
 
   object Pos