1/*  Title:      Pure/Isar/parse.scala
2    Author:     Makarius
3
4Generic parsers for Isabelle/Isar outer syntax.
5*/
6
7package isabelle
8
9
10import scala.util.parsing.combinator.Parsers
11import scala.annotation.tailrec
12
13
14object 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    private def proper_position: Parser[Position.T] =
29      new Parser[Position.T] {
30        def apply(raw_input: Input) =
31        {
32          val in = proper(raw_input)
33          val pos =
34            in.pos match {
35              case pos: Token.Pos => pos
36              case _ => Token.Pos.none
37            }
38          Success(if (in.atEnd) pos.position() else pos.position(in.first), in)
39        }
40      }
41
42    def position[A](parser: Parser[A]): Parser[(A, Position.T)] =
43      proper_position ~ parser ^^ { case x ~ y => (y, x) }
44
45    def token(s: String, pred: Elem => Boolean): Parser[Elem] =
46      new Parser[Elem] {
47        def apply(raw_input: Input) =
48        {
49          val in = proper(raw_input)
50          if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
51          else {
52            val token = in.first
53            if (pred(token)) Success(token, proper(in.rest))
54            else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
55          }
56        }
57      }
58
59    def atom(s: String, pred: Elem => Boolean): Parser[String] =
60      token(s, pred) ^^ (_.content)
61
62    def command(name: String): Parser[String] = atom("command " + quote(name), _.is_command(name))
63    def $$$(name: String): Parser[String] = atom("keyword " + quote(name), _.is_keyword(name))
64    def string: Parser[String] = atom("string", _.is_string)
65    def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
66    def name: Parser[String] = atom("name", _.is_name)
67    def embedded: Parser[String] = atom("embedded content", _.is_embedded)
68    def text: Parser[String] = atom("text", _.is_text)
69    def ML_source: Parser[String] = atom("ML source", _.is_text)
70    def document_source: Parser[String] = atom("document source", _.is_text)
71
72    def path: Parser[String] =
73      atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
74
75    def session_name: Parser[String] = atom("session name", _.is_system_name)
76    def theory_name: Parser[String] = atom("theory name", _.is_system_name)
77
78    private def tag_name: Parser[String] =
79      atom("tag name", tok =>
80          tok.kind == Token.Kind.IDENT ||
81          tok.kind == Token.Kind.STRING)
82
83    def tags: Parser[List[String]] = rep($$$("%") ~> tag_name)
84
85
86    /* wrappers */
87
88    def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
89
90    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] =
91    {
92      val result = parse(p, in)
93      val rest = proper(result.next)
94      if (result.successful && !rest.atEnd) Error("bad input", rest)
95      else result
96    }
97  }
98}
99
100