--- a/src/Tools/jEdit/src/document_dockable.scala Sun Feb 05 14:59:50 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Sun Feb 05 15:01:49 2023 +0100
@@ -215,9 +215,8 @@
val result = Exn.capture {
val snapshot = document_session.get_snapshot
- using(JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot))) {
- session_context => Document_Editor.build(session_context, document_session, progress)
- }
+ using(JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot)))(
+ Document_Editor.build(_, document_session, progress))
}
val msgs =
result match {