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