tuned;
authorwenzelm
Mon Feb 25 11:38:35 2019 +0100 (3 months ago ago)
changeset 700239a7f94ab4df9
parent 70022 b3c9291b5fc7
child 70024 edda2d14c108
tuned;
src/Pure/ML/ml_lex.ML
     1.1 --- a/src/Pure/ML/ml_lex.ML	Sun Feb 24 20:44:17 2019 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Feb 25 11:38:35 2019 +0100
     1.3 @@ -371,10 +371,11 @@
     1.4        if Position.is_reported_range pos
     1.5        then Position.report pos (language (Input.is_delimited source))
     1.6        else ();
     1.7 -    val syms =
     1.8 -      Symbol_Pos.explode (Input.text_of source, pos)
     1.9 -      |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p));
    1.10 -  in reader {opaque_warning = opaque_warning} scan syms end;
    1.11 +  in
    1.12 +    Input.source_explode source
    1.13 +    |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p))
    1.14 +    |> reader {opaque_warning = opaque_warning} scan
    1.15 +  end;
    1.16  
    1.17  val read_source =
    1.18    read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true}