src/Pure/Isar/keyword.scala
author wenzelm
Sun Jul 10 11:18:35 2016 +0200 (2016-07-10)
changeset 63429 baedd4724f08
parent 63428 005b490f0ce2
child 63430 9c5fcd355a2d
permissions -rw-r--r--
tuned signature: more uniform Keyword.spec;
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@60694
    32
  val NEXT_BLOCK = "next_block"
wenzelm@46967
    33
  val PRF_OPEN = "prf_open"
wenzelm@46967
    34
  val PRF_CLOSE = "prf_close"
wenzelm@46967
    35
  val PRF_CHAIN = "prf_chain"
wenzelm@46967
    36
  val PRF_DECL = "prf_decl"
wenzelm@46967
    37
  val PRF_ASM = "prf_asm"
wenzelm@46967
    38
  val PRF_ASM_GOAL = "prf_asm_goal"
wenzelm@46967
    39
  val PRF_SCRIPT = "prf_script"
wenzelm@60624
    40
  val PRF_SCRIPT_GOAL = "prf_script_goal"
wenzelm@60624
    41
  val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
wenzelm@29449
    42
wenzelm@36681
    43
wenzelm@59700
    44
  /* command categories */
wenzelm@36681
    45
wenzelm@58999
    46
  val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
wenzelm@58999
    47
wenzelm@57835
    48
  val diag = Set(DIAG)
wenzelm@57835
    49
wenzelm@58999
    50
  val document_heading = Set(DOCUMENT_HEADING)
wenzelm@58999
    51
  val document_body = Set(DOCUMENT_BODY)
wenzelm@58999
    52
  val document_raw = Set(DOCUMENT_RAW)
wenzelm@58999
    53
  val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
wenzelm@57835
    54
wenzelm@59700
    55
  val theory_begin = Set(THY_BEGIN)
wenzelm@59700
    56
  val theory_end = Set(THY_END)
wenzelm@59700
    57
wenzelm@59701
    58
  val theory_load = Set(THY_LOAD)
wenzelm@59701
    59
wenzelm@58868
    60
  val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
wenzelm@57837
    61
wenzelm@58800
    62
  val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
wenzelm@58800
    63
wenzelm@58868
    64
  val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
wenzelm@57835
    65
wenzelm@40456
    66
  val proof =
wenzelm@60694
    67
    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
wenzelm@60694
    68
      PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
wenzelm@60624
    69
      PRF_SCRIPT_ASM_GOAL)
wenzelm@57835
    70
wenzelm@57835
    71
  val proof_body =
wenzelm@60694
    72
    Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
wenzelm@60694
    73
      PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
wenzelm@60624
    74
      PRF_SCRIPT_ASM_GOAL)
wenzelm@57835
    75
wenzelm@57835
    76
  val theory_goal = Set(THY_GOAL)
wenzelm@60624
    77
  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
wenzelm@57835
    78
  val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
wenzelm@57835
    79
  val qed_global = Set(QED_GLOBAL)
wenzelm@58900
    80
wenzelm@60692
    81
  val proof_open = proof_goal + PRF_OPEN
wenzelm@60692
    82
  val proof_close = qed + PRF_CLOSE
wenzelm@63428
    83
  val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE)
wenzelm@60692
    84
wenzelm@58900
    85
wenzelm@58900
    86
wenzelm@58900
    87
  /** keyword tables **/
wenzelm@58900
    88
wenzelm@58928
    89
  type Spec = ((String, List[String]), List[String])
wenzelm@58928
    90
wenzelm@63429
    91
  val no_spec: Spec = (("", Nil), Nil)
wenzelm@63429
    92
wenzelm@58900
    93
  object Keywords
wenzelm@58900
    94
  {
wenzelm@58900
    95
    def empty: Keywords = new Keywords()
wenzelm@58900
    96
  }
wenzelm@58900
    97
wenzelm@58900
    98
  class Keywords private(
wenzelm@58900
    99
    val minor: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@58901
   100
    val major: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@59073
   101
    protected val commands: Map[String, (String, List[String])] = Map.empty)
wenzelm@58900
   102
  {
wenzelm@58901
   103
    override def toString: String =
wenzelm@58901
   104
    {
wenzelm@58906
   105
      val keywords1 = minor.iterator.map(quote(_)).toList
wenzelm@58906
   106
      val keywords2 =
wenzelm@58906
   107
        for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield {
wenzelm@58901
   108
          quote(name) + " :: " + quote(kind) +
wenzelm@58901
   109
          (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
wenzelm@58901
   110
        }
wenzelm@58906
   111
      (keywords1 ::: keywords2).mkString("keywords\n  ", " and\n  ", "")
wenzelm@58900
   112
    }
wenzelm@58900
   113
wenzelm@58900
   114
wenzelm@59073
   115
    /* merge */
wenzelm@59073
   116
wenzelm@59073
   117
    def is_empty: Boolean = minor.is_empty && major.is_empty
wenzelm@59073
   118
wenzelm@59073
   119
    def ++ (other: Keywords): Keywords =
wenzelm@59073
   120
      if (this eq other) this
wenzelm@59073
   121
      else if (is_empty) other
wenzelm@59073
   122
      else {
wenzelm@59073
   123
        val minor1 = minor ++ other.minor
wenzelm@59073
   124
        val major1 = major ++ other.major
wenzelm@59073
   125
        val commands1 =
wenzelm@59073
   126
          if (commands eq other.commands) commands
wenzelm@59073
   127
          else if (commands.isEmpty) other.commands
wenzelm@59073
   128
          else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@59073
   129
        new Keywords(minor1, major1, commands1)
wenzelm@59073
   130
      }
wenzelm@59073
   131
wenzelm@59073
   132
wenzelm@58902
   133
    /* add keywords */
wenzelm@58902
   134
wenzelm@63429
   135
    def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords =
wenzelm@63429
   136
      if (kind == "") new Keywords(minor + name, major, commands)
wenzelm@63429
   137
      else {
wenzelm@63429
   138
        val major1 = major + name
wenzelm@63429
   139
        val commands1 = commands + (name -> (kind, tags))
wenzelm@63429
   140
        new Keywords(minor, major1, commands1)
wenzelm@63429
   141
      }
wenzelm@58902
   142
wenzelm@58928
   143
    def add_keywords(header: Thy_Header.Keywords): Keywords =
wenzelm@58928
   144
      (this /: header) {
wenzelm@63429
   145
        case (keywords, (name, ((kind, tags), _), _)) =>
wenzelm@63429
   146
          if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
wenzelm@63429
   147
          else keywords + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
wenzelm@58928
   148
      }
wenzelm@58928
   149
wenzelm@58902
   150
wenzelm@58901
   151
    /* command kind */
wenzelm@58900
   152
wenzelm@58906
   153
    def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
wenzelm@58900
   154
wenzelm@63424
   155
    def is_command(token: Token, check_kind: String => Boolean): Boolean =
wenzelm@63424
   156
      token.is_command &&
wenzelm@63424
   157
        (command_kind(token.source) match { case Some(k) => check_kind(k) case None => false })
wenzelm@59701
   158
wenzelm@58900
   159
wenzelm@58900
   160
    /* load commands */
wenzelm@58900
   161
wenzelm@58900
   162
    def load_command(name: String): Option[List[String]] =
wenzelm@58906
   163
      commands.get(name) match {
wenzelm@58900
   164
        case Some((THY_LOAD, exts)) => Some(exts)
wenzelm@58900
   165
        case _ => None
wenzelm@58900
   166
      }
wenzelm@58900
   167
wenzelm@58900
   168
    private lazy val load_commands: List[(String, List[String])] =
wenzelm@58906
   169
      (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList
wenzelm@58900
   170
wenzelm@58900
   171
    def load_commands_in(text: String): Boolean =
wenzelm@58900
   172
      load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
wenzelm@58900
   173
  }
wenzelm@29449
   174
}