# HG changeset patch
# User wenzelm
# Date 1482060740 -3600
# Node ID 4719f13989df415ee9162bf619e05ae82d978424
# Parent  50c715579715f9b60391a51f427dcb398f0378f0
more permissive syntax;
more PIDE markup;

diff -r 50c715579715 -r 4719f13989df src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Dec 18 12:32:20 2016 +0100
@@ -260,10 +260,12 @@
 
 val _ = Theory.setup
  (ML_Antiquotation.value @{binding keyword}
-    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
-      if Keyword.is_keyword (Thy_Header.get_keywords thy) name then
-        "Parse.$$$ " ^ ML_Syntax.print_string name
-      else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
+    (Args.context -- Scan.lift (Parse.position (Parse.name || Parse.keyword_with (K true)))
+      >> (fn (ctxt, (name, pos)) =>
+        if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
+          (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
+           "Parse.$$$ " ^ ML_Syntax.print_string name)
+        else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
   ML_Antiquotation.value @{binding command_keyword}
     (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
       (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of