author | haftmann |
Wed, 11 Aug 2010 08:58:18 +0200 | |
changeset 38338 | 0e0e1fd9cc03 |
parent 36956 | 21be4832c362 |
child 38367 | f7d2574dc3a6 |
permissions | -rw-r--r-- |
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
1 |
/* Title: Pure/Isar/token.scala |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
3 |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
4 |
Outer token syntax for Isabelle/Isar. |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
5 |
*/ |
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
6 |
|
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
8 |
|
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
9 |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
10 |
object Token |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
11 |
{ |
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
12 |
/* tokens */ |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
13 |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
14 |
object Kind extends Enumeration |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
15 |
{ |
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
16 |
val COMMAND = Value("command") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
17 |
val KEYWORD = Value("keyword") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
18 |
val IDENT = Value("identifier") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
19 |
val LONG_IDENT = Value("long identifier") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
20 |
val SYM_IDENT = Value("symbolic identifier") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
21 |
val VAR = Value("schematic variable") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
22 |
val TYPE_IDENT = Value("type variable") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
23 |
val TYPE_VAR = Value("schematic type variable") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
24 |
val NAT = Value("number") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
25 |
val STRING = Value("string") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
26 |
val ALT_STRING = Value("back-quoted string") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
27 |
val VERBATIM = Value("verbatim text") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
28 |
val SPACE = Value("white space") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
29 |
val COMMENT = Value("comment text") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
30 |
val BAD_INPUT = Value("bad input") |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
31 |
val UNPARSED = Value("unparsed input") |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
32 |
} |
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
33 |
|
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
34 |
|
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
35 |
/* token reader */ |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
36 |
|
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
37 |
class Line_Position(val line: Int) extends scala.util.parsing.input.Position |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
38 |
{ |
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
39 |
def column = 0 |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
40 |
def lineContents = "" |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
41 |
override def toString = line.toString |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
42 |
|
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
43 |
def advance(token: Token): Line_Position = |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
44 |
{ |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
45 |
var n = 0 |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
46 |
for (c <- token.content if c == '\n') n += 1 |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
47 |
if (n == 0) this else new Line_Position(line + n) |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
48 |
} |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
49 |
} |
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
50 |
|
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
51 |
abstract class Reader extends scala.util.parsing.input.Reader[Token] |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
52 |
|
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
53 |
private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
54 |
{ |
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
55 |
def first = tokens.head |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
56 |
def rest = new Token_Reader(tokens.tail, pos.advance(first)) |
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
57 |
def atEnd = tokens.isEmpty |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
58 |
} |
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
59 |
|
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset
|
60 |
def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1)) |
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
61 |
} |
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm
parents:
diff
changeset
|
62 |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
63 |
|
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
64 |
sealed case class Token(val kind: Token.Kind.Value, val source: String) |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
65 |
{ |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
66 |
def is_command: Boolean = kind == Token.Kind.COMMAND |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
67 |
def is_delimited: Boolean = |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
68 |
kind == Token.Kind.STRING || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
69 |
kind == Token.Kind.ALT_STRING || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
70 |
kind == Token.Kind.VERBATIM || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
71 |
kind == Token.Kind.COMMENT |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
72 |
def is_name: Boolean = |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
73 |
kind == Token.Kind.IDENT || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
74 |
kind == Token.Kind.SYM_IDENT || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
75 |
kind == Token.Kind.STRING || |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
76 |
kind == Token.Kind.NAT |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
77 |
def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
78 |
def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
79 |
def is_space: Boolean = kind == Token.Kind.SPACE |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
80 |
def is_comment: Boolean = kind == Token.Kind.COMMENT |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
81 |
def is_ignored: Boolean = is_space || is_comment |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
82 |
def is_unparsed: Boolean = kind == Token.Kind.UNPARSED |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
83 |
|
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
84 |
def content: String = |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
85 |
if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source) |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
86 |
else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source) |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
87 |
else if (kind == Token.Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source) |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
88 |
else if (kind == Token.Kind.COMMENT) Scan.Lexicon.empty.comment_content(source) |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
89 |
else source |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
90 |
|
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
91 |
def text: (String, String) = |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
92 |
if (kind == Token.Kind.COMMAND && source == ";") ("terminator", "") |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
93 |
else (kind.toString, source) |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
94 |
} |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset
|
95 |