clarified keyword categories;
authorwenzelm
Fri Nov 07 17:31:01 2014 +0100 (2014-11-07)
changeset 589313097ec653547
parent 58930 13d3eb07a17a
child 58932 5fd496c26e3b
clarified keyword categories;
tuned;
src/Doc/Datatypes/Datatypes.thy
src/Doc/System/Sessions.thy
src/Doc/antiquote_setup.ML
src/Pure/Isar/keyword.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Nov 07 16:55:09 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Nov 07 17:31:01 2014 +0100
     1.3 @@ -1538,7 +1538,7 @@
     1.4  
     1.5  \item
     1.6  Introduce a fully unspecified constant @{text "un_D\<^sub>0 \<Colon> 'a"} using
     1.7 -@{keyword consts}.
     1.8 +@{command consts}.
     1.9  
    1.10  \item
    1.11  Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
    1.12 @@ -2597,7 +2597,7 @@
    1.13  
    1.14  text {*
    1.15  \noindent
    1.16 -Using \keyw{print_theorems} and @{keyword print_bnfs}, we can contemplate and
    1.17 +Using \keyw{print_theorems} and @{command print_bnfs}, we can contemplate and
    1.18  show the world what we have achieved.
    1.19  
    1.20  This particular example does not need any nonemptiness witness, because the
     2.1 --- a/src/Doc/System/Sessions.thy	Fri Nov 07 16:55:09 2014 +0100
     2.2 +++ b/src/Doc/System/Sessions.thy	Fri Nov 07 17:31:01 2014 +0100
     2.3 @@ -126,7 +126,7 @@
     2.4    files that are involved in the processing of this session.  This
     2.5    should cover anything outside the formal content of the theory
     2.6    sources.  In contrast, files that are loaded formally
     2.7 -  within a theory, e.g.\ via @{keyword "ML_file"}, need not be
     2.8 +  within a theory, e.g.\ via @{command "ML_file"}, need not be
     2.9    declared again.
    2.10  
    2.11    \item \isakeyword{document_files}~@{text "("}\isakeyword{in}~@{text
     3.1 --- a/src/Doc/antiquote_setup.ML	Fri Nov 07 16:55:09 2014 +0100
     3.2 +++ b/src/Doc/antiquote_setup.ML	Fri Nov 07 17:31:01 2014 +0100
     3.3 @@ -192,7 +192,7 @@
     3.4  fun no_check _ _ = true;
     3.5  
     3.6  fun is_keyword ctxt (name, _) =
     3.7 -  Keyword.is_literal (Thy_Header.get_keywords' ctxt) name;
     3.8 +  Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name;
     3.9  
    3.10  fun check_command ctxt (name, pos) =
    3.11    let
     4.1 --- a/src/Pure/Isar/keyword.ML	Fri Nov 07 16:55:09 2014 +0100
     4.2 +++ b/src/Pure/Isar/keyword.ML	Fri Nov 07 17:31:01 2014 +0100
     4.3 @@ -36,8 +36,9 @@
     4.4    val empty_keywords: keywords
     4.5    val merge_keywords: keywords * keywords -> keywords
     4.6    val add_keywords: (string * spec option) list -> keywords -> keywords
     4.7 +  val is_keyword: keywords -> string -> bool
     4.8 +  val is_command: keywords -> string -> bool
     4.9    val is_literal: keywords -> string -> bool
    4.10 -  val is_command: keywords -> string -> bool
    4.11    val command_files: keywords -> string -> Path.T -> Path.T list
    4.12    val command_tags: keywords -> string -> string list
    4.13    val is_diag: keywords -> string -> bool
    4.14 @@ -159,21 +160,19 @@
    4.15          in (minor, major', commands') end)));
    4.16  
    4.17  
    4.18 -(* lookup keywords *)
    4.19 +(* keyword status *)
    4.20  
    4.21 -fun is_literal keywords s =
    4.22 -  let
    4.23 -    val minor = minor_keywords keywords;
    4.24 -    val major = major_keywords keywords;
    4.25 -    val syms = Symbol.explode s;
    4.26 -  in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
    4.27 +fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s);
    4.28 +fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
    4.29 +fun is_literal keywords = is_keyword keywords orf is_command keywords;
    4.30  
    4.31 -fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
    4.32  
    4.33 -fun command_keyword (Keywords {commands, ...}) = Symtab.lookup commands;
    4.34 +(* command kind *)
    4.35 +
    4.36 +fun command_kind (Keywords {commands, ...}) = Symtab.lookup commands;
    4.37  
    4.38  fun command_files keywords name path =
    4.39 -  (case command_keyword keywords name of
    4.40 +  (case command_kind keywords name of
    4.41      NONE => []
    4.42    | SOME {kind, files, ...} =>
    4.43        if kind <> thy_load then []
    4.44 @@ -181,7 +180,7 @@
    4.45        else map (fn ext => Path.ext ext path) files);
    4.46  
    4.47  fun command_tags keywords name =
    4.48 -  (case command_keyword keywords name of
    4.49 +  (case command_kind keywords name of
    4.50      SOME {tags, ...} => tags
    4.51    | NONE => []);
    4.52  
    4.53 @@ -192,7 +191,7 @@
    4.54    let
    4.55      val tab = Symtab.make_set ks;
    4.56      fun pred keywords name =
    4.57 -      (case command_keyword keywords name of
    4.58 +      (case command_kind keywords name of
    4.59          NONE => false
    4.60        | SOME {kind, ...} => Symtab.defined tab kind);
    4.61    in pred end;