# HG changeset patch
# User wenzelm
# Date 1468144110 -7200
# Node ID 9c5fcd355a2d49b250f9adf9c7241c3211798d7d
# Parent  baedd4724f08f525dfbfc51269ae1a6202a6d4bf
support for quasi_command keywords;

diff -r baedd4724f08 -r 9c5fcd355a2d src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Sun Jul 10 11:18:35 2016 +0200
+++ b/src/Pure/Isar/keyword.ML	Sun Jul 10 11:48:30 2016 +0200
@@ -32,8 +32,10 @@
   val prf_script: string
   val prf_script_goal: string
   val prf_script_asm_goal: string
+  val quasi_command: string
   type spec = (string * string list) * string list
   val no_spec: spec
+  val quasi_command_spec: spec
   type keywords
   val minor_keywords: keywords -> Scan.lexicon
   val major_keywords: keywords -> Scan.lexicon
@@ -105,8 +107,9 @@
 val prf_script = "prf_script";
 val prf_script_goal = "prf_script_goal";
 val prf_script_asm_goal = "prf_script_asm_goal";
+val quasi_command = "quasi_command";
 
-val kinds =
+val command_kinds =
   [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
     thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block,
     next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script,
@@ -118,6 +121,7 @@
 type spec = (string * string list) * string list;
 
 val no_spec: spec = (("", []), []);
+val quasi_command_spec: spec = ((quasi_command, []), []);
 
 type entry =
  {pos: Position.T,
@@ -127,7 +131,7 @@
   tags: string list};
 
 fun check_spec pos ((kind, files), tags) : entry =
-  if not (member (op =) kinds kind) then
+  if not (member (op =) command_kinds kind) then
     error ("Unknown outer syntax keyword kind " ^ quote kind)
   else if not (null files) andalso kind <> thy_load then
     error ("Illegal specification of files for " ^ quote kind)
@@ -171,7 +175,7 @@
 
 val add_keywords =
   fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
-    if kind = "" then
+    if kind = "" orelse kind = quasi_command then
       let
         val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
       in (minor', major, commands) end
diff -r baedd4724f08 -r 9c5fcd355a2d src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Sun Jul 10 11:18:35 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Sun Jul 10 11:48:30 2016 +0200
@@ -39,6 +39,7 @@
   val PRF_SCRIPT = "prf_script"
   val PRF_SCRIPT_GOAL = "prf_script_goal"
   val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
+  val QUASI_COMMAND = "quasi_command"
 
 
   /* command categories */
@@ -89,6 +90,7 @@
   type Spec = ((String, List[String]), List[String])
 
   val no_spec: Spec = (("", Nil), Nil)
+  val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil)
 
   object Keywords
   {
@@ -98,17 +100,22 @@
   class Keywords private(
     val minor: Scan.Lexicon = Scan.Lexicon.empty,
     val major: Scan.Lexicon = Scan.Lexicon.empty,
+    protected val quasi_commands: Set[String] = Set.empty,
     protected val commands: Map[String, (String, List[String])] = Map.empty)
   {
     override def toString: String =
     {
-      val keywords1 = minor.iterator.map(quote(_)).toList
+      val keywords1 =
+        for (name <- minor.iterator.toList) yield {
+          if (quasi_commands.contains(name)) (name, quote(name) + " :: \"quasi_command\"")
+          else (name, quote(name))
+        }
       val keywords2 =
-        for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield {
-          quote(name) + " :: " + quote(kind) +
-          (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
+        for ((name, (kind, files)) <- commands.toList) yield {
+          (name, quote(name) + " :: " + quote(kind) +
+            (if (files.isEmpty) "" else " (" + commas_quote(files) + ")"))
         }
-      (keywords1 ::: keywords2).mkString("keywords\n  ", " and\n  ", "")
+      (keywords1 ::: keywords2).sortBy(_._1).map(_._2).mkString("keywords\n  ", " and\n  ", "")
     }
 
 
@@ -122,22 +129,25 @@
       else {
         val minor1 = minor ++ other.minor
         val major1 = major ++ other.major
+        val quasi_commands1 = quasi_commands ++ other.quasi_commands
         val commands1 =
           if (commands eq other.commands) commands
           else if (commands.isEmpty) other.commands
           else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
-        new Keywords(minor1, major1, commands1)
+        new Keywords(minor1, major1, quasi_commands1, commands1)
       }
 
 
     /* add keywords */
 
     def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords =
-      if (kind == "") new Keywords(minor + name, major, commands)
+      if (kind == "") new Keywords(minor + name, major, quasi_commands, commands)
+      else if (kind == QUASI_COMMAND)
+        new Keywords(minor + name, major, quasi_commands + name, commands)
       else {
         val major1 = major + name
         val commands1 = commands + (name -> (kind, tags))
-        new Keywords(minor, major1, commands1)
+        new Keywords(minor, major1, quasi_commands, commands1)
       }
 
     def add_keywords(header: Thy_Header.Keywords): Keywords =
@@ -156,6 +166,9 @@
       token.is_command &&
         (command_kind(token.source) match { case Some(k) => check_kind(k) case None => false })
 
+    def is_quasi_command(token: Token): Boolean =
+      token.is_keyword && quasi_commands.contains(token.source)
+
 
     /* load commands */