--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Sep 16 15:37:12 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Sep 17 15:51:11 2010 +0200
@@ -121,7 +121,7 @@
fun message {message = msg, hard, location = loc, context = _} =
let
val txt =
- Markup.markup Markup.location
+ Markup.markup Markup.no_report
((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
Markup.markup (Position.report_markup (offset_position_of loc)) "";