added Keyword.is_heading (cf. Scala version);
authorwenzelm
Sat, 06 Nov 2010 20:18:06 +0100
changeset 40397 4ad71312a192
parent 40396 c4c6fa6819aa
child 40398 cdda2847a91e
added Keyword.is_heading (cf. Scala version); tuned;
src/Pure/Isar/keyword.ML
--- 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;
 
-