1.1 --- a/src/Pure/ML/ml_lex.ML	Mon May 31 16:45:48 2010 +0200
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Mon May 31 18:17:48 2010 +0200
     1.3 @@ -267,17 +267,24 @@
     1.4    let
     1.5      val _ = Position.report Markup.ML_source pos;
     1.6      val syms = Symbol_Pos.explode (txt, pos);
     1.7 -  in
     1.8 -    (Source.of_list syms
     1.9 -      |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
    1.10 -        (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    1.11 -      |> Source.exhaust
    1.12 -      |> tap (List.app (Antiquote.report report_token))
    1.13 -      |> tap Antiquote.check_nesting
    1.14 -      |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
    1.15 -    handle ERROR msg =>
    1.16 -      cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos)
    1.17 -  end;
    1.18 +    val termination =
    1.19 +      if null syms then []
    1.20 +      else
    1.21 +        let
    1.22 +          val pos1 = List.last syms |-> Position.advance;
    1.23 +          val pos2 = Position.advance Symbol.space pos1;
    1.24 +        in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
    1.25 +    val input =
    1.26 +      (Source.of_list syms
    1.27 +        |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
    1.28 +          (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    1.29 +        |> Source.exhaust
    1.30 +        |> tap (List.app (Antiquote.report report_token))
    1.31 +        |> tap Antiquote.check_nesting
    1.32 +        |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
    1.33 +      handle ERROR msg =>
    1.34 +        cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
    1.35 +  in input @ termination end;
    1.36  
    1.37  end;
    1.38