author | wenzelm |
Wed, 08 Jul 2015 12:09:44 +0200 | |
changeset 60692 | 896704918a1f |
parent 60624 | 5b6552e12421 |
child 60694 | b3fa4a8cdb5f |
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" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
32 |
val PRF_OPEN = "prf_open" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
33 |
val PRF_CLOSE = "prf_close" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
34 |
val PRF_CHAIN = "prf_chain" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
35 |
val PRF_DECL = "prf_decl" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
36 |
val PRF_ASM = "prf_asm" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46123
diff
changeset
|
37 |
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
|
38 |
val PRF_SCRIPT = "prf_script" |
60624 | 39 |
val PRF_SCRIPT_GOAL = "prf_script_goal" |
40 |
val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal" |
|
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
41 |
|
36681 | 42 |
|
59700 | 43 |
/* command categories */ |
36681 | 44 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
45 |
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
|
46 |
|
57835 | 47 |
val diag = Set(DIAG) |
48 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
49 |
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
|
50 |
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
|
51 |
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
|
52 |
val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) |
57835 | 53 |
|
59700 | 54 |
val theory_begin = Set(THY_BEGIN) |
55 |
val theory_end = Set(THY_END) |
|
56 |
||
59701 | 57 |
val theory_load = Set(THY_LOAD) |
58 |
||
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
59 |
val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL) |
57837 | 60 |
|
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
57837
diff
changeset
|
61 |
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
|
62 |
|
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
63 |
val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL) |
57835 | 64 |
|
40456 | 65 |
val proof = |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
66 |
Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, |
60624 | 67 |
PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, |
68 |
PRF_SCRIPT_ASM_GOAL) |
|
57835 | 69 |
|
70 |
val proof_body = |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
71 |
Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, |
60624 | 72 |
PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, |
73 |
PRF_SCRIPT_ASM_GOAL) |
|
57835 | 74 |
|
75 |
val theory_goal = Set(THY_GOAL) |
|
60624 | 76 |
val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) |
57835 | 77 |
val qed = Set(QED, QED_SCRIPT, QED_BLOCK) |
78 |
val qed_global = Set(QED_GLOBAL) |
|
58900 | 79 |
|
60692 | 80 |
val proof_open = proof_goal + PRF_OPEN |
81 |
val proof_close = qed + PRF_CLOSE |
|
82 |
||
58900 | 83 |
|
84 |
||
85 |
/** keyword tables **/ |
|
86 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
87 |
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
|
88 |
|
58900 | 89 |
object Keywords |
90 |
{ |
|
91 |
def empty: Keywords = new Keywords() |
|
92 |
} |
|
93 |
||
94 |
class Keywords private( |
|
95 |
val minor: Scan.Lexicon = Scan.Lexicon.empty, |
|
58901 | 96 |
val major: Scan.Lexicon = Scan.Lexicon.empty, |
59073 | 97 |
protected val commands: Map[String, (String, List[String])] = Map.empty) |
58900 | 98 |
{ |
58901 | 99 |
override def toString: String = |
100 |
{ |
|
58906 | 101 |
val keywords1 = minor.iterator.map(quote(_)).toList |
102 |
val keywords2 = |
|
103 |
for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield { |
|
58901 | 104 |
quote(name) + " :: " + quote(kind) + |
105 |
(if (files.isEmpty) "" else " (" + commas_quote(files) + ")") |
|
106 |
} |
|
58906 | 107 |
(keywords1 ::: keywords2).mkString("keywords\n ", " and\n ", "") |
58900 | 108 |
} |
109 |
||
110 |
||
59073 | 111 |
/* merge */ |
112 |
||
113 |
def is_empty: Boolean = minor.is_empty && major.is_empty |
|
114 |
||
115 |
def ++ (other: Keywords): Keywords = |
|
116 |
if (this eq other) this |
|
117 |
else if (is_empty) other |
|
118 |
else { |
|
119 |
val minor1 = minor ++ other.minor |
|
120 |
val major1 = major ++ other.major |
|
121 |
val commands1 = |
|
122 |
if (commands eq other.commands) commands |
|
123 |
else if (commands.isEmpty) other.commands |
|
124 |
else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } |
|
125 |
new Keywords(minor1, major1, commands1) |
|
126 |
} |
|
127 |
||
128 |
||
58902 | 129 |
/* add keywords */ |
130 |
||
58907 | 131 |
def + (name: String): Keywords = new Keywords(minor + name, major, commands) |
132 |
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
|
133 |
def + (name: String, kind_tags: (String, List[String])): Keywords = |
58902 | 134 |
{ |
135 |
val major1 = major + name |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
136 |
val commands1 = commands + (name -> kind_tags) |
58906 | 137 |
new Keywords(minor, major1, commands1) |
58902 | 138 |
} |
139 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
140 |
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
|
141 |
(this /: header) { |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
142 |
case (keywords, (name, None, _)) => |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
143 |
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
|
144 |
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
|
145 |
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
|
146 |
} |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58907
diff
changeset
|
147 |
|
58902 | 148 |
|
58901 | 149 |
/* command kind */ |
58900 | 150 |
|
58906 | 151 |
def command_kind(name: String): Option[String] = commands.get(name).map(_._1) |
58900 | 152 |
|
59701 | 153 |
def is_command_kind(name: String, pred: String => Boolean): Boolean = |
154 |
command_kind(name) match { |
|
155 |
case Some(kind) => pred(kind) |
|
156 |
case None => false |
|
157 |
} |
|
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 |
} |