# 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);