equal
deleted
inserted
replaced
213 output_process(progress) |
213 output_process(progress) |
214 show_page(output_page) |
214 show_page(output_page) |
215 |
215 |
216 val result = Exn.capture { |
216 val result = Exn.capture { |
217 val snapshot = document_session.get_snapshot |
217 val snapshot = document_session.get_snapshot |
218 using(JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot))) { |
218 using(JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot)))( |
219 session_context => Document_Editor.build(session_context, document_session, progress) |
219 Document_Editor.build(_, document_session, progress)) |
220 } |
|
221 } |
220 } |
222 val msgs = |
221 val msgs = |
223 result match { |
222 result match { |
224 case Exn.Res(_) => |
223 case Exn.Res(_) => |
225 List(Protocol.writeln_message("DONE")) |
224 List(Protocol.writeln_message("DONE")) |