src/Pure/Isar/parse.scala
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 36956 21be4832c362
child 43283 446e6621762d
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
wenzelm@34159
     1
/*  Title:      Pure/Isar/outer_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@34159
     9
import scala.util.parsing.combinator.Parsers
wenzelm@34159
    10
wenzelm@34159
    11
wenzelm@36948
    12
object Parse
wenzelm@34159
    13
{
wenzelm@34161
    14
  /* parsing tokens */
wenzelm@34161
    15
wenzelm@34159
    16
  trait Parser extends Parsers
wenzelm@34159
    17
  {
wenzelm@36956
    18
    type Elem = Token
wenzelm@34159
    19
wenzelm@34266
    20
    def filter_proper = true
wenzelm@34266
    21
wenzelm@34161
    22
    private def proper(in: Input): Input =
wenzelm@34311
    23
      if (in.atEnd || !in.first.is_ignored || !filter_proper) in
wenzelm@34161
    24
      else proper(in.rest)
wenzelm@34159
    25
wenzelm@34159
    26
    def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
wenzelm@34159
    27
    {
wenzelm@34161
    28
      def apply(raw_input: Input) =
wenzelm@34159
    29
      {
wenzelm@34161
    30
        val in = proper(raw_input)
wenzelm@34159
    31
        if (in.atEnd) Failure(s + " expected (past end-of-file!)", in)
wenzelm@34159
    32
        else {
wenzelm@34159
    33
          val token = in.first
wenzelm@34161
    34
          if (pred(token)) Success(token, proper(in.rest))
wenzelm@34159
    35
          else
wenzelm@34159
    36
            token.text match {
wenzelm@34159
    37
              case (txt, "") =>
wenzelm@34159
    38
                Failure(s + " expected,\nbut " + txt + " was found", in)
wenzelm@34159
    39
              case (txt1, txt2) =>
wenzelm@34159
    40
                Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
wenzelm@34159
    41
            }
wenzelm@34159
    42
        }
wenzelm@34159
    43
      }
wenzelm@34159
    44
    }
wenzelm@34159
    45
wenzelm@34266
    46
    def not_eof: Parser[Elem] = token("input token", _ => true)
wenzelm@34266
    47
    def eof: Parser[Unit] = not(not_eof)
wenzelm@34266
    48
wenzelm@34168
    49
    def atom(s: String, pred: Elem => Boolean): Parser[String] =
wenzelm@34168
    50
      token(s, pred) ^^ (_.content)
wenzelm@34168
    51
wenzelm@34168
    52
    def keyword(name: String): Parser[String] =
wenzelm@36956
    53
      atom(Token.Kind.KEYWORD.toString + " \"" + name + "\"",
wenzelm@36956
    54
        tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
wenzelm@34159
    55
wenzelm@34168
    56
    def name: Parser[String] = atom("name declaration", _.is_name)
wenzelm@34168
    57
    def xname: Parser[String] = atom("name reference", _.is_xname)
wenzelm@34168
    58
    def text: Parser[String] = atom("text", _.is_text)
wenzelm@34168
    59
    def ML_source: Parser[String] = atom("ML source", _.is_text)
wenzelm@34168
    60
    def doc_source: Parser[String] = atom("document source", _.is_text)
wenzelm@34168
    61
    def path: Parser[String] = atom("file name/path specification", _.is_name)
wenzelm@34168
    62
wenzelm@34168
    63
    private def tag_name: Parser[String] =
wenzelm@34168
    64
      atom("tag name", tok =>
wenzelm@36956
    65
          tok.kind == Token.Kind.IDENT ||
wenzelm@36956
    66
          tok.kind == Token.Kind.STRING)
wenzelm@34168
    67
wenzelm@34168
    68
    def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
wenzelm@34161
    69
wenzelm@34161
    70
wenzelm@34161
    71
    /* wrappers */
wenzelm@34161
    72
wenzelm@36956
    73
    def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
wenzelm@36956
    74
    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = parse(phrase(p), in)
wenzelm@34159
    75
  }
wenzelm@34159
    76
}
wenzelm@34159
    77