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