author | wenzelm |
Fri, 25 Sep 2015 19:13:47 +0200 | |
changeset 61262 | 7bd1eb4b056e |
parent 59693 | d96cb03caf9e |
child 62965 | 5bf08c9aa036 |
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 |
|
59692 | 62 |
def command(name: String): Parser[String] = |
63 |
atom("command " + quote(name), tok => tok.is_command && tok.source == name) |
|
48718 | 64 |
|
58908 | 65 |
def $$$(name: String): Parser[String] = |
48718 | 66 |
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
|
67 |
|
46943 | 68 |
def string: Parser[String] = atom("string", _.is_string) |
48349
a78e5d399599
support Session.Queue with ordering and dependencies;
wenzelm
parents:
46943
diff
changeset
|
69 |
def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s)) |
34168 | 70 |
def name: Parser[String] = atom("name declaration", _.is_name) |
71 |
def xname: Parser[String] = atom("name reference", _.is_xname) |
|
72 |
def text: Parser[String] = atom("text", _.is_text) |
|
73 |
def ML_source: Parser[String] = atom("ML source", _.is_text) |
|
51627
589daaf48dba
tuned signature -- agree with markup terminology;
wenzelm
parents:
48912
diff
changeset
|
74 |
def document_source: Parser[String] = atom("document source", _.is_text) |
59693 | 75 |
|
48484 | 76 |
def path: Parser[String] = |
55879
ac979f750c1a
clarified path checks: avoid crash of rendering due to spurious errors;
wenzelm
parents:
55618
diff
changeset
|
77 |
atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content)) |
59693 | 78 |
|
48484 | 79 |
def theory_name: Parser[String] = |
56209 | 80 |
atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content)) |
56801
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56464
diff
changeset
|
81 |
def theory_xname: Parser[String] = |
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56464
diff
changeset
|
82 |
atom("theory name reference", tok => tok.is_xname && Path.is_wellformed(tok.content)) |
34168 | 83 |
|
84 |
private def tag_name: Parser[String] = |
|
85 |
atom("tag name", tok => |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
86 |
tok.kind == Token.Kind.IDENT || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
87 |
tok.kind == Token.Kind.STRING) |
34168 | 88 |
|
58908 | 89 |
def tags: Parser[List[String]] = rep($$$("%") ~> tag_name) |
34161 | 90 |
|
91 |
||
92 |
/* wrappers */ |
|
93 |
||
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
94 |
def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in) |
48912 | 95 |
|
48600
305ebcd9018a
proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;
wenzelm
parents:
48599
diff
changeset
|
96 |
def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = |
48912 | 97 |
{ |
98 |
val result = parse(p, in) |
|
99 |
val rest = proper(result.next) |
|
100 |
if (result.successful && !rest.atEnd) Error("bad input", rest) |
|
101 |
else result |
|
102 |
} |
|
34159
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
103 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
104 |
} |
903092d61519
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm
parents:
diff
changeset
|
105 |