|
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 sealed abstract class Token |
|
13 { |
|
14 def source: String |
|
15 def content: String = source |
|
16 |
|
17 def is_delimited: Boolean = false |
|
18 def is_name: Boolean = false |
|
19 def is_xname: Boolean = false |
|
20 def is_text: Boolean = false |
|
21 def is_space: Boolean = false |
|
22 def is_comment: Boolean = false |
|
23 def is_proper: Boolean = !(is_space || is_comment) |
|
24 } |
|
25 |
|
26 case class Command(val source: String) extends Token |
|
27 |
|
28 case class Keyword(val source: String) extends Token |
|
29 |
|
30 case class Ident(val source: String) extends Token |
|
31 { |
|
32 override def is_name = true |
|
33 override def is_xname = true |
|
34 override def is_text = true |
|
35 } |
|
36 |
|
37 case class Long_Ident(val source: String) extends Token |
|
38 { |
|
39 override def is_xname = true |
|
40 override def is_text = true |
|
41 } |
|
42 |
|
43 case class Sym_Ident(val source: String) extends Token |
|
44 { |
|
45 override def is_name = true |
|
46 override def is_xname = true |
|
47 override def is_text = true |
|
48 } |
|
49 |
|
50 case class Var(val source: String) extends Token |
|
51 |
|
52 case class Type_Ident(val source: String) extends Token |
|
53 |
|
54 case class Type_Var(val source: String) extends Token |
|
55 |
|
56 case class Nat(val source: String) extends Token |
|
57 { |
|
58 override def is_name = true |
|
59 override def is_xname = true |
|
60 override def is_text = true |
|
61 } |
|
62 |
|
63 case class String_Token(val source: String) extends Token |
|
64 { |
|
65 override def content = Scan.Lexicon.empty.quoted_content("\"", source) |
|
66 override def is_delimited = true |
|
67 override def is_name = true |
|
68 override def is_xname = true |
|
69 override def is_text = true |
|
70 } |
|
71 |
|
72 case class Alt_String_Token(val source: String) extends Token |
|
73 { |
|
74 override def content = Scan.Lexicon.empty.quoted_content("`", source) |
|
75 override def is_delimited = true |
|
76 } |
|
77 |
|
78 case class Verbatim(val source: String) extends Token |
|
79 { |
|
80 override def content = Scan.Lexicon.empty.verbatim_content(source) |
|
81 override def is_delimited = true |
|
82 override def is_text = true |
|
83 } |
|
84 |
|
85 case class Space(val source: String) extends Token |
|
86 { |
|
87 override def is_space = true |
|
88 } |
|
89 |
|
90 case class Comment(val source: String) extends Token |
|
91 { |
|
92 override def is_delimited = true |
|
93 override def is_comment = true |
|
94 } |
|
95 |
|
96 case class Bad_Input(val source: String) extends Token |
|
97 case class Unparsed(val source: String) extends Token |
|
98 } |
|
99 |