# HG changeset patch
# User wenzelm
# Date 1418050770 -3600
# Node ID 8a78c7cb5b14d960acb7609711c7a31e8f6ec97e
# Parent  364992cd3c505b3963c9698d933b2f0e86c9d44a
some special cases for official SML, to treat Isabelle symbols like raw characters;

diff -r 364992cd3c50 -r 8a78c7cb5b14 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Dec 08 15:21:57 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Dec 08 15:59:30 2014 +0100
@@ -80,9 +80,12 @@
 
     val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
+    val input_explode =
+      if #SML flags then String.explode
+      else maps (String.explode o Symbol.esc) o Symbol.explode;
+
     val input_buffer =
-      Unsynchronized.ref (toks |> map
-        (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
+      Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
 
     fun get () =
       (case ! input_buffer of
diff -r 364992cd3c50 -r 8a78c7cb5b14 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Dec 08 15:21:57 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Mon Dec 08 15:59:30 2014 +0100
@@ -295,7 +295,10 @@
 
 fun gen_read SML pos text =
   let
-    val syms = Symbol_Pos.explode (text, pos);
+    val syms =
+      Symbol_Pos.explode (text, pos)
+      |> SML ? maps (fn (s, p) => raw_explode s |> map (rpair p));
+
     val termination =
       if null syms then []
       else