1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 02 12:36:54 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 02 13:37:58 2012 +0200
     1.3 @@ -49,10 +49,17 @@
     1.4   {comment: string,
     1.5    markup: Thy_Output.markup option,
     1.6    int_only: bool,
     1.7 -  parse: (Toplevel.transition -> Toplevel.transition) parser};
     1.8 +  parse: (Toplevel.transition -> Toplevel.transition) parser,
     1.9 +  pos: Position.T,
    1.10 +  id: serial};
    1.11  
    1.12 -fun make_command comment markup int_only parse =
    1.13 -  Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
    1.14 +fun new_command comment markup int_only parse pos =
    1.15 +  Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
    1.16 +    pos = pos, id = serial ()};
    1.17 +
    1.18 +fun command_markup def (name, Command {pos, id, ...}) =
    1.19 +  Markup.properties (Position.entity_properties_of def id pos)
    1.20 +    (Isabelle_Markup.entity Isabelle_Markup.commandN name);
    1.21  
    1.22  
    1.23  (* parse command *)
    1.24 @@ -125,9 +132,10 @@
    1.25  (*synchronized wrt. Keywords*)
    1.26  val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
    1.27  
    1.28 -fun add_command ((name, kind), pos) cmd = CRITICAL (fn () =>
    1.29 +fun add_command (name, kind) cmd = CRITICAL (fn () =>
    1.30    let
    1.31      val thy = ML_Context.the_global_context ();
    1.32 +    val Command {pos, ...} = cmd;
    1.33      val _ =
    1.34        (case try (Thy_Header.the_keyword thy) name of
    1.35          SOME spec =>
    1.36 @@ -138,6 +146,7 @@
    1.37            if Context.theory_name thy = Context.PureN
    1.38            then Keyword.define (name, SOME kind)
    1.39            else error ("Undeclared outer syntax command " ^ quote name ^ Position.str_of pos));
    1.40 +    val _ = Position.report pos (command_markup true (name, cmd));
    1.41    in
    1.42      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    1.43       (if not (Symtab.defined commands name) then ()
    1.44 @@ -160,14 +169,14 @@
    1.45  
    1.46  fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
    1.47  
    1.48 -fun command command_spec comment parse =
    1.49 -  add_command command_spec (make_command comment NONE false parse);
    1.50 +fun command (spec, pos) comment parse =
    1.51 +  add_command spec (new_command comment NONE false parse pos);
    1.52  
    1.53 -fun markup_command markup command_spec comment parse =
    1.54 -  add_command command_spec (make_command comment (SOME markup) false parse);
    1.55 +fun markup_command markup (spec, pos) comment parse =
    1.56 +  add_command spec (new_command comment (SOME markup) false parse pos);
    1.57  
    1.58 -fun improper_command command_spec comment parse =
    1.59 -  add_command command_spec (make_command comment NONE true parse);
    1.60 +fun improper_command (spec, pos) comment parse =
    1.61 +  add_command spec (new_command comment NONE true parse pos);
    1.62  
    1.63  end;
    1.64  
    1.65 @@ -266,7 +275,16 @@
    1.66    let
    1.67      val commands = lookup_commands outer_syntax;
    1.68      val range_pos = Position.set_range (Token.range toks);
    1.69 -    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks);
    1.70 +
    1.71 +    fun command_reports tok =
    1.72 +      if Token.kind_of tok = Token.Command then
    1.73 +        let val name = Token.content_of tok in
    1.74 +          (case commands name of
    1.75 +            NONE => []
    1.76 +          | SOME cmd => [(Token.position_of tok, command_markup false (name, cmd))])
    1.77 +        end
    1.78 +      else [];
    1.79 +    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks @ maps command_reports toks);
    1.80    in
    1.81      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
    1.82        [tr] =>