author | wenzelm |
Sat, 28 Nov 2020 22:20:48 +0100 | |
changeset 72764 | 722c0d02ffab |
parent 72748 | 04d5f6d769a7 |
child 72765 | f34f5c057c9e |
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 = "", |
|
111 |
load_command: String = "", |
|
112 |
tags: List[String] = Nil) |
|
65384 | 113 |
{ |
65385 | 114 |
override def toString: String = |
115 |
kind + |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
116 |
(if (load_command.isEmpty) "" else " (" + quote(load_command) + ")") + |
65385 | 117 |
(if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", "")) |
72764 | 118 |
|
119 |
def map(f: String => String): Spec = |
|
120 |
copy(kind = f(kind), load_command = f(load_command), tags = tags.map(f)) |
|
65384 | 121 |
} |
63429 | 122 |
|
58900 | 123 |
object Keywords |
124 |
{ |
|
125 |
def empty: Keywords = new Keywords() |
|
126 |
} |
|
127 |
||
128 |
class Keywords private( |
|
63441 | 129 |
val kinds: Map[String, String] = Map.empty, |
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
130 |
val load_commands: Map[String, String] = Map.empty) |
58900 | 131 |
{ |
58901 | 132 |
override def toString: String = |
133 |
{ |
|
63441 | 134 |
val entries = |
135 |
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
|
136 |
val load_decl = |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
137 |
load_commands.get(name) match { |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
138 |
case Some(load_command) => " (" + quote(load_command) + ")" |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
139 |
case None => "" |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
140 |
} |
63441 | 141 |
val kind_decl = |
142 |
if (kind == "") "" |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
143 |
else " :: " + quote(kind) + load_decl |
63441 | 144 |
quote(name) + kind_decl |
63430 | 145 |
} |
63441 | 146 |
entries.mkString("keywords\n ", " and\n ", "") |
58900 | 147 |
} |
148 |
||
149 |
||
59073 | 150 |
/* merge */ |
151 |
||
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
152 |
def is_empty: Boolean = kinds.isEmpty |
59073 | 153 |
|
154 |
def ++ (other: Keywords): Keywords = |
|
155 |
if (this eq other) this |
|
156 |
else if (is_empty) other |
|
157 |
else { |
|
63441 | 158 |
val kinds1 = |
159 |
if (kinds eq other.kinds) kinds |
|
160 |
else if (kinds.isEmpty) other.kinds |
|
161 |
else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } |
|
162 |
val load_commands1 = |
|
163 |
if (load_commands eq other.load_commands) load_commands |
|
164 |
else if (load_commands.isEmpty) other.load_commands |
|
165 |
else |
|
166 |
(load_commands /: other.load_commands) { |
|
167 |
case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } |
|
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
168 |
new Keywords(kinds1, load_commands1) |
59073 | 169 |
} |
170 |
||
171 |
||
58902 | 172 |
/* add keywords */ |
173 |
||
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
174 |
def + (name: String, kind: String = "", load_command: String = ""): Keywords = |
63441 | 175 |
{ |
176 |
val kinds1 = kinds + (name -> kind) |
|
177 |
val load_commands1 = |
|
66919 | 178 |
if (kind == THY_LOAD) { |
71601 | 179 |
if (!Symbol.iterator(name).forall(Symbol.is_ascii)) |
66919 | 180 |
error("Bad theory load command " + quote(name)) |
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
181 |
load_commands + (name -> load_command) |
66919 | 182 |
} |
63441 | 183 |
else load_commands |
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
184 |
new Keywords(kinds1, load_commands1) |
63441 | 185 |
} |
58902 | 186 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
187 |
def add_keywords(header: Thy_Header.Keywords): Keywords = |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
188 |
(this /: header) { |
65384 | 189 |
case (keywords, (name, spec)) => |
72764 | 190 |
if (spec.kind.isEmpty) |
65384 | 191 |
keywords + Symbol.decode(name) + Symbol.encode(name) |
192 |
else |
|
193 |
keywords + |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
194 |
(Symbol.decode(name), spec.kind, spec.load_command) + |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72740
diff
changeset
|
195 |
(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
|
196 |
} |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
197 |
|
58902 | 198 |
|
58901 | 199 |
/* command kind */ |
58900 | 200 |
|
63424 | 201 |
def is_command(token: Token, check_kind: String => Boolean): Boolean = |
202 |
token.is_command && |
|
63441 | 203 |
(kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false }) |
204 |
||
205 |
def is_before_command(token: Token): Boolean = |
|
206 |
token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND) |
|
59701 | 207 |
|
63430 | 208 |
def is_quasi_command(token: Token): Boolean = |
63441 | 209 |
token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND) |
63430 | 210 |
|
63809 | 211 |
def is_indent_command(token: Token): Boolean = |
212 |
token.is_begin_or_command || is_quasi_command(token) |
|
213 |
||
58900 | 214 |
|
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
215 |
/* lexicons */ |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
216 |
|
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
217 |
private def make_lexicon(is_minor: Boolean): Scan.Lexicon = |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
218 |
(Scan.Lexicon.empty /: kinds)( |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
219 |
{ |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
220 |
case (lex, (name, kind)) => |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
221 |
if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor) |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
222 |
lex + name |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
223 |
else lex |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
224 |
}) |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
225 |
|
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
226 |
lazy val minor: Scan.Lexicon = make_lexicon(true) |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
227 |
lazy val major: Scan.Lexicon = make_lexicon(false) |
58900 | 228 |
} |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
229 |
} |