# HG changeset patch
# User wenzelm
# Date 1415377861 -3600
# Node ID 3097ec6535477aaff7b42842e61312937cb3c67f
# Parent  13d3eb07a17adf70f3a288c151c1016b5283a69b
clarified keyword categories;
tuned;

diff -r 13d3eb07a17a -r 3097ec653547 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Nov 07 16:55:09 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Nov 07 17:31:01 2014 +0100
@@ -1538,7 +1538,7 @@
 
 \item
 Introduce a fully unspecified constant @{text "un_D\<^sub>0 \<Colon> 'a"} using
-@{keyword consts}.
+@{command consts}.
 
 \item
 Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
@@ -2597,7 +2597,7 @@
 
 text {*
 \noindent
-Using \keyw{print_theorems} and @{keyword print_bnfs}, we can contemplate and
+Using \keyw{print_theorems} and @{command print_bnfs}, we can contemplate and
 show the world what we have achieved.
 
 This particular example does not need any nonemptiness witness, because the
diff -r 13d3eb07a17a -r 3097ec653547 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Fri Nov 07 16:55:09 2014 +0100
+++ b/src/Doc/System/Sessions.thy	Fri Nov 07 17:31:01 2014 +0100
@@ -126,7 +126,7 @@
   files that are involved in the processing of this session.  This
   should cover anything outside the formal content of the theory
   sources.  In contrast, files that are loaded formally
-  within a theory, e.g.\ via @{keyword "ML_file"}, need not be
+  within a theory, e.g.\ via @{command "ML_file"}, need not be
   declared again.
 
   \item \isakeyword{document_files}~@{text "("}\isakeyword{in}~@{text
diff -r 13d3eb07a17a -r 3097ec653547 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Fri Nov 07 16:55:09 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Fri Nov 07 17:31:01 2014 +0100
@@ -192,7 +192,7 @@
 fun no_check _ _ = true;
 
 fun is_keyword ctxt (name, _) =
-  Keyword.is_literal (Thy_Header.get_keywords' ctxt) name;
+  Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name;
 
 fun check_command ctxt (name, pos) =
   let
diff -r 13d3eb07a17a -r 3097ec653547 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Fri Nov 07 16:55:09 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Fri Nov 07 17:31:01 2014 +0100
@@ -36,8 +36,9 @@
   val empty_keywords: keywords
   val merge_keywords: keywords * keywords -> keywords
   val add_keywords: (string * spec option) list -> keywords -> keywords
+  val is_keyword: keywords -> string -> bool
+  val is_command: keywords -> string -> bool
   val is_literal: keywords -> string -> bool
-  val is_command: keywords -> string -> bool
   val command_files: keywords -> string -> Path.T -> Path.T list
   val command_tags: keywords -> string -> string list
   val is_diag: keywords -> string -> bool
@@ -159,21 +160,19 @@
         in (minor, major', commands') end)));
 
 
-(* lookup keywords *)
+(* keyword status *)
 
-fun is_literal keywords s =
-  let
-    val minor = minor_keywords keywords;
-    val major = major_keywords keywords;
-    val syms = Symbol.explode s;
-  in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
+fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s);
+fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
+fun is_literal keywords = is_keyword keywords orf is_command keywords;
 
-fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
 
-fun command_keyword (Keywords {commands, ...}) = Symtab.lookup commands;
+(* command kind *)
+
+fun command_kind (Keywords {commands, ...}) = Symtab.lookup commands;
 
 fun command_files keywords name path =
-  (case command_keyword keywords name of
+  (case command_kind keywords name of
     NONE => []
   | SOME {kind, files, ...} =>
       if kind <> thy_load then []
@@ -181,7 +180,7 @@
       else map (fn ext => Path.ext ext path) files);
 
 fun command_tags keywords name =
-  (case command_keyword keywords name of
+  (case command_kind keywords name of
     SOME {tags, ...} => tags
   | NONE => []);
 
@@ -192,7 +191,7 @@
   let
     val tab = Symtab.make_set ks;
     fun pred keywords name =
-      (case command_keyword keywords name of
+      (case command_kind keywords name of
         NONE => false
       | SOME {kind, ...} => Symtab.defined tab kind);
   in pred end;