changeset 59878 | 05362c246a64 |
parent 59812 | 675d0c692c41 |
child 59934 | b65c4370f831 |
--- a/src/Pure/ML/ml_antiquotations.ML Tue Mar 31 15:29:09 2015 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Tue Mar 31 16:43:49 2015 +0200 @@ -47,7 +47,7 @@ |> filter completed |> map (fn a => (a, ("system_option", a)))); val report = Markup.markup_report (Completion.reported_text completion); - in cat_error msg report end; + in error (msg ^ report) end; val _ = Context_Position.report ctxt pos markup; in ML_Syntax.print_string name end)) #>