more markup;
authorwenzelm
Wed Jul 23 18:14:59 2014 +0200 (2014-07-23)
changeset 57623249c0297cf10
parent 57622 2da79fca5708
child 57624 a7acd2d8c2fb
more markup;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 23 18:04:16 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 23 18:14:59 2014 +0200
     1.3 @@ -146,24 +146,25 @@
     1.4      val context = ML_Context.the_generic_context ();
     1.5      val thy = Context.theory_of context;
     1.6      val Command {pos, ...} = cmd;
     1.7 +    val command_name = quote (Markup.markup Markup.keyword1 name);
     1.8      val _ =
     1.9        (case try (Thy_Header.the_keyword thy) name of
    1.10          SOME spec =>
    1.11            if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
    1.12            else error ("Inconsistent outer syntax keyword declaration " ^
    1.13 -            quote name ^ Position.here pos)
    1.14 +            command_name ^ Position.here pos)
    1.15        | NONE =>
    1.16            if Context.theory_name thy = Context.PureN
    1.17            then Keyword.define (name, SOME kind)
    1.18 -          else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
    1.19 +          else error ("Undeclared outer syntax command " ^ command_name ^ Position.here pos));
    1.20      val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
    1.21    in
    1.22      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    1.23       (if not (Symtab.defined commands name) then ()
    1.24        else if ! batch_mode then
    1.25 -        error ("Attempt to redefine outer syntax command " ^ quote name)
    1.26 +        error ("Attempt to redefine outer syntax command " ^ command_name)
    1.27        else
    1.28 -        warning ("Redefining outer syntax command " ^ quote name ^
    1.29 +        warning ("Redefining outer syntax command " ^ command_name ^
    1.30            Position.here (Position.thread_data ()));
    1.31        Symtab.update (name, cmd) commands)))
    1.32    end);