author | wenzelm |
Tue, 17 Oct 2017 13:51:43 +0200 | |
changeset 66877 | 4f0ccfe1bcb6 |
parent 64471 | c40c2975fb02 |
child 66914 | fb3f13a9c756 |
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 |
|
59692 | 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] { |
|
56464 | 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 |
|
59692 | 53 |
if (pred(token)) Success(token, proper(in.rest)) |
58861
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
56801
diff
changeset
|
54 |
else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in) |
56464 | 55 |
} |
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
56 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
57 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
58 |
|
34168 | 59 |
def atom(s: String, pred: Elem => Boolean): Parser[String] = |
59692 | 60 |
token(s, pred) ^^ (_.content) |
34168 | 61 |
|
63446 | 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)) |
|
46943 | 64 |
def string: Parser[String] = atom("string", _.is_string) |
48349
a78e5d399599
support Session.Queue with ordering and dependencies;
wenzelm
parents:
46943
diff
changeset
|
65 |
def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s)) |
62969 | 66 |
def name: Parser[String] = atom("name", _.is_name) |
64471
c40c2975fb02
more uniform path syntax, as in ML (see 5a7c919a4ada);
wenzelm
parents:
63446
diff
changeset
|
67 |
def embedded: Parser[String] = atom("embedded content", _.is_embedded) |
34168 | 68 |
def text: Parser[String] = atom("text", _.is_text) |
69 |
def ML_source: Parser[String] = atom("ML source", _.is_text) |
|
51627
589daaf48dba
tuned signature -- agree with markup terminology;
wenzelm
parents:
48912
diff
changeset
|
70 |
def document_source: Parser[String] = atom("document source", _.is_text) |
59693 | 71 |
|
48484 | 72 |
def path: Parser[String] = |
64471
c40c2975fb02
more uniform path syntax, as in ML (see 5a7c919a4ada);
wenzelm
parents:
63446
diff
changeset
|
73 |
atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content)) |
59693 | 74 |
|
48484 | 75 |
def theory_name: Parser[String] = |
56209 | 76 |
atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content)) |
34168 | 77 |
|
78 |
private def tag_name: Parser[String] = |
|
79 |
atom("tag name", tok => |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
80 |
tok.kind == Token.Kind.IDENT || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
81 |
tok.kind == Token.Kind.STRING) |
34168 | 82 |
|
58908 | 83 |
def tags: Parser[List[String]] = rep($$$("%") ~> tag_name) |
34161 | 84 |
|
85 |
||
86 |
/* wrappers */ |
|
87 |
||
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
88 |
def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in) |
48912 | 89 |
|
48600
305ebcd9018a
proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;
wenzelm
parents:
48599
diff
changeset
|
90 |
def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = |
48912 | 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 |
} |
|
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
97 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
98 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
99 |