src/Pure/Isar/outer_syntax.scala
changeset 43411 0206466ee473
parent 40533 e38e80686ce5
child 43445 270bbbcda059
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Jun 16 11:59:29 2011 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Jun 16 17:25:16 2011 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  
     1.6  import scala.util.parsing.input.{Reader, CharSequenceReader}
     1.7 +import scala.collection.mutable
     1.8  
     1.9  
    1.10  class Outer_Syntax(symbols: Symbol.Interpretation)
    1.11 @@ -73,4 +74,21 @@
    1.12  
    1.13    def scan(input: CharSequence): List[Token] =
    1.14      scan(new CharSequenceReader(input))
    1.15 +
    1.16 +  def scan_context(input: CharSequence, context: Scan.Context): (List[Token], Scan.Context) =
    1.17 +  {
    1.18 +    import lexicon._
    1.19 +
    1.20 +    var in: Reader[Char] = new CharSequenceReader(input)
    1.21 +    val toks = new mutable.ListBuffer[Token]
    1.22 +    var ctxt = context
    1.23 +    while (!in.atEnd) {
    1.24 +      parse(token_context(symbols, is_command, ctxt), in) match {
    1.25 +        case Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    1.26 +        case NoSuccess(_, rest) =>
    1.27 +          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.28 +      }
    1.29 +    }
    1.30 +    (toks.toList, ctxt)
    1.31 +  }
    1.32  }