1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/keyword.scala	Sat May 15 22:05:49 2010 +0200
     1.3 @@ -0,0 +1,72 @@
     1.4 +/*  Title:      Pure/Isar/keyword.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Isar command keyword classification and keyword tables.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Keyword
    1.14 +{
    1.15 +  /* kinds */
    1.16 +
    1.17 +  val MINOR = "minor"
    1.18 +  val CONTROL = "control"
    1.19 +  val DIAG = "diag"
    1.20 +  val THY_BEGIN = "theory-begin"
    1.21 +  val THY_SWITCH = "theory-switch"
    1.22 +  val THY_END = "theory-end"
    1.23 +  val THY_HEADING = "theory-heading"
    1.24 +  val THY_DECL = "theory-decl"
    1.25 +  val THY_SCRIPT = "theory-script"
    1.26 +  val THY_GOAL = "theory-goal"
    1.27 +  val QED = "qed"
    1.28 +  val QED_BLOCK = "qed-block"
    1.29 +  val QED_GLOBAL = "qed-global"
    1.30 +  val PRF_HEADING = "proof-heading"
    1.31 +  val PRF_GOAL = "proof-goal"
    1.32 +  val PRF_BLOCK = "proof-block"
    1.33 +  val PRF_OPEN = "proof-open"
    1.34 +  val PRF_CLOSE = "proof-close"
    1.35 +  val PRF_CHAIN = "proof-chain"
    1.36 +  val PRF_DECL = "proof-decl"
    1.37 +  val PRF_ASM = "proof-asm"
    1.38 +  val PRF_ASM_GOAL = "proof-asm-goal"
    1.39 +  val PRF_SCRIPT = "proof-script"
    1.40 +
    1.41 +
    1.42 +  /* categories */
    1.43 +
    1.44 +  val minor = Set(MINOR)
    1.45 +  val control = Set(CONTROL)
    1.46 +  val diag = Set(DIAG)
    1.47 +  val heading = Set(THY_HEADING, PRF_HEADING)
    1.48 +  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    1.49 +  val theory2 = Set(THY_DECL, THY_GOAL)
    1.50 +  val proof1 =
    1.51 +    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    1.52 +  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    1.53 +  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    1.54 +
    1.55 +
    1.56 +  /* reports */
    1.57 +
    1.58 +  object Keyword_Decl {
    1.59 +    def unapply(msg: XML.Tree): Option[String] =
    1.60 +      msg match {
    1.61 +        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
    1.62 +        case _ => None
    1.63 +      }
    1.64 +  }
    1.65 +
    1.66 +  object Command_Decl {
    1.67 +    def unapply(msg: XML.Tree): Option[(String, String)] =
    1.68 +      msg match {
    1.69 +        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
    1.70 +          Some((name, kind))
    1.71 +        case _ => None
    1.72 +      }
    1.73 +  }
    1.74 +}
    1.75 +

     2.1 --- a/src/Pure/Isar/outer_keyword.scala	Sat May 15 21:57:27 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,72 +0,0 @@
     2.4 -/*  Title:      Pure/Isar/outer_keyword.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Isar command keyword classification and keyword tables.
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -
    2.13 -object Outer_Keyword
    2.14 -{
    2.15 -  /* kinds */
    2.16 -
    2.17 -  val MINOR = "minor"
    2.18 -  val CONTROL = "control"
    2.19 -  val DIAG = "diag"
    2.20 -  val THY_BEGIN = "theory-begin"
    2.21 -  val THY_SWITCH = "theory-switch"
    2.22 -  val THY_END = "theory-end"
    2.23 -  val THY_HEADING = "theory-heading"
    2.24 -  val THY_DECL = "theory-decl"
    2.25 -  val THY_SCRIPT = "theory-script"
    2.26 -  val THY_GOAL = "theory-goal"
    2.27 -  val QED = "qed"
    2.28 -  val QED_BLOCK = "qed-block"
    2.29 -  val QED_GLOBAL = "qed-global"
    2.30 -  val PRF_HEADING = "proof-heading"
    2.31 -  val PRF_GOAL = "proof-goal"
    2.32 -  val PRF_BLOCK = "proof-block"
    2.33 -  val PRF_OPEN = "proof-open"
    2.34 -  val PRF_CLOSE = "proof-close"
    2.35 -  val PRF_CHAIN = "proof-chain"
    2.36 -  val PRF_DECL = "proof-decl"
    2.37 -  val PRF_ASM = "proof-asm"
    2.38 -  val PRF_ASM_GOAL = "proof-asm-goal"
    2.39 -  val PRF_SCRIPT = "proof-script"
    2.40 -
    2.41 -
    2.42 -  /* categories */
    2.43 -
    2.44 -  val minor = Set(MINOR)
    2.45 -  val control = Set(CONTROL)
    2.46 -  val diag = Set(DIAG)
    2.47 -  val heading = Set(THY_HEADING, PRF_HEADING)
    2.48 -  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    2.49 -  val theory2 = Set(THY_DECL, THY_GOAL)
    2.50 -  val proof1 =
    2.51 -    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    2.52 -  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    2.53 -  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    2.54 -
    2.55 -
    2.56 -  /* reports */
    2.57 -
    2.58 -  object Keyword_Decl {
    2.59 -    def unapply(msg: XML.Tree): Option[String] =
    2.60 -      msg match {
    2.61 -        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
    2.62 -        case _ => None
    2.63 -      }
    2.64 -  }
    2.65 -
    2.66 -  object Command_Decl {
    2.67 -    def unapply(msg: XML.Tree): Option[(String, String)] =
    2.68 -      msg match {
    2.69 -        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
    2.70 -          Some((name, kind))
    2.71 -        case _ => None
    2.72 -      }
    2.73 -  }
    2.74 -}
    2.75 -

     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat May 15 21:57:27 2010 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat May 15 22:05:49 2010 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  
     3.5  class Outer_Syntax(symbols: Symbol.Interpretation)
     3.6  {
     3.7 -  protected val keywords: Map[String, String] = Map((";" -> Outer_Keyword.DIAG))
     3.8 +  protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
     3.9    protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
    3.10    lazy val completion: Completion = new Completion + symbols  // FIXME !?
    3.11  
    3.12 @@ -28,11 +28,11 @@
    3.13      }
    3.14    }
    3.15  
    3.16 -  def + (name: String): Outer_Syntax = this + (name, Outer_Keyword.MINOR)
    3.17 +  def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    3.18  
    3.19    def is_command(name: String): Boolean =
    3.20      keywords.get(name) match {
    3.21 -      case Some(kind) => kind != Outer_Keyword.MINOR
    3.22 +      case Some(kind) => kind != Keyword.MINOR
    3.23        case None => false
    3.24      }
    3.25  

     4.1 --- a/src/Pure/System/session.scala	Sat May 15 21:57:27 2010 +0200
     4.2 +++ b/src/Pure/System/session.scala	Sat May 15 22:05:49 2010 +0200
     4.3 @@ -140,8 +140,8 @@
     4.4              }
     4.5  
     4.6            // keyword declarations
     4.7 -          case List(Outer_Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
     4.8 -          case List(Outer_Keyword.Keyword_Decl(name)) => syntax += name
     4.9 +          case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    4.10 +          case List(Keyword.Keyword_Decl(name)) => syntax += name
    4.11  
    4.12            case _ => if (!result.is_ready) bad_result(result)
    4.13          }

     5.1 --- a/src/Pure/build-jars	Sat May 15 21:57:27 2010 +0200
     5.2 +++ b/src/Pure/build-jars	Sat May 15 22:05:49 2010 +0200
     5.3 @@ -33,7 +33,7 @@
     5.4    General/xml.scala
     5.5    General/yxml.scala
     5.6    Isar/isar_document.scala
     5.7 -  Isar/outer_keyword.scala
     5.8 +  Isar/keyword.scala
     5.9    Isar/outer_lex.scala
    5.10    Isar/outer_parse.scala
    5.11    Isar/outer_syntax.scala