src/Pure/Isar/parse.scala
author wenzelm
Thu Aug 23 17:46:03 2012 +0200 (2012-08-23)
changeset 48911 5debc3e4fa81
parent 48718 73e6c22e2d94
child 48912 ffdb37019b2f
permissions -rw-r--r--
tuned messages: end-of-input rarely means physical end-of-file from the past;
     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 import scala.util.parsing.combinator.Parsers
    10 import scala.annotation.tailrec
    11 
    12 
    13 object Parse
    14 {
    15   /* parsing tokens */
    16 
    17   trait Parser extends Parsers
    18   {
    19     type Elem = Token
    20 
    21     def filter_proper: Boolean = true
    22 
    23     @tailrec private def proper(in: Input): Input =
    24       if (!filter_proper || in.atEnd || in.first.is_proper) in
    25       else proper(in.rest)
    26 
    27     def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
    28     {
    29       def apply(raw_input: Input) =
    30       {
    31         val in = proper(raw_input)
    32         if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
    33         else {
    34           val token = in.first
    35           if (pred(token)) Success(token, proper(in.rest))
    36           else
    37             token.text match {
    38               case (txt, "") =>
    39                 Failure(s + " expected,\nbut " + txt + " was found", in)
    40               case (txt1, txt2) =>
    41                 Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
    42             }
    43         }
    44       }
    45     }
    46 
    47     def not_eof: Parser[Elem] = token("input token", _ => true)
    48     def eof: Parser[Unit] = not(not_eof)
    49 
    50     def atom(s: String, pred: Elem => Boolean): Parser[String] =
    51       token(s, pred) ^^ (_.content)
    52 
    53     def command(name: String): Parser[String] =
    54       atom("command " + quote(name), tok => tok.is_command && tok.source == name)
    55 
    56     def keyword(name: String): Parser[String] =
    57       atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
    58 
    59     def string: Parser[String] = atom("string", _.is_string)
    60     def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
    61     def name: Parser[String] = atom("name declaration", _.is_name)
    62     def xname: Parser[String] = atom("name reference", _.is_xname)
    63     def text: Parser[String] = atom("text", _.is_text)
    64     def ML_source: Parser[String] = atom("ML source", _.is_text)
    65     def doc_source: Parser[String] = atom("document source", _.is_text)
    66     def path: Parser[String] =
    67       atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content))
    68     def theory_name: Parser[String] =
    69       atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content))
    70 
    71     private def tag_name: Parser[String] =
    72       atom("tag name", tok =>
    73           tok.kind == Token.Kind.IDENT ||
    74           tok.kind == Token.Kind.STRING)
    75 
    76     def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
    77 
    78 
    79     /* wrappers */
    80 
    81     def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
    82     def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] =
    83       parse(p <~ eof, in)
    84   }
    85 }
    86