src/Pure/Isar/keyword.ML

 *)
 
 signature KEYWORD =
 sig
   val diag: string
-  val heading: string
+  val document_heading: string
+  val document_body: string
+  val document_raw: string
   val thy_begin: string
   val thy_end: string
   val thy_decl: string
   val thy_decl_block: string
   val thy_load: string

   val is_keyword: keywords -> string -> bool
   val is_command: keywords -> string -> bool
   val is_literal: keywords -> string -> bool
   val command_files: keywords -> string -> Path.T -> Path.T list
   val command_tags: keywords -> string -> string list
+  val is_vacuous: keywords -> string -> bool
   val is_diag: keywords -> string -> bool
-  val is_heading: keywords -> string -> bool
+  val is_document_heading: keywords -> string -> bool
+  val is_document_body: keywords -> string -> bool
+  val is_document_raw: keywords -> string -> bool
   val is_theory_begin: keywords -> string -> bool
   val is_theory_load: keywords -> string -> bool
   val is_theory: keywords -> string -> bool
   val is_theory_body: keywords -> string -> bool
   val is_proof: keywords -> string -> bool

 (** keyword classification **)
 
 (* kinds *)
 
 val diag = "diag";
-val heading = "heading";
+val document_heading = "document_heading";
+val document_body = "document_body";
+val document_raw = "document_raw";
 val thy_begin = "thy_begin";
 val thy_end = "thy_end";
 val thy_decl = "thy_decl";
 val thy_decl_block = "thy_decl_block";
 val thy_load = "thy_load";

 val prf_asm_goal = "prf_asm_goal";
 val prf_asm_goal_script = "prf_asm_goal_script";
 val prf_script = "prf_script";
 
 val kinds =
-  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
-    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+  [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, prf_open,
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 
 (* specifications *)
 
 type T =

       (case command_kind keywords name of
         NONE => false
       | SOME {kind, ...} => Symtab.defined tab kind);
   in pred end;
 
+val is_vacuous = command_category [diag, document_heading, document_body, document_raw];
+
 val is_diag = command_category [diag];
 
-val is_heading = command_category [heading];
+val is_document_heading = command_category [document_heading];
+val is_document_body = command_category [document_body];
+val is_document_raw = command_category [document_raw];
+val is_document = command_category [document_heading, document_body, document_raw];
 
 val is_theory_begin = command_category [thy_begin];
 
 val is_theory_load = command_category [thy_load];
 

 val is_proof = command_category
   [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
     prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_proof_body = command_category
-  [diag, heading, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm,
-    prf_asm_goal, prf_asm_goal_script, prf_script];
+  [diag, document_heading, document_body, document_raw, prf_block, prf_open, prf_close,
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_theory_goal = command_category [thy_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];