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