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