author | wenzelm |
Wed, 19 Oct 2011 16:45:46 +0200 | |
changeset 45197 | b6c527c64789 |
parent 40459 | 913e545d9a9b |
child 45666 | d83797ef0d2d |
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 |
|
34158
8b66bd211dcf
class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;
wenzelm
parents:
32450
diff
changeset
|
4 |
Isar command keyword classification and keyword tables. |
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 |
{ |
36681 | 12 |
/* kinds */ |
13 |
||
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
14 |
val MINOR = "minor" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
15 |
val CONTROL = "control" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
16 |
val DIAG = "diag" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
17 |
val THY_BEGIN = "theory-begin" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
18 |
val THY_SWITCH = "theory-switch" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
19 |
val THY_END = "theory-end" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
20 |
val THY_HEADING = "theory-heading" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
21 |
val THY_DECL = "theory-decl" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
22 |
val THY_SCRIPT = "theory-script" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
23 |
val THY_GOAL = "theory-goal" |
40456 | 24 |
val THY_SCHEMATIC_GOAL = "theory-schematic-goal" |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
25 |
val QED = "qed" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
26 |
val QED_BLOCK = "qed-block" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
27 |
val QED_GLOBAL = "qed-global" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
28 |
val PRF_HEADING = "proof-heading" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
29 |
val PRF_GOAL = "proof-goal" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
30 |
val PRF_BLOCK = "proof-block" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
31 |
val PRF_OPEN = "proof-open" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
32 |
val PRF_CLOSE = "proof-close" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
33 |
val PRF_CHAIN = "proof-chain" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
34 |
val PRF_DECL = "proof-decl" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
35 |
val PRF_ASM = "proof-asm" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
36 |
val PRF_ASM_GOAL = "proof-asm-goal" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
37 |
val PRF_SCRIPT = "proof-script" |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
38 |
|
36681 | 39 |
|
40 |
/* categories */ |
|
41 |
||
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
42 |
val minor = Set(MINOR) |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
43 |
val control = Set(CONTROL) |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
44 |
val diag = Set(DIAG) |
40456 | 45 |
val theory = |
46 |
Set(THY_BEGIN, THY_SWITCH, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT, |
|
47 |
THY_GOAL, THY_SCHEMATIC_GOAL) |
|
29450 | 48 |
val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END) |
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
49 |
val theory2 = Set(THY_DECL, THY_GOAL) |
40456 | 50 |
val proof = |
51 |
Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK, |
|
52 |
PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT) |
|
29450 | 53 |
val proof1 = |
54 |
Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL) |
|
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
55 |
val proof2 = Set(PRF_ASM, PRF_ASM_GOAL) |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
56 |
val improper = Set(THY_SCRIPT, PRF_SCRIPT) |
36681 | 57 |
|
58 |
||
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
59 |
/* protocol messages */ |
36681 | 60 |
|
61 |
object Keyword_Decl { |
|
62 |
def unapply(msg: XML.Tree): Option[String] = |
|
63 |
msg match { |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36947
diff
changeset
|
64 |
case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name) |
36681 | 65 |
case _ => None |
66 |
} |
|
67 |
} |
|
68 |
||
69 |
object Command_Decl { |
|
70 |
def unapply(msg: XML.Tree): Option[(String, String)] = |
|
71 |
msg match { |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36947
diff
changeset
|
72 |
case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) => |
36681 | 73 |
Some((name, kind)) |
74 |
case _ => None |
|
75 |
} |
|
76 |
} |
|
29449
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
77 |
} |
6e7745d35a30
added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff
changeset
|
78 |