diff -r e312c7fa3bad -r 3d709d300d0f src/Tools/jEdit/src/document_dockable.scala --- 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 {