src/Pure/Isar/keyword.scala
author wenzelm
Thu Mar 14 16:55:06 2019 +0100 (3 months ago)
changeset 69913 ca515cf61651
parent 67090 0ec94bb9cec4
child 69917 66c4567664b5
permissions -rw-r--r--
more specific keyword kinds;
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@69913
    24
  val THY_DEFN = "thy_defn"
wenzelm@69913
    25
  val THY_STMT = "thy_stmt"
wenzelm@48867
    26
  val THY_LOAD = "thy_load"
wenzelm@46967
    27
  val THY_GOAL = "thy_goal"
wenzelm@69913
    28
  val THY_GOAL_DEFN = "thy_goal_defn"
wenzelm@69913
    29
  val THY_GOAL_STMT = "thy_goal_stmt"
wenzelm@29449
    30
  val QED = "qed"
wenzelm@53571
    31
  val QED_SCRIPT = "qed_script"
wenzelm@46967
    32
  val QED_BLOCK = "qed_block"
wenzelm@46967
    33
  val QED_GLOBAL = "qed_global"
wenzelm@46967
    34
  val PRF_GOAL = "prf_goal"
wenzelm@46967
    35
  val PRF_BLOCK = "prf_block"
wenzelm@60694
    36
  val NEXT_BLOCK = "next_block"
wenzelm@46967
    37
  val PRF_OPEN = "prf_open"
wenzelm@46967
    38
  val PRF_CLOSE = "prf_close"
wenzelm@46967
    39
  val PRF_CHAIN = "prf_chain"
wenzelm@46967
    40
  val PRF_DECL = "prf_decl"
wenzelm@46967
    41
  val PRF_ASM = "prf_asm"
wenzelm@46967
    42
  val PRF_ASM_GOAL = "prf_asm_goal"
wenzelm@46967
    43
  val PRF_SCRIPT = "prf_script"
wenzelm@60624
    44
  val PRF_SCRIPT_GOAL = "prf_script_goal"
wenzelm@60624
    45
  val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
wenzelm@63441
    46
wenzelm@63441
    47
  val BEFORE_COMMAND = "before_command"
wenzelm@63430
    48
  val QUASI_COMMAND = "quasi_command"
wenzelm@29449
    49
wenzelm@36681
    50
wenzelm@59700
    51
  /* command categories */
wenzelm@36681
    52
wenzelm@58999
    53
  val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
wenzelm@58999
    54
wenzelm@57835
    55
  val diag = Set(DIAG)
wenzelm@57835
    56
wenzelm@58999
    57
  val document_heading = Set(DOCUMENT_HEADING)
wenzelm@58999
    58
  val document_body = Set(DOCUMENT_BODY)
wenzelm@58999
    59
  val document_raw = Set(DOCUMENT_RAW)
wenzelm@58999
    60
  val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
wenzelm@57835
    61
wenzelm@59700
    62
  val theory_begin = Set(THY_BEGIN)
wenzelm@59700
    63
  val theory_end = Set(THY_END)
wenzelm@59700
    64
wenzelm@59701
    65
  val theory_load = Set(THY_LOAD)
wenzelm@59701
    66
wenzelm@69913
    67
  val theory =
wenzelm@69913
    68
    Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT,
wenzelm@69913
    69
      THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
wenzelm@57837
    70
wenzelm@58800
    71
  val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
wenzelm@58800
    72
wenzelm@69913
    73
  val theory_body =
wenzelm@69913
    74
    Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT,
wenzelm@69913
    75
      THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
wenzelm@57835
    76
wenzelm@63479
    77
  val prf_script = Set(PRF_SCRIPT)
wenzelm@63479
    78
wenzelm@40456
    79
  val proof =
wenzelm@60694
    80
    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
wenzelm@60694
    81
      PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
wenzelm@60624
    82
      PRF_SCRIPT_ASM_GOAL)
wenzelm@57835
    83
wenzelm@57835
    84
  val proof_body =
wenzelm@60694
    85
    Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
wenzelm@60694
    86
      PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
wenzelm@60624
    87
      PRF_SCRIPT_ASM_GOAL)
wenzelm@57835
    88
wenzelm@69913
    89
  val theory_goal = Set(THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
wenzelm@60624
    90
  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
wenzelm@57835
    91
  val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
wenzelm@57835
    92
  val qed_global = Set(QED_GLOBAL)
wenzelm@58900
    93
wenzelm@60692
    94
  val proof_open = proof_goal + PRF_OPEN
wenzelm@60692
    95
  val proof_close = qed + PRF_CLOSE
wenzelm@63428
    96
  val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE)
wenzelm@60692
    97
wenzelm@63603
    98
  val close_structure = Set(NEXT_BLOCK, QED_BLOCK, PRF_CLOSE, THY_END)
wenzelm@63603
    99
wenzelm@58900
   100
wenzelm@58900
   101
wenzelm@58900
   102
  /** keyword tables **/
wenzelm@58900
   103
wenzelm@65384
   104
  object Spec
wenzelm@65384
   105
  {
wenzelm@65384
   106
    val none: Spec = Spec("")
wenzelm@65384
   107
  }
wenzelm@65384
   108
  sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
wenzelm@65384
   109
  {
wenzelm@65384
   110
    def is_none: Boolean = kind == ""
wenzelm@65385
   111
wenzelm@65385
   112
    override def toString: String =
wenzelm@65385
   113
      kind +
wenzelm@65385
   114
        (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") +
wenzelm@65385
   115
        (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", ""))
wenzelm@65384
   116
  }
wenzelm@63429
   117
wenzelm@58900
   118
  object Keywords
wenzelm@58900
   119
  {
wenzelm@58900
   120
    def empty: Keywords = new Keywords()
wenzelm@58900
   121
  }
wenzelm@58900
   122
wenzelm@58900
   123
  class Keywords private(
wenzelm@63441
   124
    val kinds: Map[String, String] = Map.empty,
wenzelm@63441
   125
    val load_commands: Map[String, List[String]] = Map.empty)
wenzelm@58900
   126
  {
wenzelm@58901
   127
    override def toString: String =
wenzelm@58901
   128
    {
wenzelm@63441
   129
      val entries =
wenzelm@63441
   130
        for ((name, kind) <- kinds.toList.sortBy(_._1)) yield {
wenzelm@63441
   131
          val exts = load_commands.getOrElse(name, Nil)
wenzelm@63441
   132
          val kind_decl =
wenzelm@63441
   133
            if (kind == "") ""
wenzelm@63441
   134
            else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")")
wenzelm@63441
   135
          quote(name) + kind_decl
wenzelm@63430
   136
        }
wenzelm@63441
   137
      entries.mkString("keywords\n  ", " and\n  ", "")
wenzelm@58900
   138
    }
wenzelm@58900
   139
wenzelm@58900
   140
wenzelm@59073
   141
    /* merge */
wenzelm@59073
   142
wenzelm@67090
   143
    def is_empty: Boolean = kinds.isEmpty
wenzelm@59073
   144
wenzelm@59073
   145
    def ++ (other: Keywords): Keywords =
wenzelm@59073
   146
      if (this eq other) this
wenzelm@59073
   147
      else if (is_empty) other
wenzelm@59073
   148
      else {
wenzelm@63441
   149
        val kinds1 =
wenzelm@63441
   150
          if (kinds eq other.kinds) kinds
wenzelm@63441
   151
          else if (kinds.isEmpty) other.kinds
wenzelm@63441
   152
          else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@63441
   153
        val load_commands1 =
wenzelm@63441
   154
          if (load_commands eq other.load_commands) load_commands
wenzelm@63441
   155
          else if (load_commands.isEmpty) other.load_commands
wenzelm@63441
   156
          else
wenzelm@63441
   157
            (load_commands /: other.load_commands) {
wenzelm@63441
   158
              case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@67090
   159
        new Keywords(kinds1, load_commands1)
wenzelm@59073
   160
      }
wenzelm@59073
   161
wenzelm@59073
   162
wenzelm@58902
   163
    /* add keywords */
wenzelm@58902
   164
wenzelm@63441
   165
    def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords =
wenzelm@63441
   166
    {
wenzelm@63441
   167
      val kinds1 = kinds + (name -> kind)
wenzelm@63441
   168
      val load_commands1 =
wenzelm@66919
   169
        if (kind == THY_LOAD) {
wenzelm@66919
   170
          if (!Symbol.iterator(name).forall(Symbol.is_ascii(_)))
wenzelm@66919
   171
            error("Bad theory load command " + quote(name))
wenzelm@66919
   172
          load_commands + (name -> exts)
wenzelm@66919
   173
        }
wenzelm@63441
   174
        else load_commands
wenzelm@67090
   175
      new Keywords(kinds1, load_commands1)
wenzelm@63441
   176
    }
wenzelm@58902
   177
wenzelm@58928
   178
    def add_keywords(header: Thy_Header.Keywords): Keywords =
wenzelm@58928
   179
      (this /: header) {
wenzelm@65384
   180
        case (keywords, (name, spec)) =>
wenzelm@65384
   181
          if (spec.is_none)
wenzelm@65384
   182
            keywords + Symbol.decode(name) + Symbol.encode(name)
wenzelm@65384
   183
          else
wenzelm@65384
   184
            keywords +
wenzelm@65384
   185
              (Symbol.decode(name), spec.kind, spec.exts) +
wenzelm@65384
   186
              (Symbol.encode(name), spec.kind, spec.exts)
wenzelm@58928
   187
      }
wenzelm@58928
   188
wenzelm@58902
   189
wenzelm@58901
   190
    /* command kind */
wenzelm@58900
   191
wenzelm@63424
   192
    def is_command(token: Token, check_kind: String => Boolean): Boolean =
wenzelm@63424
   193
      token.is_command &&
wenzelm@63441
   194
        (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false })
wenzelm@63441
   195
wenzelm@63441
   196
    def is_before_command(token: Token): Boolean =
wenzelm@63441
   197
      token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
wenzelm@59701
   198
wenzelm@63430
   199
    def is_quasi_command(token: Token): Boolean =
wenzelm@63441
   200
      token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
wenzelm@63430
   201
wenzelm@63809
   202
    def is_indent_command(token: Token): Boolean =
wenzelm@63809
   203
      token.is_begin_or_command || is_quasi_command(token)
wenzelm@63809
   204
wenzelm@58900
   205
wenzelm@58900
   206
    /* load commands */
wenzelm@58900
   207
wenzelm@58900
   208
    def load_commands_in(text: String): Boolean =
wenzelm@58900
   209
      load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
wenzelm@67090
   210
wenzelm@67090
   211
wenzelm@67090
   212
    /* lexicons */
wenzelm@67090
   213
wenzelm@67090
   214
    private def make_lexicon(is_minor: Boolean): Scan.Lexicon =
wenzelm@67090
   215
      (Scan.Lexicon.empty /: kinds)(
wenzelm@67090
   216
        {
wenzelm@67090
   217
          case (lex, (name, kind)) =>
wenzelm@67090
   218
            if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor)
wenzelm@67090
   219
              lex + name
wenzelm@67090
   220
            else lex
wenzelm@67090
   221
        })
wenzelm@67090
   222
wenzelm@67090
   223
    lazy val minor: Scan.Lexicon = make_lexicon(true)
wenzelm@67090
   224
    lazy val major: Scan.Lexicon = make_lexicon(false)
wenzelm@58900
   225
  }
wenzelm@29449
   226
}