more position information and PIDE markup for command keywords;

--- 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 =

--- a/src/Pure/ML/ml_antiquotations.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -254,10 +254,11 @@
         "Parse.$$$ " ^ ML_Syntax.print_string name
       else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
   ML_Antiquotation.value @{binding command_spec}
-    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
-      if Keyword.is_command (Thy_Header.get_keywords thy) name then
-        ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)
-      else error ("Bad outer syntax command " ^ quote name ^ Position.here pos))));
+    (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
+      (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
+        SOME markup =>
+         (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
+          ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos))
+      | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos)))));
 
 end;
-

--- a/src/Pure/PIDE/document.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -125,8 +125,8 @@
           NONE => I
         | SOME id => Protocol_Message.command_positions_yxml id)
         |> error;
-    val {name = (name, _), imports, keywords} = header;
-    val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
+    val {name = (name, _), imports, ...} = header;
+    val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
   in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
 
 fun get_perspective (Node {perspective, ...}) = perspective;

--- a/src/Pure/PIDE/protocol.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -81,7 +81,8 @@
                               (option (pair (pair string (list string)) (list string)))))
                               (list YXML.string_of_body)))) a;
                         val imports' = map (rpair Position.none) imports;
-                        val header = Thy_Header.make (name, Position.none) imports' keywords;
+                        val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
+                        val header = Thy_Header.make (name, Position.none) imports' keywords';
                       in Document.Deps {master = master, header = header, errors = errors} end,
                     fn (a :: b, c) =>
                       Document.Perspective (bool_atom a, map int_atom b,

--- a/src/Pure/Thy/thy_header.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/Thy/thy_header.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -6,7 +6,7 @@
 
 signature THY_HEADER =
 sig
-  type keywords = (string * Keyword.spec option) list
+  type keywords = ((string * Position.T) * Keyword.spec option) list
   type header =
    {name: string * Position.T,
     imports: (string * Position.T) list,
@@ -29,7 +29,7 @@
 
 (* header *)
 
-type keywords = (string * Keyword.spec option) list;
+type keywords = ((string * Position.T) * Keyword.spec option) list;
 
 type header =
  {name: string * Position.T,
@@ -59,26 +59,26 @@
 val bootstrap_keywords =
   Keyword.empty_keywords
   |> Keyword.add_keywords
-    [("%", NONE),
-     ("(", NONE),
-     (")", NONE),
-     (",", NONE),
-     ("::", NONE),
-     ("==", NONE),
-     ("and", NONE),
-     (beginN, NONE),
-     (importsN, NONE),
-     (keywordsN, NONE),
-     (headerN, SOME ((Keyword.document_heading, []), [])),
-     (chapterN, SOME ((Keyword.document_heading, []), [])),
-     (sectionN, SOME ((Keyword.document_heading, []), [])),
-     (subsectionN, SOME ((Keyword.document_heading, []), [])),
-     (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
-     (textN, SOME ((Keyword.document_body, []), [])),
-     (txtN, SOME ((Keyword.document_body, []), [])),
-     (text_rawN, SOME ((Keyword.document_raw, []), [])),
-     (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
-     ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
+    [(("%", @{here}), NONE),
+     (("(", @{here}), NONE),
+     ((")", @{here}), NONE),
+     ((",", @{here}), NONE),
+     (("::", @{here}), NONE),
+     (("==", @{here}), NONE),
+     (("and", @{here}), NONE),
+     ((beginN, @{here}), NONE),
+     ((importsN, @{here}), NONE),
+     ((keywordsN, @{here}), NONE),
+     ((headerN, @{here}), SOME ((Keyword.document_heading, []), [])),
+     ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
+     ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+     ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+     ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+     ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
+     ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
+     ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
+     ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
+     (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
 
 
 (* theory data *)
@@ -119,7 +119,7 @@
   Parse.group (fn () => "outer syntax keyword completion") Parse.name;
 
 val keyword_decl =
-  Scan.repeat1 Parse.string --
+  Scan.repeat1 (Parse.position Parse.string) --
   Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
   Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
   >> (fn ((names, spec), _) => map (rpair spec) names);

--- a/src/Pure/Tools/find_consts.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -140,7 +140,7 @@
 
 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
 
-val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
+val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
 
 in
 

--- a/src/Pure/Tools/find_theorems.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -524,7 +524,7 @@
 
 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
 
-val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
+val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
 
 in