# HG changeset patch
# User wenzelm
# Date 1428330644 -7200
# Node ID 343905de27b19a718bf665be44a40a0f011d3f3e
# Parent  b65c4370f8314e4d7b3afa01ac59fcabebaac6bb
clarified command keyword markup;

diff -r b65c4370f831 -r 343905de27b1 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Apr 06 16:00:19 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 06 16:30:44 2015 +0200
@@ -173,8 +173,8 @@
 
 local
 
-fun hide_names command_spec what hide parse prep =
-  Outer_Syntax.command command_spec ("hide " ^ what ^ " from name space")
+fun hide_names command_keyword what hide parse prep =
+  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
     ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
       (Toplevel.theory (fn thy =>
         let val ctxt = Proof_Context.init_global thy
diff -r b65c4370f831 -r 343905de27b1 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon Apr 06 16:00:19 2015 +0200
+++ b/src/Pure/Isar/keyword.ML	Mon Apr 06 16:30:44 2015 +0200
@@ -189,7 +189,7 @@
   lookup_command keywords name
   |> Option.map (fn {pos, id, ...} =>
       Markup.properties (Position.entity_properties_of false id pos)
-        (Markup.entity Markup.commandN name));
+        (Markup.entity Markup.command_keywordN name));
 
 fun command_kind keywords = Option.map #kind o lookup_command keywords;
 
diff -r b65c4370f831 -r 343905de27b1 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 16:00:19 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 16:30:44 2015 +0200
@@ -8,16 +8,16 @@
 sig
   val help: theory -> string list -> unit
   val print_commands: theory -> unit
-  type command_spec = string * Position.T
-  val command: command_spec -> string ->
+  type command_keyword = string * Position.T
+  val command: command_keyword -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val local_theory': command_spec -> string ->
+  val local_theory': command_keyword -> string ->
     (bool -> local_theory -> local_theory) parser -> unit
-  val local_theory: command_spec -> string ->
+  val local_theory: command_keyword -> string ->
     (local_theory -> local_theory) parser -> unit
-  val local_theory_to_proof': command_spec -> string ->
+  val local_theory_to_proof': command_keyword -> string ->
     (bool -> local_theory -> Proof.state) parser -> unit
-  val local_theory_to_proof: command_spec -> string ->
+  val local_theory_to_proof: command_keyword -> string ->
     (local_theory -> Proof.state) parser -> unit
   val parse: theory -> Position.T -> string -> Toplevel.transition list
   val parse_tokens: theory -> Token.T list -> Toplevel.transition list
@@ -134,7 +134,7 @@
 
 (* implicit theory setup *)
 
-type command_spec = string * Position.T;
+type command_keyword = string * Position.T;
 
 fun raw_command (name, pos) comment command_parser =
   let val setup = add_command name (new_command comment command_parser pos)
@@ -143,8 +143,8 @@
 fun command (name, pos) comment parse =
   raw_command (name, pos) comment (Parser parse);
 
-fun local_theory_command trans command_spec comment parse =
-  raw_command command_spec comment
+fun local_theory_command trans command_keyword comment parse =
+  raw_command command_keyword comment
     (Private_Parser (fn private =>
       Parse.opt_target -- parse >> (fn (target, f) => trans private target f)));
 
diff -r b65c4370f831 -r 343905de27b1 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Apr 06 16:00:19 2015 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Apr 06 16:30:44 2015 +0200
@@ -115,6 +115,7 @@
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
   val inputN: string val input: bool -> Properties.T -> T
+  val command_keywordN: string val command_keyword: T
   val commandN: string val command: T
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
@@ -464,6 +465,7 @@
 
 (* outer syntax *)
 
+val (command_keywordN, command_keyword) = markup_elem "command_keyword";
 val (commandN, command) = markup_elem "command";
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";