# HG changeset patch
# User wenzelm
# Date 1426427161 -3600
# Node ID 8ab877c9199223240dd446188ffb55bab9381145
# Parent  d887abcc7c24a41f28a6963759d5a68bc30f1e3a
more command categories, as in ML;
tuned;

diff -r d887abcc7c24 -r 8ab877c91992 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Sun Mar 15 12:49:20 2015 +0100
+++ b/src/Pure/Isar/keyword.ML	Sun Mar 15 14:46:01 2015 +0100
@@ -249,4 +249,3 @@
 fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
 
 end;
-
diff -r d887abcc7c24 -r 8ab877c91992 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Sun Mar 15 12:49:20 2015 +0100
+++ b/src/Pure/Isar/keyword.scala	Sun Mar 15 14:46:01 2015 +0100
@@ -53,6 +53,8 @@
   val theory_begin = Set(THY_BEGIN)
   val theory_end = Set(THY_END)
 
+  val theory_load = Set(THY_LOAD)
+
   val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
 
   val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
@@ -142,6 +144,12 @@
 
     def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
 
+    def is_command_kind(name: String, pred: String => Boolean): Boolean =
+      command_kind(name) match {
+        case Some(kind) => pred(kind)
+        case None => false
+      }
+
 
     /* load commands */
 
@@ -158,4 +166,3 @@
       load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
   }
 }
-
diff -r d887abcc7c24 -r 8ab877c91992 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sun Mar 15 12:49:20 2015 +0100
+++ b/src/Pure/Isar/token.scala	Sun Mar 15 14:46:01 2015 +0100
@@ -212,8 +212,7 @@
 {
   def is_command: Boolean = kind == Token.Kind.COMMAND
   def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
-    is_command &&
-      (keywords.command_kind(source) match { case Some(k) => pred(k) case None => false })
+    is_command && keywords.is_command_kind(source, pred)
   def is_keyword: Boolean = kind == Token.Kind.KEYWORD
   def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   def is_ident: Boolean = kind == Token.Kind.IDENT