# HG changeset patch
# User wenzelm
# Date 1289071086 -3600
# Node ID 4ad71312a192ef7f2cd51e1fe48c9e5674eed8c8
# Parent  c4c6fa6819aa9455b7221e3986b2b94fa57bb758
added Keyword.is_heading (cf. Scala version);
tuned;

diff -r c4c6fa6819aa -r 4ad71312a192 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;
 
-