src/Pure/ML/ml_context.ML
changeset 39507 839873937ddd
parent 39388 fdbb2c55ffc2
child 39557 fe5722fce758
equal deleted inserted replaced
39506:cf61ec140c4d 39507:839873937ddd
   116 
   116 
   117 fun antiquotation src ctxt =
   117 fun antiquotation src ctxt =
   118   let val ((name, _), pos) = Args.dest_src src in
   118   let val ((name, _), pos) = Args.dest_src src in
   119     (case Symtab.lookup (! global_parsers) name of
   119     (case Symtab.lookup (! global_parsers) name of
   120       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   120       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   121     | SOME scan => (Context_Position.report ctxt (Markup.ML_antiq name) pos;
   121     | SOME scan =>
       
   122        (Context_Position.report ctxt pos (Markup.ML_antiq name);
   122         Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   123         Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   123   end;
   124   end;
   124 
   125 
   125 end;
   126 end;
   126 
   127