# HG changeset patch
# User wenzelm
# Date 1288863217 -3600
# Node ID d25bbb5f1c9e91f94b065dcd5734a1101aa848fa
# Parent  755862729f8d383020f6d759dc1bbc11e4cac253
warn in correlation with report -- avoid spurious message duplicates;

diff -r 755862729f8d -r d25bbb5f1c9e src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Thu Nov 04 10:22:59 2010 +0100
+++ b/src/Pure/ML/ml_lex.ML	Thu Nov 04 10:33:37 2010 +0100
@@ -70,17 +70,18 @@
 fun content_of (Token (_, (_, x))) = x;
 fun token_leq (tok, tok') = content_of tok <= content_of tok';
 
+fun warn tok =
+  (case tok of
+    Token (_, (Keyword, ":>")) =>
+      warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
+        \prefer non-opaque matching (:) possibly with abstype" ^
+        Position.str_of (pos_of tok))
+  | _ => ());
+
 fun check_content_of tok =
   (case kind_of tok of
     Error msg => error msg
-  | _ =>
-      (case tok of
-        Token (_, (Keyword, ":>")) =>
-          warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
-            \prefer non-opaque matching (:) possibly with abstype" ^
-            Position.str_of (pos_of tok))
-      | _ => ();
-      content_of tok));
+  | _ => content_of tok);
 
 val flatten = implode o map (Symbol.escape o check_content_of);
 
@@ -288,7 +289,7 @@
         |> Source.exhaust
         |> tap (List.app (Antiquote.report report_token))
         |> tap Antiquote.check_nesting
-        |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
+        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
       handle ERROR msg =>
         cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
   in input @ termination end;