--- 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