author | wenzelm |
Tue, 11 May 2021 20:19:07 +0200 | |
changeset 73675 | 6c56f2ebe157 |
parent 73359 | d8a0e996614b |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
36947 | 1 |
/* Title: Pure/Isar/keyword.scala |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
3 |
|
58900 | 4 |
Isar keyword classification. |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
6 |
|
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
8 |
|
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
9 |
|
36947 | 10 |
object Keyword |
32450 | 11 |
{ |
58900 | 12 |
/** keyword classification **/ |
13 |
||
36681 | 14 |
/* kinds */ |
15 |
||
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
16 |
val DIAG = "diag" |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
17 |
val DOCUMENT_HEADING = "document_heading" |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
18 |
val DOCUMENT_BODY = "document_body" |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
19 |
val DOCUMENT_RAW = "document_raw" |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
20 |
val THY_BEGIN = "thy_begin" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
21 |
val THY_END = "thy_end" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
22 |
val THY_DECL = "thy_decl" |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
57837
diff
changeset
|
23 |
val THY_DECL_BLOCK = "thy_decl_block" |
69913 | 24 |
val THY_DEFN = "thy_defn" |
25 |
val THY_STMT = "thy_stmt" |
|
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
46969
diff
changeset
|
26 |
val THY_LOAD = "thy_load" |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
27 |
val THY_GOAL = "thy_goal" |
69913 | 28 |
val THY_GOAL_DEFN = "thy_goal_defn" |
29 |
val THY_GOAL_STMT = "thy_goal_stmt" |
|
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
30 |
val QED = "qed" |
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
31 |
val QED_SCRIPT = "qed_script" |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
32 |
val QED_BLOCK = "qed_block" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
33 |
val QED_GLOBAL = "qed_global" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
34 |
val PRF_GOAL = "prf_goal" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
35 |
val PRF_BLOCK = "prf_block" |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
36 |
val NEXT_BLOCK = "next_block" |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
37 |
val PRF_OPEN = "prf_open" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
38 |
val PRF_CLOSE = "prf_close" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
39 |
val PRF_CHAIN = "prf_chain" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
40 |
val PRF_DECL = "prf_decl" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
41 |
val PRF_ASM = "prf_asm" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
42 |
val PRF_ASM_GOAL = "prf_asm_goal" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
43 |
val PRF_SCRIPT = "prf_script" |
60624 | 44 |
val PRF_SCRIPT_GOAL = "prf_script_goal" |
45 |
val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal" |
|
63441 | 46 |
|
47 |
val BEFORE_COMMAND = "before_command" |
|
63430 | 48 |
val QUASI_COMMAND = "quasi_command" |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
49 |
|
36681 | 50 |
|
59700 | 51 |
/* command categories */ |
36681 | 52 |
|
70123 | 53 |
val vacuous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
54 |
|
57835 | 55 |
val diag = Set(DIAG) |
56 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
57 |
val document_heading = Set(DOCUMENT_HEADING) |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
58 |
val document_body = Set(DOCUMENT_BODY) |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
59 |
val document_raw = Set(DOCUMENT_RAW) |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
60 |
val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) |
57835 | 61 |
|
59700 | 62 |
val theory_begin = Set(THY_BEGIN) |
63 |
val theory_end = Set(THY_END) |
|
64 |
||
59701 | 65 |
val theory_load = Set(THY_LOAD) |
66 |
||
69913 | 67 |
val theory = |
68 |
Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT, |
|
69 |
THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT) |
|
57837 | 70 |
|
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
57837
diff
changeset
|
71 |
val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK) |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
57837
diff
changeset
|
72 |
|
69913 | 73 |
val theory_body = |
74 |
Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT, |
|
75 |
THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT) |
|
57835 | 76 |
|
69917 | 77 |
val theory_defn = Set(THY_DEFN, THY_GOAL_DEFN) |
78 |
||
63479 | 79 |
val prf_script = Set(PRF_SCRIPT) |
80 |
||
40456 | 81 |
val proof = |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
82 |
Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN, |
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
83 |
PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, |
60624 | 84 |
PRF_SCRIPT_ASM_GOAL) |
57835 | 85 |
|
86 |
val proof_body = |
|
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
87 |
Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN, |
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
88 |
PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, |
60624 | 89 |
PRF_SCRIPT_ASM_GOAL) |
57835 | 90 |
|
72669 | 91 |
val proof_asm = Set(PRF_ASM, PRF_ASM_GOAL) |
92 |
val improper = Set(QED_SCRIPT, PRF_SCRIPT, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) |
|
93 |
||
69913 | 94 |
val theory_goal = Set(THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT) |
60624 | 95 |
val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) |
57835 | 96 |
val qed = Set(QED, QED_SCRIPT, QED_BLOCK) |
97 |
val qed_global = Set(QED_GLOBAL) |
|
58900 | 98 |
|
60692 | 99 |
val proof_open = proof_goal + PRF_OPEN |
100 |
val proof_close = qed + PRF_CLOSE |
|
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63424
diff
changeset
|
101 |
val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE) |
60692 | 102 |
|
63603 | 103 |
val close_structure = Set(NEXT_BLOCK, QED_BLOCK, PRF_CLOSE, THY_END) |
104 |
||
58900 | 105 |
|
106 |
||
107 |
/** keyword tables **/ |
|
108 |
||
72764 | 109 |
sealed case class Spec( |
110 |
kind: String = "", |
|
72765 | 111 |
kind_pos: Position.T = Position.none, |
72764 | 112 |
load_command: String = "", |
72765 | 113 |
load_command_pos: Position.T = Position.none, |
72764 | 114 |
tags: List[String] = Nil) |
65384 | 115 |
{ |
65385 | 116 |
override def toString: String = |
117 |
kind + |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
118 |
(if (load_command.isEmpty) "" else " (" + quote(load_command) + ")") + |
65385 | 119 |
(if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", "")) |
72764 | 120 |
|
121 |
def map(f: String => String): Spec = |
|
122 |
copy(kind = f(kind), load_command = f(load_command), tags = tags.map(f)) |
|
65384 | 123 |
} |
63429 | 124 |
|
58900 | 125 |
object Keywords |
126 |
{ |
|
127 |
def empty: Keywords = new Keywords() |
|
128 |
} |
|
129 |
||
130 |
class Keywords private( |
|
63441 | 131 |
val kinds: Map[String, String] = Map.empty, |
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
132 |
val load_commands: Map[String, String] = Map.empty) |
58900 | 133 |
{ |
58901 | 134 |
override def toString: String = |
135 |
{ |
|
63441 | 136 |
val entries = |
137 |
for ((name, kind) <- kinds.toList.sortBy(_._1)) yield { |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
138 |
val load_decl = |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
139 |
load_commands.get(name) match { |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
140 |
case Some(load_command) => " (" + quote(load_command) + ")" |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
141 |
case None => "" |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
142 |
} |
63441 | 143 |
val kind_decl = |
144 |
if (kind == "") "" |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
145 |
else " :: " + quote(kind) + load_decl |
63441 | 146 |
quote(name) + kind_decl |
63430 | 147 |
} |
63441 | 148 |
entries.mkString("keywords\n ", " and\n ", "") |
58900 | 149 |
} |
150 |
||
151 |
||
59073 | 152 |
/* merge */ |
153 |
||
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
154 |
def is_empty: Boolean = kinds.isEmpty |
59073 | 155 |
|
156 |
def ++ (other: Keywords): Keywords = |
|
157 |
if (this eq other) this |
|
158 |
else if (is_empty) other |
|
159 |
else { |
|
63441 | 160 |
val kinds1 = |
161 |
if (kinds eq other.kinds) kinds |
|
162 |
else if (kinds.isEmpty) other.kinds |
|
73359 | 163 |
else other.kinds.foldLeft(kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } |
63441 | 164 |
val load_commands1 = |
165 |
if (load_commands eq other.load_commands) load_commands |
|
166 |
else if (load_commands.isEmpty) other.load_commands |
|
73359 | 167 |
else { |
168 |
other.load_commands.foldLeft(load_commands) { |
|
169 |
case (m, e) => if (m.isDefinedAt(e._1)) m else m + e |
|
170 |
} |
|
171 |
} |
|
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
172 |
new Keywords(kinds1, load_commands1) |
59073 | 173 |
} |
174 |
||
175 |
||
58902 | 176 |
/* add keywords */ |
177 |
||
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
178 |
def + (name: String, kind: String = "", load_command: String = ""): Keywords = |
63441 | 179 |
{ |
180 |
val kinds1 = kinds + (name -> kind) |
|
181 |
val load_commands1 = |
|
66919 | 182 |
if (kind == THY_LOAD) { |
71601 | 183 |
if (!Symbol.iterator(name).forall(Symbol.is_ascii)) |
66919 | 184 |
error("Bad theory load command " + quote(name)) |
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
185 |
load_commands + (name -> load_command) |
66919 | 186 |
} |
63441 | 187 |
else load_commands |
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
188 |
new Keywords(kinds1, load_commands1) |
63441 | 189 |
} |
58902 | 190 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
191 |
def add_keywords(header: Thy_Header.Keywords): Keywords = |
73359 | 192 |
header.foldLeft(this) { |
65384 | 193 |
case (keywords, (name, spec)) => |
72764 | 194 |
if (spec.kind.isEmpty) |
65384 | 195 |
keywords + Symbol.decode(name) + Symbol.encode(name) |
196 |
else |
|
197 |
keywords + |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
198 |
(Symbol.decode(name), spec.kind, spec.load_command) + |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
199 |
(Symbol.encode(name), spec.kind, spec.load_command) |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
200 |
} |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
201 |
|
58902 | 202 |
|
58901 | 203 |
/* command kind */ |
58900 | 204 |
|
63424 | 205 |
def is_command(token: Token, check_kind: String => Boolean): Boolean = |
206 |
token.is_command && |
|
63441 | 207 |
(kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false }) |
208 |
||
209 |
def is_before_command(token: Token): Boolean = |
|
210 |
token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND) |
|
59701 | 211 |
|
63430 | 212 |
def is_quasi_command(token: Token): Boolean = |
63441 | 213 |
token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND) |
63430 | 214 |
|
63809 | 215 |
def is_indent_command(token: Token): Boolean = |
216 |
token.is_begin_or_command || is_quasi_command(token) |
|
217 |
||
58900 | 218 |
|
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
219 |
/* lexicons */ |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
220 |
|
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
221 |
private def make_lexicon(is_minor: Boolean): Scan.Lexicon = |
73359 | 222 |
kinds.foldLeft(Scan.Lexicon.empty) { |
223 |
case (lex, (name, kind)) => |
|
224 |
if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor) |
|
225 |
lex + name |
|
226 |
else lex |
|
227 |
} |
|
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
228 |
|
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
229 |
lazy val minor: Scan.Lexicon = make_lexicon(true) |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
230 |
lazy val major: Scan.Lexicon = make_lexicon(false) |
58900 | 231 |
} |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
232 |
} |