# HG changeset patch # User wenzelm # Date 1275327373 -7200 # Node ID 91dfe7dccfdfd6948af3a516bd9143de0d569f5d # Parent 47d1ee50205b44bf19bce1e362cc64a1abca29b9# Parent 1c8cf00489347baff3bcec248e79e3af21f5b9c2 merged diff -r 47d1ee50205b -r 91dfe7dccfdf src/Pure/Isar/toplevel.ML --- 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)); diff -r 47d1ee50205b -r 91dfe7dccfdf src/Pure/ML/ml_compiler_polyml-5.3.ML --- 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); diff -r 47d1ee50205b -r 91dfe7dccfdf src/Pure/ML/ml_lex.ML --- 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;