added Keyword.is_heading (cf. Scala version);
tuned;
--- a/src/Pure/Isar/keyword.ML Sat Nov 06 19:37:31 2010 +0100
+++ b/src/Pure/Isar/keyword.ML Sat Nov 06 20:18:06 2010 +0100
@@ -51,6 +51,7 @@
val is_diag: string -> bool
val is_control: string -> bool
val is_regular: string -> bool
+ val is_heading: string -> bool
val is_theory_begin: string -> bool
val is_theory: string -> bool
val is_proof: string -> bool
@@ -192,7 +193,9 @@
val is_diag = command_category [diag];
val is_control = command_category [control];
-fun is_regular name = not (is_diag name orelse is_control name);
+val is_regular = not o command_category [diag, control];
+
+val is_heading = command_category [thy_heading, prf_heading];
val is_theory_begin = command_category [thy_begin];
@@ -211,4 +214,3 @@
end;
-