merged

--- a/src/Pure/Isar/toplevel.ML	Mon May 31 17:41:06 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon May 31 19:36:13 2010 +0200
@@ -643,6 +643,7 @@
     Exn.Result () =>
       (case transition true tr st of
         SOME (st', NONE) => (status tr Markup.finished; SOME st')
+      | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
       | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
       | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
   | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));

--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon May 31 17:41:06 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon May 31 19:36:13 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 17:41:06 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon May 31 19:36:13 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;