# HG changeset patch # User wenzelm # Date 1273953949 -7200 # Node ID 285b39022372ab2aacdf8ef1204def204b2bf030 # Parent 4eba866311df182d2d6b4e8bb0164b14028bf0c8 renamed Outer_Keyword to Keyword (in Scala); diff -r 4eba866311df -r 285b39022372 src/Pure/Isar/keyword.scala --- /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 + } + } +} + diff -r 4eba866311df -r 285b39022372 src/Pure/Isar/outer_keyword.scala --- 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 - } - } -} - diff -r 4eba866311df -r 285b39022372 src/Pure/Isar/outer_syntax.scala --- 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 } diff -r 4eba866311df -r 285b39022372 src/Pure/System/session.scala --- 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) } diff -r 4eba866311df -r 285b39022372 src/Pure/build-jars --- 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