src/Pure/Isar/keyword.scala
author wenzelm
Tue Dec 09 21:14:11 2014 +0100 (2014-12-09)
changeset 59122 c1dbcde94cd2
parent 59073 dcecfcc56dce
child 59700 d887abcc7c24
permissions -rw-r--r--
tuned signature;
     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 PRF_OPEN = "prf_open"
    33   val PRF_CLOSE = "prf_close"
    34   val PRF_CHAIN = "prf_chain"
    35   val PRF_DECL = "prf_decl"
    36   val PRF_ASM = "prf_asm"
    37   val PRF_ASM_GOAL = "prf_asm_goal"
    38   val PRF_ASM_GOAL_SCRIPT = "prf_asm_goal_script"
    39   val PRF_SCRIPT = "prf_script"
    40 
    41 
    42   /* categories */
    43 
    44   val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
    45 
    46   val diag = Set(DIAG)
    47 
    48   val document_heading = Set(DOCUMENT_HEADING)
    49   val document_body = Set(DOCUMENT_BODY)
    50   val document_raw = Set(DOCUMENT_RAW)
    51   val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
    52 
    53   val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
    54 
    55   val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
    56 
    57   val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
    58 
    59   val proof =
    60     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
    61       PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    62 
    63   val proof_body =
    64     Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
    65       PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    66 
    67   val theory_goal = Set(THY_GOAL)
    68   val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
    69   val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
    70   val qed_global = Set(QED_GLOBAL)
    71 
    72 
    73 
    74   /** keyword tables **/
    75 
    76   type Spec = ((String, List[String]), List[String])
    77 
    78   object Keywords
    79   {
    80     def empty: Keywords = new Keywords()
    81   }
    82 
    83   class Keywords private(
    84     val minor: Scan.Lexicon = Scan.Lexicon.empty,
    85     val major: Scan.Lexicon = Scan.Lexicon.empty,
    86     protected val commands: Map[String, (String, List[String])] = Map.empty)
    87   {
    88     override def toString: String =
    89     {
    90       val keywords1 = minor.iterator.map(quote(_)).toList
    91       val keywords2 =
    92         for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield {
    93           quote(name) + " :: " + quote(kind) +
    94           (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
    95         }
    96       (keywords1 ::: keywords2).mkString("keywords\n  ", " and\n  ", "")
    97     }
    98 
    99 
   100     /* merge */
   101 
   102     def is_empty: Boolean = minor.is_empty && major.is_empty
   103 
   104     def ++ (other: Keywords): Keywords =
   105       if (this eq other) this
   106       else if (is_empty) other
   107       else {
   108         val minor1 = minor ++ other.minor
   109         val major1 = major ++ other.major
   110         val commands1 =
   111           if (commands eq other.commands) commands
   112           else if (commands.isEmpty) other.commands
   113           else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
   114         new Keywords(minor1, major1, commands1)
   115       }
   116 
   117 
   118     /* add keywords */
   119 
   120     def + (name: String): Keywords = new Keywords(minor + name, major, commands)
   121     def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
   122     def + (name: String, kind_tags: (String, List[String])): Keywords =
   123     {
   124       val major1 = major + name
   125       val commands1 = commands + (name -> kind_tags)
   126       new Keywords(minor, major1, commands1)
   127     }
   128 
   129     def add_keywords(header: Thy_Header.Keywords): Keywords =
   130       (this /: header) {
   131         case (keywords, (name, None, _)) =>
   132           keywords + Symbol.decode(name) + Symbol.encode(name)
   133         case (keywords, (name, Some((kind_tags, _)), _)) =>
   134           keywords + (Symbol.decode(name), kind_tags) + (Symbol.encode(name), kind_tags)
   135       }
   136 
   137 
   138     /* command kind */
   139 
   140     def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
   141 
   142 
   143     /* load commands */
   144 
   145     def load_command(name: String): Option[List[String]] =
   146       commands.get(name) match {
   147         case Some((THY_LOAD, exts)) => Some(exts)
   148         case _ => None
   149       }
   150 
   151     private lazy val load_commands: List[(String, List[String])] =
   152       (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList
   153 
   154     def load_commands_in(text: String): Boolean =
   155       load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
   156   }
   157 }
   158