more markup;
authorwenzelm
Wed, 23 Jul 2014 18:14:59 +0200
changeset 57623 249c0297cf10
parent 57622 2da79fca5708
child 57624 a7acd2d8c2fb
more markup;
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);