tuned;
authorwenzelm
Mon, 25 Feb 2019 11:38:35 +0100
changeset 70023 9a7f94ab4df9
parent 70022 b3c9291b5fc7
child 70024 edda2d14c108
tuned;
src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Feb 24 20:44:17 2019 +0100
+++ b/src/Pure/ML/ml_lex.ML	Mon Feb 25 11:38:35 2019 +0100
@@ -371,10 +371,11 @@
       if Position.is_reported_range pos
       then Position.report pos (language (Input.is_delimited source))
       else ();
-    val syms =
-      Symbol_Pos.explode (Input.text_of source, pos)
-      |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p));
-  in reader {opaque_warning = opaque_warning} scan syms end;
+  in
+    Input.source_explode source
+    |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p))
+    |> reader {opaque_warning = opaque_warning} scan
+  end;
 
 val read_source =
   read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true}