src/Pure/ML/ml_antiquotations.ML
changeset 59878 05362c246a64
parent 59812 675d0c692c41
child 59934 b65c4370f831
equal deleted inserted replaced
59877:a04ea4709c8d 59878:05362c246a64
    45                 Completion.make (name, pos) (fn completed =>
    45                 Completion.make (name, pos) (fn completed =>
    46                     Options.names (Options.default ())
    46                     Options.names (Options.default ())
    47                     |> filter completed
    47                     |> filter completed
    48                     |> map (fn a => (a, ("system_option", a))));
    48                     |> map (fn a => (a, ("system_option", a))));
    49               val report = Markup.markup_report (Completion.reported_text completion);
    49               val report = Markup.markup_report (Completion.reported_text completion);
    50             in cat_error msg report end;
    50             in error (msg ^ report) end;
    51         val _ = Context_Position.report ctxt pos markup;
    51         val _ = Context_Position.report ctxt pos markup;
    52       in ML_Syntax.print_string name end)) #>
    52       in ML_Syntax.print_string name end)) #>
    53 
    53 
    54   ML_Antiquotation.value @{binding theory}
    54   ML_Antiquotation.value @{binding theory}
    55     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    55     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>