tuned;
authorwenzelm
Sun, 05 Feb 2023 15:01:49 +0100
changeset 77196 3d709d300d0f
parent 77195 e312c7fa3bad
child 77197 a541da01ba67
tuned;
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 {