# HG changeset patch # User wenzelm # Date 1406132099 -7200 # Node ID 249c0297cf10ea9be173b22a0fc8b2d727c9a89b # Parent 2da79fca57089c0bb41dfa02575891d6fe461989 more markup; diff -r 2da79fca5708 -r 249c0297cf10 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Wed Jul 23 18:04:16 2014 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 23 18:14:59 2014 +0200 @@ -146,24 +146,25 @@ val context = ML_Context.the_generic_context (); val thy = Context.theory_of context; val Command {pos, ...} = cmd; + val command_name = quote (Markup.markup Markup.keyword1 name); val _ = (case try (Thy_Header.the_keyword thy) name of SOME spec => if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then () else error ("Inconsistent outer syntax keyword declaration " ^ - quote name ^ Position.here pos) + command_name ^ Position.here pos) | NONE => if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind) - else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos)); + else error ("Undeclared outer syntax command " ^ command_name ^ Position.here pos)); val _ = Context_Position.report_generic context pos (command_markup true (name, cmd)); in Unsynchronized.change global_outer_syntax (map_commands (fn commands => (if not (Symtab.defined commands name) then () else if ! batch_mode then - error ("Attempt to redefine outer syntax command " ^ quote name) + error ("Attempt to redefine outer syntax command " ^ command_name) else - warning ("Redefining outer syntax command " ^ quote name ^ + warning ("Redefining outer syntax command " ^ command_name ^ Position.here (Position.thread_data ())); Symtab.update (name, cmd) commands))) end);