| changeset 39441 | 4110cc1b8f9f |
| parent 39296 | e275d581a218 |
| child 39507 | 839873937ddd |
--- a/src/Pure/Isar/proof_context.ML Fri Sep 17 17:09:31 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Sep 17 17:10:44 2010 +0200 @@ -734,8 +734,8 @@ local fun parse_failed ctxt pos msg kind = - (Context_Position.report ctxt Markup.bad pos; - cat_error msg ("Failed to parse " ^ kind)); + cat_error msg ("Failed to parse " ^ kind ^ + Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos "")); fun parse_sort ctxt text = let