# HG changeset patch
# User wenzelm
# Date 1459542003 -7200
# Node ID 288c309df28d592acd2796df9f43d900c2be6272
# Parent  3c4e9a7937b1c6f8153af731806756117537f950
explicit warning about formal use of Unicode;

diff -r 3c4e9a7937b1 -r 288c309df28d src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 21:34:51 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 22:20:03 2016 +0200
@@ -204,7 +204,7 @@
 fun reports_of_block pos =
   [(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)];
 
-fun reports_of (xsym, pos: Position.T) =
+fun reports_of (xsym, pos) =
   (case xsym of
     Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)]
   | Argument _ => [(pos, Markup.expression "mixfix argument")]
@@ -213,6 +213,15 @@
   | Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)]
   | En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]);
 
+fun reports_text_of (xsym, pos) =
+  (case xsym of
+    Delim s =>
+      if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then
+        [((pos, Markup.bad),
+          "Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")]
+      else []
+  | _ => []);
+
 fun read_block_properties ss =
   let
     val props = read_properties ss;
@@ -273,6 +282,7 @@
         (res, []) => map_filter I res
       | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos));
     val _ = Position.reports (maps reports_of xsymbs);
+    val _ = Position.reports_text (maps reports_text_of xsymbs);
   in xsymbs end;
 
 val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none));