author | wenzelm |
Thu, 14 Mar 2019 16:55:06 +0100 | |
changeset 69913 | ca515cf61651 |
parent 67090 | 0ec94bb9cec4 |
child 69917 | 66c4567664b5 |
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 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
53 |
val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) |
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 |
|
63479 | 77 |
val prf_script = Set(PRF_SCRIPT) |
78 |
||
40456 | 79 |
val proof = |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
80 |
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
|
81 |
PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, |
60624 | 82 |
PRF_SCRIPT_ASM_GOAL) |
57835 | 83 |
|
84 |
val proof_body = |
|
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
85 |
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
|
86 |
PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, |
60624 | 87 |
PRF_SCRIPT_ASM_GOAL) |
57835 | 88 |
|
69913 | 89 |
val theory_goal = Set(THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT) |
60624 | 90 |
val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) |
57835 | 91 |
val qed = Set(QED, QED_SCRIPT, QED_BLOCK) |
92 |
val qed_global = Set(QED_GLOBAL) |
|
58900 | 93 |
|
60692 | 94 |
val proof_open = proof_goal + PRF_OPEN |
95 |
val proof_close = qed + PRF_CLOSE |
|
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63424
diff
changeset
|
96 |
val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE) |
60692 | 97 |
|
63603 | 98 |
val close_structure = Set(NEXT_BLOCK, QED_BLOCK, PRF_CLOSE, THY_END) |
99 |
||
58900 | 100 |
|
101 |
||
102 |
/** keyword tables **/ |
|
103 |
||
65384 | 104 |
object Spec |
105 |
{ |
|
106 |
val none: Spec = Spec("") |
|
107 |
} |
|
108 |
sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil) |
|
109 |
{ |
|
110 |
def is_none: Boolean = kind == "" |
|
65385 | 111 |
|
112 |
override def toString: String = |
|
113 |
kind + |
|
114 |
(if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") + |
|
115 |
(if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", "")) |
|
65384 | 116 |
} |
63429 | 117 |
|
58900 | 118 |
object Keywords |
119 |
{ |
|
120 |
def empty: Keywords = new Keywords() |
|
121 |
} |
|
122 |
||
123 |
class Keywords private( |
|
63441 | 124 |
val kinds: Map[String, String] = Map.empty, |
125 |
val load_commands: Map[String, List[String]] = Map.empty) |
|
58900 | 126 |
{ |
58901 | 127 |
override def toString: String = |
128 |
{ |
|
63441 | 129 |
val entries = |
130 |
for ((name, kind) <- kinds.toList.sortBy(_._1)) yield { |
|
131 |
val exts = load_commands.getOrElse(name, Nil) |
|
132 |
val kind_decl = |
|
133 |
if (kind == "") "" |
|
134 |
else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") |
|
135 |
quote(name) + kind_decl |
|
63430 | 136 |
} |
63441 | 137 |
entries.mkString("keywords\n ", " and\n ", "") |
58900 | 138 |
} |
139 |
||
140 |
||
59073 | 141 |
/* merge */ |
142 |
||
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
143 |
def is_empty: Boolean = kinds.isEmpty |
59073 | 144 |
|
145 |
def ++ (other: Keywords): Keywords = |
|
146 |
if (this eq other) this |
|
147 |
else if (is_empty) other |
|
148 |
else { |
|
63441 | 149 |
val kinds1 = |
150 |
if (kinds eq other.kinds) kinds |
|
151 |
else if (kinds.isEmpty) other.kinds |
|
152 |
else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } |
|
153 |
val load_commands1 = |
|
154 |
if (load_commands eq other.load_commands) load_commands |
|
155 |
else if (load_commands.isEmpty) other.load_commands |
|
156 |
else |
|
157 |
(load_commands /: other.load_commands) { |
|
158 |
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
|
159 |
new Keywords(kinds1, load_commands1) |
59073 | 160 |
} |
161 |
||
162 |
||
58902 | 163 |
/* add keywords */ |
164 |
||
63441 | 165 |
def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords = |
166 |
{ |
|
167 |
val kinds1 = kinds + (name -> kind) |
|
168 |
val load_commands1 = |
|
66919 | 169 |
if (kind == THY_LOAD) { |
170 |
if (!Symbol.iterator(name).forall(Symbol.is_ascii(_))) |
|
171 |
error("Bad theory load command " + quote(name)) |
|
172 |
load_commands + (name -> exts) |
|
173 |
} |
|
63441 | 174 |
else load_commands |
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
175 |
new Keywords(kinds1, load_commands1) |
63441 | 176 |
} |
58902 | 177 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
178 |
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
|
179 |
(this /: header) { |
65384 | 180 |
case (keywords, (name, spec)) => |
181 |
if (spec.is_none) |
|
182 |
keywords + Symbol.decode(name) + Symbol.encode(name) |
|
183 |
else |
|
184 |
keywords + |
|
185 |
(Symbol.decode(name), spec.kind, spec.exts) + |
|
186 |
(Symbol.encode(name), spec.kind, spec.exts) |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
187 |
} |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
188 |
|
58902 | 189 |
|
58901 | 190 |
/* command kind */ |
58900 | 191 |
|
63424 | 192 |
def is_command(token: Token, check_kind: String => Boolean): Boolean = |
193 |
token.is_command && |
|
63441 | 194 |
(kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false }) |
195 |
||
196 |
def is_before_command(token: Token): Boolean = |
|
197 |
token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND) |
|
59701 | 198 |
|
63430 | 199 |
def is_quasi_command(token: Token): Boolean = |
63441 | 200 |
token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND) |
63430 | 201 |
|
63809 | 202 |
def is_indent_command(token: Token): Boolean = |
203 |
token.is_begin_or_command || is_quasi_command(token) |
|
204 |
||
58900 | 205 |
|
206 |
/* load commands */ |
|
207 |
||
208 |
def load_commands_in(text: String): Boolean = |
|
209 |
load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) |
|
67090
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
210 |
|
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
211 |
|
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
212 |
/* lexicons */ |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
213 |
|
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
214 |
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
|
215 |
(Scan.Lexicon.empty /: kinds)( |
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 |
case (lex, (name, kind)) => |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
218 |
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
|
219 |
lex + name |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
220 |
else lex |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
221 |
}) |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
222 |
|
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
223 |
lazy val minor: Scan.Lexicon = make_lexicon(true) |
0ec94bb9cec4
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
wenzelm
parents:
66919
diff
changeset
|
224 |
lazy val major: Scan.Lexicon = make_lexicon(false) |
58900 | 225 |
} |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
226 |
} |