src/Pure/Isar/outer_keyword.scala
author wenzelm
Thu, 06 May 2010 13:41:30 +0200
changeset 36681 dffeca08d3bf
parent 34166 446a33b874b3
permissions -rw-r--r--
extractors for outer keyword declarations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Isar/outer_keyword.scala
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
34158
8b66bd211dcf class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;
wenzelm
parents: 32450
diff changeset
    10
object Outer_Keyword
32450
375db037f4d2 misc tuning;
wenzelm
parents: 29450
diff changeset
    11
{
36681
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    12
  /* kinds */
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    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"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    24
  val QED = "qed"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    25
  val QED_BLOCK = "qed-block"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    26
  val QED_GLOBAL = "qed-global"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    27
  val PRF_HEADING = "proof-heading"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    28
  val PRF_GOAL = "proof-goal"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    29
  val PRF_BLOCK = "proof-block"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    30
  val PRF_OPEN = "proof-open"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    31
  val PRF_CLOSE = "proof-close"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    32
  val PRF_CHAIN = "proof-chain"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    33
  val PRF_DECL = "proof-decl"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    34
  val PRF_ASM = "proof-asm"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    35
  val PRF_ASM_GOAL = "proof-asm-goal"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    36
  val PRF_SCRIPT = "proof-script"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    37
36681
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    38
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    39
  /* categories */
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    40
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    41
  val minor = Set(MINOR)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    42
  val control = Set(CONTROL)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    43
  val diag = Set(DIAG)
29450
ac7f67be7f1f tuned categories;
wenzelm
parents: 29449
diff changeset
    44
  val heading = Set(THY_HEADING, PRF_HEADING)
ac7f67be7f1f tuned categories;
wenzelm
parents: 29449
diff changeset
    45
  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    46
  val theory2 = Set(THY_DECL, THY_GOAL)
29450
ac7f67be7f1f tuned categories;
wenzelm
parents: 29449
diff changeset
    47
  val proof1 =
ac7f67be7f1f tuned categories;
wenzelm
parents: 29449
diff changeset
    48
    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
    49
  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    50
  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
36681
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    51
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    52
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    53
  /* reports */
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    54
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    55
  object Keyword_Decl {
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    56
    def unapply(msg: XML.Tree): Option[String] =
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    57
      msg match {
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    58
        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    59
        case _ => None
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    60
      }
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    61
  }
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    62
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    63
  object Command_Decl {
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    64
    def unapply(msg: XML.Tree): Option[(String, String)] =
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    65
      msg match {
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    66
        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    67
          Some((name, kind))
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    68
        case _ => None
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    69
      }
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    70
  }
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    71
}
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    72