src/Pure/Isar/keyword.scala
author wenzelm
Mon Dec 01 15:21:49 2014 +0100 (2014-12-01)
changeset 59073 dcecfcc56dce
parent 58999 ed09ae4ea2d8
child 59122 c1dbcde94cd2
permissions -rw-r--r--
more merge operations;
wenzelm@36947
     1
/*  Title:      Pure/Isar/keyword.scala
wenzelm@29449
     2
    Author:     Makarius
wenzelm@29449
     3
wenzelm@58900
     4
Isar keyword classification.
wenzelm@29449
     5
*/
wenzelm@29449
     6
wenzelm@29449
     7
package isabelle
wenzelm@29449
     8
wenzelm@29449
     9
wenzelm@36947
    10
object Keyword
wenzelm@32450
    11
{
wenzelm@58900
    12
  /** keyword classification **/
wenzelm@58900
    13
wenzelm@36681
    14
  /* kinds */
wenzelm@36681
    15
wenzelm@29449
    16
  val DIAG = "diag"
wenzelm@58999
    17
  val DOCUMENT_HEADING = "document_heading"
wenzelm@58999
    18
  val DOCUMENT_BODY = "document_body"
wenzelm@58999
    19
  val DOCUMENT_RAW = "document_raw"
wenzelm@46967
    20
  val THY_BEGIN = "thy_begin"
wenzelm@46967
    21
  val THY_END = "thy_end"
wenzelm@46967
    22
  val THY_DECL = "thy_decl"
wenzelm@58800
    23
  val THY_DECL_BLOCK = "thy_decl_block"
wenzelm@48867
    24
  val THY_LOAD = "thy_load"
wenzelm@46967
    25
  val THY_GOAL = "thy_goal"
wenzelm@29449
    26
  val QED = "qed"
wenzelm@53571
    27
  val QED_SCRIPT = "qed_script"
wenzelm@46967
    28
  val QED_BLOCK = "qed_block"
wenzelm@46967
    29
  val QED_GLOBAL = "qed_global"
wenzelm@46967
    30
  val PRF_GOAL = "prf_goal"
wenzelm@46967
    31
  val PRF_BLOCK = "prf_block"
wenzelm@46967
    32
  val PRF_OPEN = "prf_open"
wenzelm@46967
    33
  val PRF_CLOSE = "prf_close"
wenzelm@46967
    34
  val PRF_CHAIN = "prf_chain"
wenzelm@46967
    35
  val PRF_DECL = "prf_decl"
wenzelm@46967
    36
  val PRF_ASM = "prf_asm"
wenzelm@46967
    37
  val PRF_ASM_GOAL = "prf_asm_goal"
wenzelm@53371
    38
  val PRF_ASM_GOAL_SCRIPT = "prf_asm_goal_script"
wenzelm@46967
    39
  val PRF_SCRIPT = "prf_script"
wenzelm@29449
    40
wenzelm@36681
    41
wenzelm@36681
    42
  /* categories */
wenzelm@36681
    43
wenzelm@58999
    44
  val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
wenzelm@58999
    45
wenzelm@57835
    46
  val diag = Set(DIAG)
wenzelm@57835
    47
wenzelm@58999
    48
  val document_heading = Set(DOCUMENT_HEADING)
wenzelm@58999
    49
  val document_body = Set(DOCUMENT_BODY)
wenzelm@58999
    50
  val document_raw = Set(DOCUMENT_RAW)
wenzelm@58999
    51
  val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
wenzelm@57835
    52
wenzelm@58868
    53
  val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
wenzelm@57837
    54
wenzelm@58800
    55
  val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
wenzelm@58800
    56
wenzelm@58868
    57
  val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
wenzelm@57835
    58
wenzelm@40456
    59
  val proof =
wenzelm@58868
    60
    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
wenzelm@58868
    61
      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
wenzelm@57835
    62
wenzelm@57835
    63
  val proof_body =
wenzelm@58999
    64
    Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
wenzelm@58999
    65
      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
wenzelm@57835
    66
wenzelm@57835
    67
  val theory_goal = Set(THY_GOAL)
wenzelm@57835
    68
  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
wenzelm@57835
    69
  val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
wenzelm@57835
    70
  val qed_global = Set(QED_GLOBAL)
wenzelm@58900
    71
wenzelm@58900
    72
wenzelm@58900
    73
wenzelm@58900
    74
  /** keyword tables **/
wenzelm@58900
    75
wenzelm@58928
    76
  type Spec = ((String, List[String]), List[String])
wenzelm@58928
    77
wenzelm@58900
    78
  object Keywords
wenzelm@58900
    79
  {
wenzelm@58900
    80
    def empty: Keywords = new Keywords()
wenzelm@58900
    81
  }
wenzelm@58900
    82
wenzelm@58900
    83
  class Keywords private(
wenzelm@58900
    84
    val minor: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@58901
    85
    val major: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@59073
    86
    protected val commands: Map[String, (String, List[String])] = Map.empty)
wenzelm@58900
    87
  {
wenzelm@58901
    88
    override def toString: String =
wenzelm@58901
    89
    {
wenzelm@58906
    90
      val keywords1 = minor.iterator.map(quote(_)).toList
wenzelm@58906
    91
      val keywords2 =
wenzelm@58906
    92
        for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield {
wenzelm@58901
    93
          quote(name) + " :: " + quote(kind) +
wenzelm@58901
    94
          (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
wenzelm@58901
    95
        }
wenzelm@58906
    96
      (keywords1 ::: keywords2).mkString("keywords\n  ", " and\n  ", "")
wenzelm@58900
    97
    }
wenzelm@58900
    98
wenzelm@58900
    99
wenzelm@59073
   100
    /* merge */
wenzelm@59073
   101
wenzelm@59073
   102
    def is_empty: Boolean = minor.is_empty && major.is_empty
wenzelm@59073
   103
wenzelm@59073
   104
    def ++ (other: Keywords): Keywords =
wenzelm@59073
   105
      if (this eq other) this
wenzelm@59073
   106
      else if (is_empty) other
wenzelm@59073
   107
      else {
wenzelm@59073
   108
        val minor1 = minor ++ other.minor
wenzelm@59073
   109
        val major1 = major ++ other.major
wenzelm@59073
   110
        val commands1 =
wenzelm@59073
   111
          if (commands eq other.commands) commands
wenzelm@59073
   112
          else if (commands.isEmpty) other.commands
wenzelm@59073
   113
          else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@59073
   114
        new Keywords(minor1, major1, commands1)
wenzelm@59073
   115
      }
wenzelm@59073
   116
wenzelm@59073
   117
wenzelm@58902
   118
    /* add keywords */
wenzelm@58902
   119
wenzelm@58907
   120
    def + (name: String): Keywords = new Keywords(minor + name, major, commands)
wenzelm@58907
   121
    def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
wenzelm@58928
   122
    def + (name: String, kind_tags: (String, List[String])): Keywords =
wenzelm@58902
   123
    {
wenzelm@58902
   124
      val major1 = major + name
wenzelm@58928
   125
      val commands1 = commands + (name -> kind_tags)
wenzelm@58906
   126
      new Keywords(minor, major1, commands1)
wenzelm@58902
   127
    }
wenzelm@58902
   128
wenzelm@58928
   129
    def add_keywords(header: Thy_Header.Keywords): Keywords =
wenzelm@58928
   130
      (this /: header) {
wenzelm@58928
   131
        case (keywords, (name, None, _)) =>
wenzelm@58928
   132
          keywords + Symbol.decode(name) + Symbol.encode(name)
wenzelm@58928
   133
        case (keywords, (name, Some((kind_tags, _)), _)) =>
wenzelm@58928
   134
          keywords + (Symbol.decode(name), kind_tags) + (Symbol.encode(name), kind_tags)
wenzelm@58928
   135
      }
wenzelm@58928
   136
wenzelm@58902
   137
wenzelm@58901
   138
    /* command kind */
wenzelm@58900
   139
wenzelm@58906
   140
    def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
wenzelm@58900
   141
wenzelm@58901
   142
    def is_command_kind(token: Token, pred: String => Boolean): Boolean =
wenzelm@58900
   143
      token.is_command &&
wenzelm@58901
   144
        (command_kind(token.source) match { case Some(k) => pred(k) case None => false })
wenzelm@58900
   145
wenzelm@58900
   146
wenzelm@58900
   147
    /* load commands */
wenzelm@58900
   148
wenzelm@58900
   149
    def load_command(name: String): Option[List[String]] =
wenzelm@58906
   150
      commands.get(name) match {
wenzelm@58900
   151
        case Some((THY_LOAD, exts)) => Some(exts)
wenzelm@58900
   152
        case _ => None
wenzelm@58900
   153
      }
wenzelm@58900
   154
wenzelm@58900
   155
    private lazy val load_commands: List[(String, List[String])] =
wenzelm@58906
   156
      (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList
wenzelm@58900
   157
wenzelm@58900
   158
    def load_commands_in(text: String): Boolean =
wenzelm@58900
   159
      load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
wenzelm@58900
   160
  }
wenzelm@29449
   161
}
wenzelm@29449
   162