terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);

--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon May 31 16:45:48 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon May 31 18:17:48 2010 +0200
@@ -87,11 +87,7 @@
           map (pair (offset_of p)) (String.explode (Symbol.esc sym)))
       end);
 
-    val end_pos =
-      if null toks then Position.none
-      else ML_Lex.end_pos_of (List.last toks);
-
-    val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
+    val input_buffer = Unsynchronized.ref input;
     val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
 
     fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);

--- a/src/Pure/ML/ml_lex.ML	Mon May 31 16:45:48 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon May 31 18:17:48 2010 +0200
@@ -267,17 +267,24 @@
   let
     val _ = Position.report Markup.ML_source pos;
     val syms = Symbol_Pos.explode (txt, pos);
-  in
-    (Source.of_list syms
-      |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
-        (SOME (false, fn msg => recover msg >> map Antiquote.Text))
-      |> Source.exhaust
-      |> tap (List.app (Antiquote.report report_token))
-      |> tap Antiquote.check_nesting
-      |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
-    handle ERROR msg =>
-      cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos)
-  end;
+    val termination =
+      if null syms then []
+      else
+        let
+          val pos1 = List.last syms |-> Position.advance;
+          val pos2 = Position.advance Symbol.space pos1;
+        in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
+    val input =
+      (Source.of_list syms
+        |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
+          (SOME (false, fn msg => recover msg >> map Antiquote.Text))
+        |> Source.exhaust
+        |> tap (List.app (Antiquote.report report_token))
+        |> tap Antiquote.check_nesting
+        |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
+      handle ERROR msg =>
+        cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
+  in input @ termination end;
 
 end;