report commands as formal entities, with def/ref positions;

--- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 02 12:36:54 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 02 13:37:58 2012 +0200
@@ -49,10 +49,17 @@
  {comment: string,
   markup: Thy_Output.markup option,
   int_only: bool,
-  parse: (Toplevel.transition -> Toplevel.transition) parser};
+  parse: (Toplevel.transition -> Toplevel.transition) parser,
+  pos: Position.T,
+  id: serial};
 
-fun make_command comment markup int_only parse =
-  Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
+fun new_command comment markup int_only parse pos =
+  Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
+    pos = pos, id = serial ()};
+
+fun command_markup def (name, Command {pos, id, ...}) =
+  Markup.properties (Position.entity_properties_of def id pos)
+    (Isabelle_Markup.entity Isabelle_Markup.commandN name);
 
 
 (* parse command *)
@@ -125,9 +132,10 @@
 (*synchronized wrt. Keywords*)
 val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
 
-fun add_command ((name, kind), pos) cmd = CRITICAL (fn () =>
+fun add_command (name, kind) cmd = CRITICAL (fn () =>
   let
     val thy = ML_Context.the_global_context ();
+    val Command {pos, ...} = cmd;
     val _ =
       (case try (Thy_Header.the_keyword thy) name of
         SOME spec =>
@@ -138,6 +146,7 @@
           if Context.theory_name thy = Context.PureN
           then Keyword.define (name, SOME kind)
           else error ("Undeclared outer syntax command " ^ quote name ^ Position.str_of pos));
+    val _ = Position.report pos (command_markup true (name, cmd));
   in
     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
      (if not (Symtab.defined commands name) then ()
@@ -160,14 +169,14 @@
 
 fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
 
-fun command command_spec comment parse =
-  add_command command_spec (make_command comment NONE false parse);
+fun command (spec, pos) comment parse =
+  add_command spec (new_command comment NONE false parse pos);
 
-fun markup_command markup command_spec comment parse =
-  add_command command_spec (make_command comment (SOME markup) false parse);
+fun markup_command markup (spec, pos) comment parse =
+  add_command spec (new_command comment (SOME markup) false parse pos);
 
-fun improper_command command_spec comment parse =
-  add_command command_spec (make_command comment NONE true parse);
+fun improper_command (spec, pos) comment parse =
+  add_command spec (new_command comment NONE true parse pos);
 
 end;
 
@@ -266,7 +275,16 @@
   let
     val commands = lookup_commands outer_syntax;
     val range_pos = Position.set_range (Token.range toks);
-    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks);
+
+    fun command_reports tok =
+      if Token.kind_of tok = Token.Command then
+        let val name = Token.content_of tok in
+          (case commands name of
+            NONE => []
+          | SOME cmd => [(Token.position_of tok, command_markup false (name, cmd))])
+        end
+      else [];
+    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks @ maps command_reports toks);
   in
     (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
       [tr] =>