src/Pure/ML/ml_context.ML
changeset 27874 f0364f1c0ecf
parent 27868 a28b3cd0077b
child 27878 1ba19c9edd18
equal deleted inserted replaced
27873:34d61938e27a 27874:f0364f1c0ecf
   122   P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
   122   P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
   123   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   123   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   124 
   124 
   125 fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
   125 fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
   126   let
   126   let
   127     val ants = Antiquote.read (txt, pos);
   127     val syms = SymbolPos.explode (txt, pos);
       
   128     val ants = Antiquote.read (syms, pos);
   128     val ((ml_env, ml_body), opt_ctxt') =
   129     val ((ml_env, ml_body), opt_ctxt') =
   129       if not (exists Antiquote.is_antiq ants) then (("", Symbol.escape txt), opt_ctxt)
   130       if not (exists Antiquote.is_antiq ants)
       
   131       then (("", Symbol.escape (SymbolPos.content syms)), opt_ctxt)
   130       else
   132       else
   131         let
   133         let
   132           val ctxt =
   134           val ctxt =
   133             (case opt_ctxt of
   135             (case opt_ctxt of
   134               NONE => error ("Unknown context -- cannot expand ML antiquotations" ^
   136               NONE => error ("Unknown context -- cannot expand ML antiquotations" ^