src/Pure/Isar/outer_syntax.scala
changeset 59083 88b0b1f28adc
parent 59077 7e0d3da6e6d8
child 59122 c1dbcde94cd2
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Dec 03 11:50:58 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Dec 03 14:04:38 2014 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import scala.util.parsing.input.{Reader, CharSequenceReader}
     1.8  import scala.collection.mutable
     1.9  import scala.annotation.tailrec
    1.10  
    1.11 @@ -184,33 +183,6 @@
    1.12    }
    1.13  
    1.14  
    1.15 -  /* token language */
    1.16 -
    1.17 -  def scan(input: CharSequence): List[Token] =
    1.18 -  {
    1.19 -    val in: Reader[Char] = new CharSequenceReader(input)
    1.20 -    Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(keywords)), in) match {
    1.21 -      case Token.Parsers.Success(tokens, _) => tokens
    1.22 -      case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
    1.23 -    }
    1.24 -  }
    1.25 -
    1.26 -  def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
    1.27 -  {
    1.28 -    var in: Reader[Char] = new CharSequenceReader(input)
    1.29 -    val toks = new mutable.ListBuffer[Token]
    1.30 -    var ctxt = context
    1.31 -    while (!in.atEnd) {
    1.32 -      Token.Parsers.parse(Token.Parsers.token_line(keywords, ctxt), in) match {
    1.33 -        case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    1.34 -        case Token.Parsers.NoSuccess(_, rest) =>
    1.35 -          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.36 -      }
    1.37 -    }
    1.38 -    (toks.toList, ctxt)
    1.39 -  }
    1.40 -
    1.41 -
    1.42    /* command spans */
    1.43  
    1.44    def parse_spans(toks: List[Token]): List[Command_Span.Span] =
    1.45 @@ -249,7 +221,7 @@
    1.46    }
    1.47  
    1.48    def parse_spans(input: CharSequence): List[Command_Span.Span] =
    1.49 -    parse_spans(scan(input))
    1.50 +    parse_spans(Token.explode(keywords, input))
    1.51  
    1.52  
    1.53    /* overall document structure */