src/Pure/Isar/keyword.ML

--- a/src/Pure/Isar/keyword.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/Isar/keyword.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -37,10 +37,11 @@
   val no_command_keywords: keywords -> keywords
   val empty_keywords: keywords
   val merge_keywords: keywords * keywords -> keywords
-  val add_keywords: (string * spec option) list -> keywords -> keywords
+  val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
   val is_keyword: keywords -> string -> bool
   val is_command: keywords -> string -> bool
   val is_literal: keywords -> string -> bool
+  val command_markup: keywords -> string -> Markup.T option
   val command_kind: keywords -> string -> string option
   val command_files: keywords -> string -> Path.T -> Path.T list
   val command_tags: keywords -> string -> string list
@@ -105,19 +106,21 @@
 
 (* specifications *)
 
-type T =
- {kind: string,
+type spec = (string * string list) * string list;
+
+type entry =
+ {pos: Position.T,
+  id: serial,
+  kind: string,
   files: string list,  (*extensions of embedded files*)
   tags: string list};
 
-type spec = (string * string list) * string list;
-
-fun check_spec ((kind, files), tags) : T =
+fun check_spec pos ((kind, files), tags) : entry =
   if not (member (op =) kinds kind) then
     error ("Unknown outer syntax keyword kind " ^ quote kind)
   else if not (null files) andalso kind <> thy_load then
     error ("Illegal specification of files for " ^ quote kind)
-  else {kind = kind, files = files, tags = tags};
+  else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
 
 
 
@@ -128,7 +131,7 @@
 datatype keywords = Keywords of
  {minor: Scan.lexicon,
   major: Scan.lexicon,
-  commands: T Symtab.table};
+  commands: entry Symtab.table};
 
 fun minor_keywords (Keywords {minor, ...}) = minor;
 fun major_keywords (Keywords {major, ...}) = major;
@@ -157,7 +160,7 @@
     Symtab.merge (K true) (commands1, commands2));
 
 val add_keywords =
-  fold (fn (name, opt_spec) => map_keywords (fn (minor, major, commands) =>
+  fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) =>
     (case opt_spec of
       NONE =>
         let
@@ -165,9 +168,9 @@
         in (minor', major, commands) end
     | SOME spec =>
         let
-          val kind = check_spec spec;
+          val entry = check_spec pos spec;
           val major' = Scan.extend_lexicon (Symbol.explode name) major;
-          val commands' = Symtab.update (name, kind) commands;
+          val commands' = Symtab.update (name, entry) commands;
         in (minor, major', commands') end)));
 
 
@@ -178,10 +181,16 @@
 fun is_literal keywords = is_keyword keywords orf is_command keywords;
 
 
-(* command kind *)
+(* command keywords *)
 
 fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
 
+fun command_markup keywords name =
+  lookup_command keywords name
+  |> Option.map (fn {pos, id, ...} =>
+      Markup.properties (Position.entity_properties_of false id pos)
+        (Markup.entity Markup.commandN name));
+
 fun command_kind keywords = Option.map #kind o lookup_command keywords;
 
 fun command_files keywords name path =