# HG changeset patch
# User wenzelm
# Date 1350032603 -7200
# Node ID 5631ee09929396b1dae2ab7af095616df1f7aa4b
# Parent  77582720af965b9e5cdcd6f52bd16af078a1d82a
more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;

diff -r 77582720af96 -r 5631ee099293 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Oct 11 23:10:49 2012 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Oct 12 11:03:23 2012 +0200
@@ -113,10 +113,8 @@
       let
         val pos = position_of loc;
         val txt =
-          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
-            ((if hard then "Error" else "Warning") ^ Position.here pos ^ ":\n") ^
-          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
-          Position.reported_text pos Isabelle_Markup.report "";
+          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
+          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
       in if hard then err txt else warn txt end;