author | wenzelm |
Fri, 05 Apr 2013 20:54:55 +0200 | |
changeset 51627 | 589daaf48dba |
parent 48912 | ffdb37019b2f |
child 55618 | 995162143ef4 |
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 |
48599 | 10 |
import scala.annotation.tailrec |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
11 |
|
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
12 |
|
36948 | 13 |
object Parse |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
14 |
{ |
34161 | 15 |
/* parsing tokens */ |
16 |
||
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
17 |
trait Parser extends Parsers |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
18 |
{ |
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
19 |
type Elem = Token |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
20 |
|
48599 | 21 |
def filter_proper: Boolean = true |
34266 | 22 |
|
48599 | 23 |
@tailrec private def proper(in: Input): Input = |
24 |
if (!filter_proper || in.atEnd || in.first.is_proper) in |
|
34161 | 25 |
else proper(in.rest) |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
26 |
|
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
27 |
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
|
28 |
{ |
34161 | 29 |
def apply(raw_input: Input) = |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
30 |
{ |
34161 | 31 |
val in = proper(raw_input) |
48911
5debc3e4fa81
tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents:
48718
diff
changeset
|
32 |
if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in) |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
33 |
else { |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
34 |
val token = in.first |
34161 | 35 |
if (pred(token)) Success(token, proper(in.rest)) |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
36 |
else |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
37 |
token.text match { |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
38 |
case (txt, "") => |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
39 |
Failure(s + " expected,\nbut " + txt + " was found", in) |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
40 |
case (txt1, txt2) => |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
41 |
Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in) |
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 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
46 |
|
34168 | 47 |
def atom(s: String, pred: Elem => Boolean): Parser[String] = |
48 |
token(s, pred) ^^ (_.content) |
|
49 |
||
48718 | 50 |
def command(name: String): Parser[String] = |
51 |
atom("command " + quote(name), tok => tok.is_command && tok.source == name) |
|
52 |
||
34168 | 53 |
def keyword(name: String): Parser[String] = |
48718 | 54 |
atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name) |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
55 |
|
46943 | 56 |
def string: Parser[String] = atom("string", _.is_string) |
48349
a78e5d399599
support Session.Queue with ordering and dependencies;
wenzelm
parents:
46943
diff
changeset
|
57 |
def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s)) |
34168 | 58 |
def name: Parser[String] = atom("name declaration", _.is_name) |
59 |
def xname: Parser[String] = atom("name reference", _.is_xname) |
|
60 |
def text: Parser[String] = atom("text", _.is_text) |
|
61 |
def ML_source: Parser[String] = atom("ML source", _.is_text) |
|
51627
589daaf48dba
tuned signature -- agree with markup terminology;
wenzelm
parents:
48912
diff
changeset
|
62 |
def document_source: Parser[String] = atom("document source", _.is_text) |
48484 | 63 |
def path: Parser[String] = |
64 |
atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content)) |
|
65 |
def theory_name: Parser[String] = |
|
66 |
atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content)) |
|
34168 | 67 |
|
68 |
private def tag_name: Parser[String] = |
|
69 |
atom("tag name", tok => |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
70 |
tok.kind == Token.Kind.IDENT || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
71 |
tok.kind == Token.Kind.STRING) |
34168 | 72 |
|
73 |
def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name) |
|
34161 | 74 |
|
75 |
||
76 |
/* wrappers */ |
|
77 |
||
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
78 |
def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in) |
48912 | 79 |
|
48600
305ebcd9018a
proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;
wenzelm
parents:
48599
diff
changeset
|
80 |
def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = |
48912 | 81 |
{ |
82 |
val result = parse(p, in) |
|
83 |
val rest = proper(result.next) |
|
84 |
if (result.successful && !rest.atEnd) Error("bad input", rest) |
|
85 |
else result |
|
86 |
} |
|
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
87 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
88 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
89 |