--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/keyword.scala Sat May 15 22:05:49 2010 +0200
@@ -0,0 +1,72 @@
+/* Title: Pure/Isar/keyword.scala
+ Author: Makarius
+
+Isar command keyword classification and keyword tables.
+*/
+
+package isabelle
+
+
+object Keyword
+{
+ /* kinds */
+
+ val MINOR = "minor"
+ val CONTROL = "control"
+ val DIAG = "diag"
+ val THY_BEGIN = "theory-begin"
+ val THY_SWITCH = "theory-switch"
+ val THY_END = "theory-end"
+ val THY_HEADING = "theory-heading"
+ val THY_DECL = "theory-decl"
+ val THY_SCRIPT = "theory-script"
+ val THY_GOAL = "theory-goal"
+ val QED = "qed"
+ val QED_BLOCK = "qed-block"
+ val QED_GLOBAL = "qed-global"
+ val PRF_HEADING = "proof-heading"
+ val PRF_GOAL = "proof-goal"
+ val PRF_BLOCK = "proof-block"
+ val PRF_OPEN = "proof-open"
+ val PRF_CLOSE = "proof-close"
+ val PRF_CHAIN = "proof-chain"
+ val PRF_DECL = "proof-decl"
+ val PRF_ASM = "proof-asm"
+ val PRF_ASM_GOAL = "proof-asm-goal"
+ val PRF_SCRIPT = "proof-script"
+
+
+ /* categories */
+
+ val minor = Set(MINOR)
+ val control = Set(CONTROL)
+ val diag = Set(DIAG)
+ val heading = Set(THY_HEADING, PRF_HEADING)
+ val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
+ val theory2 = Set(THY_DECL, THY_GOAL)
+ val proof1 =
+ Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
+ val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
+ val improper = Set(THY_SCRIPT, PRF_SCRIPT)
+
+
+ /* reports */
+
+ object Keyword_Decl {
+ def unapply(msg: XML.Tree): Option[String] =
+ msg match {
+ case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
+ case _ => None
+ }
+ }
+
+ object Command_Decl {
+ def unapply(msg: XML.Tree): Option[(String, String)] =
+ msg match {
+ case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
+ Some((name, kind))
+ case _ => None
+ }
+ }
+}
+
--- a/src/Pure/Isar/outer_keyword.scala Sat May 15 21:57:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-/* Title: Pure/Isar/outer_keyword.scala
- Author: Makarius
-
-Isar command keyword classification and keyword tables.
-*/
-
-package isabelle
-
-
-object Outer_Keyword
-{
- /* kinds */
-
- val MINOR = "minor"
- val CONTROL = "control"
- val DIAG = "diag"
- val THY_BEGIN = "theory-begin"
- val THY_SWITCH = "theory-switch"
- val THY_END = "theory-end"
- val THY_HEADING = "theory-heading"
- val THY_DECL = "theory-decl"
- val THY_SCRIPT = "theory-script"
- val THY_GOAL = "theory-goal"
- val QED = "qed"
- val QED_BLOCK = "qed-block"
- val QED_GLOBAL = "qed-global"
- val PRF_HEADING = "proof-heading"
- val PRF_GOAL = "proof-goal"
- val PRF_BLOCK = "proof-block"
- val PRF_OPEN = "proof-open"
- val PRF_CLOSE = "proof-close"
- val PRF_CHAIN = "proof-chain"
- val PRF_DECL = "proof-decl"
- val PRF_ASM = "proof-asm"
- val PRF_ASM_GOAL = "proof-asm-goal"
- val PRF_SCRIPT = "proof-script"
-
-
- /* categories */
-
- val minor = Set(MINOR)
- val control = Set(CONTROL)
- val diag = Set(DIAG)
- val heading = Set(THY_HEADING, PRF_HEADING)
- val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
- val theory2 = Set(THY_DECL, THY_GOAL)
- val proof1 =
- Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
- val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
- val improper = Set(THY_SCRIPT, PRF_SCRIPT)
-
-
- /* reports */
-
- object Keyword_Decl {
- def unapply(msg: XML.Tree): Option[String] =
- msg match {
- case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
- case _ => None
- }
- }
-
- object Command_Decl {
- def unapply(msg: XML.Tree): Option[(String, String)] =
- msg match {
- case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
- Some((name, kind))
- case _ => None
- }
- }
-}
-
--- a/src/Pure/Isar/outer_syntax.scala Sat May 15 21:57:27 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Sat May 15 22:05:49 2010 +0200
@@ -12,7 +12,7 @@
class Outer_Syntax(symbols: Symbol.Interpretation)
{
- protected val keywords: Map[String, String] = Map((";" -> Outer_Keyword.DIAG))
+ protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
lazy val completion: Completion = new Completion + symbols // FIXME !?
@@ -28,11 +28,11 @@
}
}
- def + (name: String): Outer_Syntax = this + (name, Outer_Keyword.MINOR)
+ def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
def is_command(name: String): Boolean =
keywords.get(name) match {
- case Some(kind) => kind != Outer_Keyword.MINOR
+ case Some(kind) => kind != Keyword.MINOR
case None => false
}
--- a/src/Pure/System/session.scala Sat May 15 21:57:27 2010 +0200
+++ b/src/Pure/System/session.scala Sat May 15 22:05:49 2010 +0200
@@ -140,8 +140,8 @@
}
// keyword declarations
- case List(Outer_Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
- case List(Outer_Keyword.Keyword_Decl(name)) => syntax += name
+ case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
+ case List(Keyword.Keyword_Decl(name)) => syntax += name
case _ => if (!result.is_ready) bad_result(result)
}
--- a/src/Pure/build-jars Sat May 15 21:57:27 2010 +0200
+++ b/src/Pure/build-jars Sat May 15 22:05:49 2010 +0200
@@ -33,7 +33,7 @@
General/xml.scala
General/yxml.scala
Isar/isar_document.scala
- Isar/outer_keyword.scala
+ Isar/keyword.scala
Isar/outer_lex.scala
Isar/outer_parse.scala
Isar/outer_syntax.scala