src/Pure/Isar/keyword.scala
author wenzelm
Tue Apr 04 22:56:28 2017 +0200 (2017-04-04)
changeset 65384 36255c43c64c
parent 63809 56670ab6f55e
child 65385 23f36ab9042b
permissions -rw-r--r--
more explicit types;
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@63441
    42
wenzelm@63441
    43
  val BEFORE_COMMAND = "before_command"
wenzelm@63430
    44
  val QUASI_COMMAND = "quasi_command"
wenzelm@29449
    45
wenzelm@36681
    46
wenzelm@59700
    47
  /* command categories */
wenzelm@36681
    48
wenzelm@58999
    49
  val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
wenzelm@58999
    50
wenzelm@57835
    51
  val diag = Set(DIAG)
wenzelm@57835
    52
wenzelm@58999
    53
  val document_heading = Set(DOCUMENT_HEADING)
wenzelm@58999
    54
  val document_body = Set(DOCUMENT_BODY)
wenzelm@58999
    55
  val document_raw = Set(DOCUMENT_RAW)
wenzelm@58999
    56
  val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
wenzelm@57835
    57
wenzelm@59700
    58
  val theory_begin = Set(THY_BEGIN)
wenzelm@59700
    59
  val theory_end = Set(THY_END)
wenzelm@59700
    60
wenzelm@59701
    61
  val theory_load = Set(THY_LOAD)
wenzelm@59701
    62
wenzelm@58868
    63
  val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
wenzelm@57837
    64
wenzelm@58800
    65
  val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
wenzelm@58800
    66
wenzelm@58868
    67
  val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
wenzelm@57835
    68
wenzelm@63479
    69
  val prf_script = Set(PRF_SCRIPT)
wenzelm@63479
    70
wenzelm@40456
    71
  val proof =
wenzelm@60694
    72
    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, 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 proof_body =
wenzelm@60694
    77
    Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
wenzelm@60694
    78
      PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
wenzelm@60624
    79
      PRF_SCRIPT_ASM_GOAL)
wenzelm@57835
    80
wenzelm@57835
    81
  val theory_goal = Set(THY_GOAL)
wenzelm@60624
    82
  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
wenzelm@57835
    83
  val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
wenzelm@57835
    84
  val qed_global = Set(QED_GLOBAL)
wenzelm@58900
    85
wenzelm@60692
    86
  val proof_open = proof_goal + PRF_OPEN
wenzelm@60692
    87
  val proof_close = qed + PRF_CLOSE
wenzelm@63428
    88
  val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE)
wenzelm@60692
    89
wenzelm@63603
    90
  val close_structure = Set(NEXT_BLOCK, QED_BLOCK, PRF_CLOSE, THY_END)
wenzelm@63603
    91
wenzelm@58900
    92
wenzelm@58900
    93
wenzelm@58900
    94
  /** keyword tables **/
wenzelm@58900
    95
wenzelm@65384
    96
  object Spec
wenzelm@65384
    97
  {
wenzelm@65384
    98
    val none: Spec = Spec("")
wenzelm@65384
    99
  }
wenzelm@65384
   100
  sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
wenzelm@65384
   101
  {
wenzelm@65384
   102
    def is_none: Boolean = kind == ""
wenzelm@65384
   103
  }
wenzelm@63429
   104
wenzelm@58900
   105
  object Keywords
wenzelm@58900
   106
  {
wenzelm@58900
   107
    def empty: Keywords = new Keywords()
wenzelm@58900
   108
  }
wenzelm@58900
   109
wenzelm@58900
   110
  class Keywords private(
wenzelm@58900
   111
    val minor: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@58901
   112
    val major: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@63441
   113
    val kinds: Map[String, String] = Map.empty,
wenzelm@63441
   114
    val load_commands: Map[String, List[String]] = Map.empty)
wenzelm@58900
   115
  {
wenzelm@58901
   116
    override def toString: String =
wenzelm@58901
   117
    {
wenzelm@63441
   118
      val entries =
wenzelm@63441
   119
        for ((name, kind) <- kinds.toList.sortBy(_._1)) yield {
wenzelm@63441
   120
          val exts = load_commands.getOrElse(name, Nil)
wenzelm@63441
   121
          val kind_decl =
wenzelm@63441
   122
            if (kind == "") ""
wenzelm@63441
   123
            else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")")
wenzelm@63441
   124
          quote(name) + kind_decl
wenzelm@63430
   125
        }
wenzelm@63441
   126
      entries.mkString("keywords\n  ", " and\n  ", "")
wenzelm@58900
   127
    }
wenzelm@58900
   128
wenzelm@58900
   129
wenzelm@59073
   130
    /* merge */
wenzelm@59073
   131
wenzelm@59073
   132
    def is_empty: Boolean = minor.is_empty && major.is_empty
wenzelm@59073
   133
wenzelm@59073
   134
    def ++ (other: Keywords): Keywords =
wenzelm@59073
   135
      if (this eq other) this
wenzelm@59073
   136
      else if (is_empty) other
wenzelm@59073
   137
      else {
wenzelm@59073
   138
        val minor1 = minor ++ other.minor
wenzelm@59073
   139
        val major1 = major ++ other.major
wenzelm@63441
   140
        val kinds1 =
wenzelm@63441
   141
          if (kinds eq other.kinds) kinds
wenzelm@63441
   142
          else if (kinds.isEmpty) other.kinds
wenzelm@63441
   143
          else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@63441
   144
        val load_commands1 =
wenzelm@63441
   145
          if (load_commands eq other.load_commands) load_commands
wenzelm@63441
   146
          else if (load_commands.isEmpty) other.load_commands
wenzelm@63441
   147
          else
wenzelm@63441
   148
            (load_commands /: other.load_commands) {
wenzelm@63441
   149
              case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@63441
   150
        new Keywords(minor1, major1, kinds1, load_commands1)
wenzelm@59073
   151
      }
wenzelm@59073
   152
wenzelm@59073
   153
wenzelm@58902
   154
    /* add keywords */
wenzelm@58902
   155
wenzelm@63441
   156
    def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords =
wenzelm@63441
   157
    {
wenzelm@63441
   158
      val kinds1 = kinds + (name -> kind)
wenzelm@63441
   159
      val (minor1, major1) =
wenzelm@63441
   160
        if (kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND)
wenzelm@63441
   161
          (minor + name, major)
wenzelm@63441
   162
        else (minor, major + name)
wenzelm@63441
   163
      val load_commands1 =
wenzelm@63441
   164
        if (kind == THY_LOAD) load_commands + (name -> exts)
wenzelm@63441
   165
        else load_commands
wenzelm@63441
   166
      new Keywords(minor1, major1, kinds1, load_commands1)
wenzelm@63441
   167
    }
wenzelm@58902
   168
wenzelm@58928
   169
    def add_keywords(header: Thy_Header.Keywords): Keywords =
wenzelm@58928
   170
      (this /: header) {
wenzelm@65384
   171
        case (keywords, (name, spec)) =>
wenzelm@65384
   172
          if (spec.is_none)
wenzelm@65384
   173
            keywords + Symbol.decode(name) + Symbol.encode(name)
wenzelm@65384
   174
          else
wenzelm@65384
   175
            keywords +
wenzelm@65384
   176
              (Symbol.decode(name), spec.kind, spec.exts) +
wenzelm@65384
   177
              (Symbol.encode(name), spec.kind, spec.exts)
wenzelm@58928
   178
      }
wenzelm@58928
   179
wenzelm@58902
   180
wenzelm@58901
   181
    /* command kind */
wenzelm@58900
   182
wenzelm@63424
   183
    def is_command(token: Token, check_kind: String => Boolean): Boolean =
wenzelm@63424
   184
      token.is_command &&
wenzelm@63441
   185
        (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false })
wenzelm@63441
   186
wenzelm@63441
   187
    def is_before_command(token: Token): Boolean =
wenzelm@63441
   188
      token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
wenzelm@59701
   189
wenzelm@63430
   190
    def is_quasi_command(token: Token): Boolean =
wenzelm@63441
   191
      token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
wenzelm@63430
   192
wenzelm@63809
   193
    def is_indent_command(token: Token): Boolean =
wenzelm@63809
   194
      token.is_begin_or_command || is_quasi_command(token)
wenzelm@63809
   195
wenzelm@58900
   196
wenzelm@58900
   197
    /* load commands */
wenzelm@58900
   198
wenzelm@58900
   199
    def load_commands_in(text: String): Boolean =
wenzelm@58900
   200
      load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
wenzelm@58900
   201
  }
wenzelm@29449
   202
}