# HG changeset patch
# User wenzelm
# Date 1222804967 -7200
# Node ID f12c1c68ec8eb6205a418d56ffc57a459a760a8a
# Parent  29b2886114fb3dc9fc2df8002bcc168561b097d5
more command categories;
tuned;

diff -r 29b2886114fb -r f12c1c68ec8e src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Tue Sep 30 22:02:45 2008 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Tue Sep 30 22:02:47 2008 +0200
@@ -50,6 +50,10 @@
   val is_theory: string -> bool
   val is_proof: string -> bool
   val is_diag: string -> bool
+  val is_theory_goal: string -> bool
+  val is_proof_goal: string -> bool
+  val is_qed: string -> bool
+  val is_qed_global: string -> bool
 end;
 
 structure OuterKeyword: OUTER_KEYWORD =
@@ -163,20 +167,25 @@
   Output.status (Pretty.string_of (report_command (name, kind))));
 
 
-(* overall category *)
+(* command categories *)
 
 fun command_category ks name =
   (case command_keyword name of
     NONE => false
-  | SOME k => member (op =) ks (kind_of k));
+  | SOME k => member (op = o pairself kind_of) ks k);
 
 val is_theory = command_category
-  (map kind_of [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal]);
+  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal];
 
 val is_proof = command_category
-  (map kind_of [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]);
+  [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+
+val is_diag = command_category [diag];
 
-val is_diag = command_category [kind_of diag];
+val is_theory_goal = command_category [thy_goal];
+val is_proof_goal = command_category [prf_goal, prf_asm_goal];
+val is_qed = command_category [qed, qed_block];
+val is_qed_global = command_category [qed_global];
 
 end;