author | wenzelm |
Mon, 17 May 2010 14:23:54 +0200 | |
changeset 36956 | 21be4832c362 |
parent 36948 | d2cdad45fd14 |
child 38239 | 89a4d1028fb3 |
permissions | -rw-r--r-- |
34268 | 1 |
/* Title: Pure/Thy/thy_syntax.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Superficial theory syntax: command spans. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
34303 | 10 |
object Thy_Syntax |
34268 | 11 |
{ |
36948 | 12 |
private val parser = new Parse.Parser |
34268 | 13 |
{ |
14 |
override def filter_proper = false |
|
15 |
||
16 |
val command_span: Parser[Span] = |
|
17 |
{ |
|
34311 | 18 |
val whitespace = token("white space", _.is_ignored) |
34268 | 19 |
val command = token("command keyword", _.is_command) |
20 |
val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof |
|
21 |
command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body) |
|
22 |
} |
|
23 |
} |
|
24 |
||
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
25 |
type Span = List[Token] |
34268 | 26 |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
27 |
def parse_spans(toks: List[Token]): List[Span] = |
34268 | 28 |
{ |
29 |
import parser._ |
|
30 |
||
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36948
diff
changeset
|
31 |
parse(rep(command_span), Token.reader(toks)) match { |
34268 | 32 |
case Success(spans, rest) if rest.atEnd => spans |
33 |
case bad => error(bad.toString) |
|
34 |
} |
|
35 |
} |
|
36 |
} |