src/Pure/Isar/parse.scala
author wenzelm
Tue Mar 18 17:53:40 2014 +0100 (2014-03-18)
changeset 56209 3c89e21d9be2
parent 56208 06cc31dff138
child 56464 555f4be59be6
permissions -rw-r--r--
simplified (despite 70898d016538);
     1 /*  Title:      Pure/Isar/parse.scala
     2     Author:     Makarius
     3 
     4 Generic parsers for Isabelle/Isar outer syntax.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.util.parsing.combinator.Parsers
    11 import scala.annotation.tailrec
    12 
    13 
    14 object Parse
    15 {
    16   /* parsing tokens */
    17 
    18   trait Parser extends Parsers
    19   {
    20     type Elem = Token
    21 
    22     def filter_proper: Boolean = true
    23 
    24     @tailrec private def proper(in: Input): Input =
    25       if (!filter_proper || in.atEnd || in.first.is_proper) in
    26       else proper(in.rest)
    27 
    28     def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
    29     {
    30       def apply(raw_input: Input) =
    31       {
    32         val in = proper(raw_input)
    33         if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
    34         else {
    35           val token = in.first
    36           if (pred(token)) Success(token, proper(in.rest))
    37           else
    38             token.text match {
    39               case (txt, "") =>
    40                 Failure(s + " expected,\nbut " + txt + " was found", in)
    41               case (txt1, txt2) =>
    42                 Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
    43             }
    44         }
    45       }
    46     }
    47 
    48     def atom(s: String, pred: Elem => Boolean): Parser[String] =
    49       token(s, pred) ^^ (_.content)
    50 
    51     def command(name: String): Parser[String] =
    52       atom("command " + quote(name), tok => tok.is_command && tok.source == name)
    53 
    54     def keyword(name: String): Parser[String] =
    55       atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
    56 
    57     def string: Parser[String] = atom("string", _.is_string)
    58     def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
    59     def name: Parser[String] = atom("name declaration", _.is_name)
    60     def xname: Parser[String] = atom("name reference", _.is_xname)
    61     def text: Parser[String] = atom("text", _.is_text)
    62     def ML_source: Parser[String] = atom("ML source", _.is_text)
    63     def document_source: Parser[String] = atom("document source", _.is_text)
    64     def path: Parser[String] =
    65       atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
    66     def theory_name: Parser[String] =
    67       atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
    68 
    69     private def tag_name: Parser[String] =
    70       atom("tag name", tok =>
    71           tok.kind == Token.Kind.IDENT ||
    72           tok.kind == Token.Kind.STRING)
    73 
    74     def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
    75 
    76 
    77     /* wrappers */
    78 
    79     def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
    80 
    81     def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] =
    82     {
    83       val result = parse(p, in)
    84       val rest = proper(result.next)
    85       if (result.successful && !rest.atEnd) Error("bad input", rest)
    86       else result
    87     }
    88   }
    89 }
    90