src/Pure/Isar/parse.scala
author wenzelm
Thu, 19 Jul 2012 14:24:40 +0200
changeset 48349 a78e5d399599
parent 46943 ac1c41ea856d
child 48484 70898d016538
permissions -rw-r--r--
support Session.Queue with ordering and dependencies;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43283
446e6621762d updated headers;
wenzelm
parents: 36956
diff changeset
     1
/*  Title:      Pure/Isar/parse.scala
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
     3
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
     4
Generic parsers for Isabelle/Isar outer syntax.
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
     5
*/
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
     6
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
     7
package isabelle
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
     8
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
     9
import scala.util.parsing.combinator.Parsers
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    10
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    11
36948
d2cdad45fd14 renamed Outer_Parse to Parse (in Scala);
wenzelm
parents: 34311
diff changeset
    12
object Parse
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    13
{
34161
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    14
  /* parsing tokens */
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    15
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    16
  trait Parser extends Parsers
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    17
  {
36956
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36948
diff changeset
    18
    type Elem = Token
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    19
34266
bfe8d6998734 added filter_proper parameter;
wenzelm
parents: 34168
diff changeset
    20
    def filter_proper = true
bfe8d6998734 added filter_proper parameter;
wenzelm
parents: 34168
diff changeset
    21
34161
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    22
    private def proper(in: Input): Input =
34311
f0a6f02ad705 Outer_Lex.is_ignored;
wenzelm
parents: 34268
diff changeset
    23
      if (in.atEnd || !in.first.is_ignored || !filter_proper) in
34161
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    24
      else proper(in.rest)
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    25
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    26
    def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    27
    {
34161
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    28
      def apply(raw_input: Input) =
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    29
      {
34161
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    30
        val in = proper(raw_input)
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    31
        if (in.atEnd) Failure(s + " expected (past end-of-file!)", in)
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    32
        else {
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    33
          val token = in.first
34161
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    34
          if (pred(token)) Success(token, proper(in.rest))
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    35
          else
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    36
            token.text match {
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    37
              case (txt, "") =>
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    38
                Failure(s + " expected,\nbut " + txt + " was found", in)
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    39
              case (txt1, txt2) =>
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    40
                Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    41
            }
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    42
        }
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    43
      }
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    44
    }
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    45
34266
bfe8d6998734 added filter_proper parameter;
wenzelm
parents: 34168
diff changeset
    46
    def not_eof: Parser[Elem] = token("input token", _ => true)
bfe8d6998734 added filter_proper parameter;
wenzelm
parents: 34168
diff changeset
    47
    def eof: Parser[Unit] = not(not_eof)
bfe8d6998734 added filter_proper parameter;
wenzelm
parents: 34168
diff changeset
    48
34168
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    49
    def atom(s: String, pred: Elem => Boolean): Parser[String] =
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    50
      token(s, pred) ^^ (_.content)
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    51
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    52
    def keyword(name: String): Parser[String] =
44181
wenzelm
parents: 43283
diff changeset
    53
      atom(Token.Kind.KEYWORD.toString + " " + quote(name),
36956
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36948
diff changeset
    54
        tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    55
46943
ac1c41ea856d clarified syntax of prospective keywords;
wenzelm
parents: 44181
diff changeset
    56
    def string: Parser[String] = atom("string", _.is_string)
48349
a78e5d399599 support Session.Queue with ordering and dependencies;
wenzelm
parents: 46943
diff changeset
    57
    def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
34168
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    58
    def name: Parser[String] = atom("name declaration", _.is_name)
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    59
    def xname: Parser[String] = atom("name reference", _.is_xname)
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    60
    def text: Parser[String] = atom("text", _.is_text)
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    61
    def ML_source: Parser[String] = atom("ML source", _.is_text)
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    62
    def doc_source: Parser[String] = atom("document source", _.is_text)
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    63
    def path: Parser[String] = atom("file name/path specification", _.is_name)
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    64
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    65
    private def tag_name: Parser[String] =
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    66
      atom("tag name", tok =>
36956
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36948
diff changeset
    67
          tok.kind == Token.Kind.IDENT ||
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36948
diff changeset
    68
          tok.kind == Token.Kind.STRING)
34168
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    69
18843829c7f2 clarified atom parser: return content;
wenzelm
parents: 34161
diff changeset
    70
    def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
34161
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    71
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    72
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    73
    /* wrappers */
4c845a8f1357 consider proper input only;
wenzelm
parents: 34159
diff changeset
    74
36956
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36948
diff changeset
    75
    def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36948
diff changeset
    76
    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = parse(phrase(p), in)
34159
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    77
  }
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    78
}
903092d61519 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff changeset
    79