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