author | wenzelm |
Fri, 08 Jul 2016 22:22:51 +0200 | |
changeset 63428 | 005b490f0ce2 |
parent 63424 | e4e15bbfb3e2 |
child 63429 | baedd4724f08 |
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" |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
46969
diff
changeset
|
24 |
val THY_LOAD = "thy_load" |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
25 |
val THY_GOAL = "thy_goal" |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
26 |
val QED = "qed" |
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
27 |
val QED_SCRIPT = "qed_script" |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
28 |
val QED_BLOCK = "qed_block" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
29 |
val QED_GLOBAL = "qed_global" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
30 |
val PRF_GOAL = "prf_goal" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
31 |
val PRF_BLOCK = "prf_block" |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
32 |
val NEXT_BLOCK = "next_block" |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
33 |
val PRF_OPEN = "prf_open" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
34 |
val PRF_CLOSE = "prf_close" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
35 |
val PRF_CHAIN = "prf_chain" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
36 |
val PRF_DECL = "prf_decl" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
37 |
val PRF_ASM = "prf_asm" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
38 |
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
|
39 |
val PRF_SCRIPT = "prf_script" |
60624 | 40 |
val PRF_SCRIPT_GOAL = "prf_script_goal" |
41 |
val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal" |
|
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
42 |
|
36681 | 43 |
|
59700 | 44 |
/* command categories */ |
36681 | 45 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
46 |
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
|
47 |
|
57835 | 48 |
val diag = Set(DIAG) |
49 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
50 |
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
|
51 |
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
|
52 |
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
|
53 |
val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) |
57835 | 54 |
|
59700 | 55 |
val theory_begin = Set(THY_BEGIN) |
56 |
val theory_end = Set(THY_END) |
|
57 |
||
59701 | 58 |
val theory_load = Set(THY_LOAD) |
59 |
||
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
60 |
val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL) |
57837 | 61 |
|
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
57837
diff
changeset
|
62 |
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
|
63 |
|
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
64 |
val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL) |
57835 | 65 |
|
40456 | 66 |
val proof = |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
67 |
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
|
68 |
PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, |
60624 | 69 |
PRF_SCRIPT_ASM_GOAL) |
57835 | 70 |
|
71 |
val proof_body = |
|
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60692
diff
changeset
|
72 |
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
|
73 |
PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, |
60624 | 74 |
PRF_SCRIPT_ASM_GOAL) |
57835 | 75 |
|
76 |
val theory_goal = Set(THY_GOAL) |
|
60624 | 77 |
val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) |
57835 | 78 |
val qed = Set(QED, QED_SCRIPT, QED_BLOCK) |
79 |
val qed_global = Set(QED_GLOBAL) |
|
58900 | 80 |
|
60692 | 81 |
val proof_open = proof_goal + PRF_OPEN |
82 |
val proof_close = qed + PRF_CLOSE |
|
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63424
diff
changeset
|
83 |
val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE) |
60692 | 84 |
|
58900 | 85 |
|
86 |
||
87 |
/** keyword tables **/ |
|
88 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
89 |
type Spec = ((String, List[String]), List[String]) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
90 |
|
58900 | 91 |
object Keywords |
92 |
{ |
|
93 |
def empty: Keywords = new Keywords() |
|
94 |
} |
|
95 |
||
96 |
class Keywords private( |
|
97 |
val minor: Scan.Lexicon = Scan.Lexicon.empty, |
|
58901 | 98 |
val major: Scan.Lexicon = Scan.Lexicon.empty, |
59073 | 99 |
protected val commands: Map[String, (String, List[String])] = Map.empty) |
58900 | 100 |
{ |
58901 | 101 |
override def toString: String = |
102 |
{ |
|
58906 | 103 |
val keywords1 = minor.iterator.map(quote(_)).toList |
104 |
val keywords2 = |
|
105 |
for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield { |
|
58901 | 106 |
quote(name) + " :: " + quote(kind) + |
107 |
(if (files.isEmpty) "" else " (" + commas_quote(files) + ")") |
|
108 |
} |
|
58906 | 109 |
(keywords1 ::: keywords2).mkString("keywords\n ", " and\n ", "") |
58900 | 110 |
} |
111 |
||
112 |
||
59073 | 113 |
/* merge */ |
114 |
||
115 |
def is_empty: Boolean = minor.is_empty && major.is_empty |
|
116 |
||
117 |
def ++ (other: Keywords): Keywords = |
|
118 |
if (this eq other) this |
|
119 |
else if (is_empty) other |
|
120 |
else { |
|
121 |
val minor1 = minor ++ other.minor |
|
122 |
val major1 = major ++ other.major |
|
123 |
val commands1 = |
|
124 |
if (commands eq other.commands) commands |
|
125 |
else if (commands.isEmpty) other.commands |
|
126 |
else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } |
|
127 |
new Keywords(minor1, major1, commands1) |
|
128 |
} |
|
129 |
||
130 |
||
58902 | 131 |
/* add keywords */ |
132 |
||
58907 | 133 |
def + (name: String): Keywords = new Keywords(minor + name, major, commands) |
134 |
def + (name: String, kind: String): Keywords = this + (name, (kind, Nil)) |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
135 |
def + (name: String, kind_tags: (String, List[String])): Keywords = |
58902 | 136 |
{ |
137 |
val major1 = major + name |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
138 |
val commands1 = commands + (name -> kind_tags) |
58906 | 139 |
new Keywords(minor, major1, commands1) |
58902 | 140 |
} |
141 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
142 |
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
|
143 |
(this /: header) { |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
144 |
case (keywords, (name, None, _)) => |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
145 |
keywords + Symbol.decode(name) + Symbol.encode(name) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
146 |
case (keywords, (name, Some((kind_tags, _)), _)) => |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
147 |
keywords + (Symbol.decode(name), kind_tags) + (Symbol.encode(name), kind_tags) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
148 |
} |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
149 |
|
58902 | 150 |
|
58901 | 151 |
/* command kind */ |
58900 | 152 |
|
58906 | 153 |
def command_kind(name: String): Option[String] = commands.get(name).map(_._1) |
58900 | 154 |
|
63424 | 155 |
def is_command(token: Token, check_kind: String => Boolean): Boolean = |
156 |
token.is_command && |
|
157 |
(command_kind(token.source) match { case Some(k) => check_kind(k) case None => false }) |
|
59701 | 158 |
|
58900 | 159 |
|
160 |
/* load commands */ |
|
161 |
||
162 |
def load_command(name: String): Option[List[String]] = |
|
58906 | 163 |
commands.get(name) match { |
58900 | 164 |
case Some((THY_LOAD, exts)) => Some(exts) |
165 |
case _ => None |
|
166 |
} |
|
167 |
||
168 |
private lazy val load_commands: List[(String, List[String])] = |
|
58906 | 169 |
(for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList |
58900 | 170 |
|
171 |
def load_commands_in(text: String): Boolean = |
|
172 |
load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) |
|
173 |
} |
|
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
174 |
} |