wenzelm@44163
|
1 |
/* Title: Pure/Isar/parse.scala
|
wenzelm@34166
|
2 |
Author: Makarius
|
wenzelm@34166
|
3 |
|
wenzelm@34166
|
4 |
Generic parsers for Isabelle/Isar outer syntax.
|
wenzelm@34166
|
5 |
*/
|
wenzelm@34166
|
6 |
|
wenzelm@34166
|
7 |
package isabelle
|
wenzelm@34166
|
8 |
|
wenzelm@34166
|
9 |
import scala.util.parsing.combinator.Parsers
|
wenzelm@34166
|
10 |
|
wenzelm@34166
|
11 |
|
wenzelm@36948
|
12 |
object Parse
|
wenzelm@34166
|
13 |
{
|
wenzelm@34168
|
14 |
/* parsing tokens */
|
wenzelm@34168
|
15 |
|
wenzelm@34166
|
16 |
trait Parser extends Parsers
|
wenzelm@34166
|
17 |
{
|
wenzelm@36966
|
18 |
type Elem = Token
|
wenzelm@34166
|
19 |
|
wenzelm@34271
|
20 |
def filter_proper = true
|
wenzelm@34271
|
21 |
|
wenzelm@34168
|
22 |
private def proper(in: Input): Input =
|
wenzelm@34314
|
23 |
if (in.atEnd || !in.first.is_ignored || !filter_proper) in
|
wenzelm@34168
|
24 |
else proper(in.rest)
|
wenzelm@34166
|
25 |
|
wenzelm@34166
|
26 |
def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
|
wenzelm@34166
|
27 |
{
|
wenzelm@34168
|
28 |
def apply(raw_input: Input) =
|
wenzelm@34166
|
29 |
{
|
wenzelm@34168
|
30 |
val in = proper(raw_input)
|
wenzelm@34166
|
31 |
if (in.atEnd) Failure(s + " expected (past end-of-file!)", in)
|
wenzelm@34166
|
32 |
else {
|
wenzelm@34166
|
33 |
val token = in.first
|
wenzelm@34168
|
34 |
if (pred(token)) Success(token, proper(in.rest))
|
wenzelm@34166
|
35 |
else
|
wenzelm@34166
|
36 |
token.text match {
|
wenzelm@34166
|
37 |
case (txt, "") =>
|
wenzelm@34166
|
38 |
Failure(s + " expected,\nbut " + txt + " was found", in)
|
wenzelm@34166
|
39 |
case (txt1, txt2) =>
|
wenzelm@34166
|
40 |
Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
|
wenzelm@34166
|
41 |
}
|
wenzelm@34166
|
42 |
}
|
wenzelm@34166
|
43 |
}
|
wenzelm@34166
|
44 |
}
|
wenzelm@34166
|
45 |
|
wenzelm@34271
|
46 |
def not_eof: Parser[Elem] = token("input token", _ => true)
|
wenzelm@34271
|
47 |
def eof: Parser[Unit] = not(not_eof)
|
wenzelm@34271
|
48 |
|
wenzelm@34175
|
49 |
def atom(s: String, pred: Elem => Boolean): Parser[String] =
|
wenzelm@34175
|
50 |
token(s, pred) ^^ (_.content)
|
wenzelm@34175
|
51 |
|
wenzelm@34175
|
52 |
def keyword(name: String): Parser[String] =
|
wenzelm@36966
|
53 |
atom(Token.Kind.KEYWORD.toString + " \"" + name + "\"",
|
wenzelm@36966
|
54 |
tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
|
wenzelm@34166
|
55 |
|
wenzelm@34175
|
56 |
def name: Parser[String] = atom("name declaration", _.is_name)
|
wenzelm@34175
|
57 |
def xname: Parser[String] = atom("name reference", _.is_xname)
|
wenzelm@34175
|
58 |
def text: Parser[String] = atom("text", _.is_text)
|
wenzelm@34175
|
59 |
def ML_source: Parser[String] = atom("ML source", _.is_text)
|
wenzelm@34175
|
60 |
def doc_source: Parser[String] = atom("document source", _.is_text)
|
wenzelm@34175
|
61 |
def path: Parser[String] = atom("file name/path specification", _.is_name)
|
wenzelm@34175
|
62 |
|
wenzelm@34175
|
63 |
private def tag_name: Parser[String] =
|
wenzelm@34175
|
64 |
atom("tag name", tok =>
|
wenzelm@36966
|
65 |
tok.kind == Token.Kind.IDENT ||
|
wenzelm@36966
|
66 |
tok.kind == Token.Kind.STRING)
|
wenzelm@34175
|
67 |
|
wenzelm@34175
|
68 |
def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
|
wenzelm@34168
|
69 |
|
wenzelm@34168
|
70 |
|
wenzelm@34168
|
71 |
/* wrappers */
|
wenzelm@34168
|
72 |
|
wenzelm@36966
|
73 |
def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
|
wenzelm@36966
|
74 |
def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = parse(phrase(p), in)
|
wenzelm@34166
|
75 |
}
|
wenzelm@34166
|
76 |
}
|
wenzelm@34166
|
77 |
|