--- a/src/Pure/Isar/outer_syntax.scala Thu Jun 16 11:59:29 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Thu Jun 16 17:25:16 2011 +0200
@@ -8,6 +8,7 @@
import scala.util.parsing.input.{Reader, CharSequenceReader}
+import scala.collection.mutable
class Outer_Syntax(symbols: Symbol.Interpretation)
@@ -73,4 +74,21 @@
def scan(input: CharSequence): List[Token] =
scan(new CharSequenceReader(input))
+
+ def scan_context(input: CharSequence, context: Scan.Context): (List[Token], Scan.Context) =
+ {
+ import lexicon._
+
+ var in: Reader[Char] = new CharSequenceReader(input)
+ val toks = new mutable.ListBuffer[Token]
+ var ctxt = context
+ while (!in.atEnd) {
+ parse(token_context(symbols, is_command, ctxt), in) match {
+ case Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
+ case NoSuccess(_, rest) =>
+ error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
+ }
+ }
+ (toks.toList, ctxt)
+ }
}