src/Pure/Isar/keyword.scala
author wenzelm
Sun Nov 26 13:19:52 2017 +0100 (17 months ago)
changeset 67090 0ec94bb9cec4
parent 66919 1f93e376aeb6
child 69913 ca515cf61651
permissions -rw-r--r--
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
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@65385
   103
wenzelm@65385
   104
    override def toString: String =
wenzelm@65385
   105
      kind +
wenzelm@65385
   106
        (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") +
wenzelm@65385
   107
        (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", ""))
wenzelm@65384
   108
  }
wenzelm@63429
   109
wenzelm@58900
   110
  object Keywords
wenzelm@58900
   111
  {
wenzelm@58900
   112
    def empty: Keywords = new Keywords()
wenzelm@58900
   113
  }
wenzelm@58900
   114
wenzelm@58900
   115
  class Keywords private(
wenzelm@63441
   116
    val kinds: Map[String, String] = Map.empty,
wenzelm@63441
   117
    val load_commands: Map[String, List[String]] = Map.empty)
wenzelm@58900
   118
  {
wenzelm@58901
   119
    override def toString: String =
wenzelm@58901
   120
    {
wenzelm@63441
   121
      val entries =
wenzelm@63441
   122
        for ((name, kind) <- kinds.toList.sortBy(_._1)) yield {
wenzelm@63441
   123
          val exts = load_commands.getOrElse(name, Nil)
wenzelm@63441
   124
          val kind_decl =
wenzelm@63441
   125
            if (kind == "") ""
wenzelm@63441
   126
            else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")")
wenzelm@63441
   127
          quote(name) + kind_decl
wenzelm@63430
   128
        }
wenzelm@63441
   129
      entries.mkString("keywords\n  ", " and\n  ", "")
wenzelm@58900
   130
    }
wenzelm@58900
   131
wenzelm@58900
   132
wenzelm@59073
   133
    /* merge */
wenzelm@59073
   134
wenzelm@67090
   135
    def is_empty: Boolean = kinds.isEmpty
wenzelm@59073
   136
wenzelm@59073
   137
    def ++ (other: Keywords): Keywords =
wenzelm@59073
   138
      if (this eq other) this
wenzelm@59073
   139
      else if (is_empty) other
wenzelm@59073
   140
      else {
wenzelm@63441
   141
        val kinds1 =
wenzelm@63441
   142
          if (kinds eq other.kinds) kinds
wenzelm@63441
   143
          else if (kinds.isEmpty) other.kinds
wenzelm@63441
   144
          else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@63441
   145
        val load_commands1 =
wenzelm@63441
   146
          if (load_commands eq other.load_commands) load_commands
wenzelm@63441
   147
          else if (load_commands.isEmpty) other.load_commands
wenzelm@63441
   148
          else
wenzelm@63441
   149
            (load_commands /: other.load_commands) {
wenzelm@63441
   150
              case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@67090
   151
        new Keywords(kinds1, load_commands1)
wenzelm@59073
   152
      }
wenzelm@59073
   153
wenzelm@59073
   154
wenzelm@58902
   155
    /* add keywords */
wenzelm@58902
   156
wenzelm@63441
   157
    def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords =
wenzelm@63441
   158
    {
wenzelm@63441
   159
      val kinds1 = kinds + (name -> kind)
wenzelm@63441
   160
      val load_commands1 =
wenzelm@66919
   161
        if (kind == THY_LOAD) {
wenzelm@66919
   162
          if (!Symbol.iterator(name).forall(Symbol.is_ascii(_)))
wenzelm@66919
   163
            error("Bad theory load command " + quote(name))
wenzelm@66919
   164
          load_commands + (name -> exts)
wenzelm@66919
   165
        }
wenzelm@63441
   166
        else load_commands
wenzelm@67090
   167
      new Keywords(kinds1, load_commands1)
wenzelm@63441
   168
    }
wenzelm@58902
   169
wenzelm@58928
   170
    def add_keywords(header: Thy_Header.Keywords): Keywords =
wenzelm@58928
   171
      (this /: header) {
wenzelm@65384
   172
        case (keywords, (name, spec)) =>
wenzelm@65384
   173
          if (spec.is_none)
wenzelm@65384
   174
            keywords + Symbol.decode(name) + Symbol.encode(name)
wenzelm@65384
   175
          else
wenzelm@65384
   176
            keywords +
wenzelm@65384
   177
              (Symbol.decode(name), spec.kind, spec.exts) +
wenzelm@65384
   178
              (Symbol.encode(name), spec.kind, spec.exts)
wenzelm@58928
   179
      }
wenzelm@58928
   180
wenzelm@58902
   181
wenzelm@58901
   182
    /* command kind */
wenzelm@58900
   183
wenzelm@63424
   184
    def is_command(token: Token, check_kind: String => Boolean): Boolean =
wenzelm@63424
   185
      token.is_command &&
wenzelm@63441
   186
        (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false })
wenzelm@63441
   187
wenzelm@63441
   188
    def is_before_command(token: Token): Boolean =
wenzelm@63441
   189
      token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
wenzelm@59701
   190
wenzelm@63430
   191
    def is_quasi_command(token: Token): Boolean =
wenzelm@63441
   192
      token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
wenzelm@63430
   193
wenzelm@63809
   194
    def is_indent_command(token: Token): Boolean =
wenzelm@63809
   195
      token.is_begin_or_command || is_quasi_command(token)
wenzelm@63809
   196
wenzelm@58900
   197
wenzelm@58900
   198
    /* load commands */
wenzelm@58900
   199
wenzelm@58900
   200
    def load_commands_in(text: String): Boolean =
wenzelm@58900
   201
      load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
wenzelm@67090
   202
wenzelm@67090
   203
wenzelm@67090
   204
    /* lexicons */
wenzelm@67090
   205
wenzelm@67090
   206
    private def make_lexicon(is_minor: Boolean): Scan.Lexicon =
wenzelm@67090
   207
      (Scan.Lexicon.empty /: kinds)(
wenzelm@67090
   208
        {
wenzelm@67090
   209
          case (lex, (name, kind)) =>
wenzelm@67090
   210
            if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor)
wenzelm@67090
   211
              lex + name
wenzelm@67090
   212
            else lex
wenzelm@67090
   213
        })
wenzelm@67090
   214
wenzelm@67090
   215
    lazy val minor: Scan.Lexicon = make_lexicon(true)
wenzelm@67090
   216
    lazy val major: Scan.Lexicon = make_lexicon(false)
wenzelm@58900
   217
  }
wenzelm@29449
   218
}