# HG changeset patch
# User wenzelm
# Date 1418051090 -3600
# Node ID c85e018be3a3f3a850523138e7806294cdefe06e
# Parent  af691e67f71fa176c2e10cebbbfb248cf58df4a9# Parent  8a78c7cb5b14d960acb7609711c7a31e8f6ec97e
merged

diff -r af691e67f71f -r c85e018be3a3 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Dec 08 14:32:11 2014 +0100
+++ b/src/Pure/General/symbol.scala	Mon Dec 08 16:04:50 2014 +0100
@@ -438,7 +438,7 @@
 
     /* control symbols */
 
-    val ctrl_decoded: Set[Symbol] =
+    val control_decoded: Set[Symbol] =
       Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
 
     val sub_decoded = decode("\\<^sub>")
@@ -516,11 +516,11 @@
 
   /* control symbols */
 
-  def is_ctrl(sym: Symbol): Boolean =
-    sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
+  def is_control(sym: Symbol): Boolean =
+    sym.startsWith("\\<^") || symbols.control_decoded.contains(sym)
 
   def is_controllable(sym: Symbol): Boolean =
-    !is_blank(sym) && !is_ctrl(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
+    !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
 
   def sub_decoded: Symbol = symbols.sub_decoded
   def sup_decoded: Symbol = symbols.sup_decoded
diff -r af691e67f71f -r c85e018be3a3 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Dec 08 14:32:11 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Dec 08 16:04:50 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 af691e67f71f -r c85e018be3a3 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Dec 08 14:32:11 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Mon Dec 08 16:04:50 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_lex.ML
     Author:     Makarius
 
-Lexical syntax for SML.
+Lexical syntax for Isabelle/ML and Standard ML.
 *)
 
 signature ML_LEX =
@@ -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
diff -r af691e67f71f -r c85e018be3a3 src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Mon Dec 08 14:32:11 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala	Mon Dec 08 16:04:50 2014 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/ML/ml_lex.scala
     Author:     Makarius
 
-Lexical syntax for SML.
+Lexical syntax for Isabelle/ML and Standard ML.
 */
 
 package isabelle
@@ -90,8 +90,8 @@
       repeated(character(Symbol.is_ascii_digit), 3, 3)
 
     private val str =
-      one(Symbol.is_symbolic) |
       one(character(c => c != '"' && c != '\\' && ' ' <= c && c <= '~')) |
+      one(s => Symbol.is_symbolic(s) | Symbol.is_control(s)) |
       "\\" ~ escape ^^ { case x ~ y => x + y }