more permissive syntax;
authorwenzelm
Sun Dec 18 12:32:20 2016 +0100 (2016-12-18)
changeset 645944719f13989df
parent 64593 50c715579715
child 64595 511b30aa4100
more permissive syntax;
more PIDE markup;
src/Pure/ML/ml_antiquotations.ML
     1.1 --- a/src/Pure/ML/ml_antiquotations.ML	Sat Dec 17 15:22:14 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Sun Dec 18 12:32:20 2016 +0100
     1.3 @@ -260,10 +260,12 @@
     1.4  
     1.5  val _ = Theory.setup
     1.6   (ML_Antiquotation.value @{binding keyword}
     1.7 -    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
     1.8 -      if Keyword.is_keyword (Thy_Header.get_keywords thy) name then
     1.9 -        "Parse.$$$ " ^ ML_Syntax.print_string name
    1.10 -      else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
    1.11 +    (Args.context -- Scan.lift (Parse.position (Parse.name || Parse.keyword_with (K true)))
    1.12 +      >> (fn (ctxt, (name, pos)) =>
    1.13 +        if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
    1.14 +          (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
    1.15 +           "Parse.$$$ " ^ ML_Syntax.print_string name)
    1.16 +        else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
    1.17    ML_Antiquotation.value @{binding command_keyword}
    1.18      (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
    1.19        (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of