# HG changeset patch
# User wenzelm
# Date 1406916900 -7200
# Node ID 43ff8638c02cd767f39e41a87366b075b938fc5e
# Parent  0d295e339f52d94f7d803d94508998d4f11846c3
more keyword categories (as in ML);

diff -r 0d295e339f52 -r 43ff8638c02c src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Thu Jul 31 22:02:21 2014 +0200
+++ b/src/Pure/Isar/keyword.scala	Fri Aug 01 20:15:00 2014 +0200
@@ -44,14 +44,20 @@
 
   /* categories */
 
-  val minor = Set(MINOR)
+  val diag = Set(DIAG)
   val control = Set(CONTROL)
-  val diag = Set(DIAG)
+
+  val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
+    PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
+
   val theory =
     Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
       THY_DECL, THY_GOAL)
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
+  val theory_body =
+    Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL)
+
   val proof =
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
       PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
@@ -60,5 +66,14 @@
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
       PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
+
+  val proof_body =
+    Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN,
+      PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+
+  val theory_goal = Set(THY_GOAL)
+  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
+  val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
+  val qed_global = Set(QED_GLOBAL)
 }