author | haftmann |
Sat, 20 Aug 2011 01:21:22 +0200 | |
changeset 44323 | 4b5b430eb00e |
parent 44181 | bbce0417236d |
child 46943 | ac1c41ea856d |
permissions | -rw-r--r-- |
43283 | 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 | 12 |
object Parse |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
13 |
{ |
34161 | 14 |
/* parsing tokens */ |
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 | 20 |
def filter_proper = true |
21 |
||
34161 | 22 |
private def proper(in: Input): Input = |
34311 | 23 |
if (in.atEnd || !in.first.is_ignored || !filter_proper) in |
34161 | 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 | 28 |
def apply(raw_input: Input) = |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
29 |
{ |
34161 | 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 | 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 | 46 |
def not_eof: Parser[Elem] = token("input token", _ => true) |
47 |
def eof: Parser[Unit] = not(not_eof) |
|
48 |
||
34168 | 49 |
def atom(s: String, pred: Elem => Boolean): Parser[String] = |
50 |
token(s, pred) ^^ (_.content) |
|
51 |
||
52 |
def keyword(name: String): Parser[String] = |
|
44181 | 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 |
|
34168 | 56 |
def name: Parser[String] = atom("name declaration", _.is_name) |
57 |
def xname: Parser[String] = atom("name reference", _.is_xname) |
|
58 |
def text: Parser[String] = atom("text", _.is_text) |
|
59 |
def ML_source: Parser[String] = atom("ML source", _.is_text) |
|
60 |
def doc_source: Parser[String] = atom("document source", _.is_text) |
|
61 |
def path: Parser[String] = atom("file name/path specification", _.is_name) |
|
62 |
||
63 |
private def tag_name: Parser[String] = |
|
64 |
atom("tag name", tok => |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
65 |
tok.kind == Token.Kind.IDENT || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
66 |
tok.kind == Token.Kind.STRING) |
34168 | 67 |
|
68 |
def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name) |
|
34161 | 69 |
|
70 |
||
71 |
/* wrappers */ |
|
72 |
||
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
73 |
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
|
74 |
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
|
75 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
76 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
77 |