# HG changeset patch
# User wenzelm
# Date 1375102172 -7200
# Node ID 1df3e32af79a0e84edb77b066dd907473a02c178
# Parent  9c28559e5fff0406f757e683298a865a2f13c074
tuned;

diff -r 9c28559e5fff -r 1df3e32af79a src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 14:43:21 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 14:49:32 2013 +0200
@@ -141,7 +141,7 @@
       options.string("editor_execution_range") = range.toString
       PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
 
-      val edits =
+      PIDE.session.update(
         (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
           case (edits, buffer) =>
             JEdit_Lib.buffer_lock(buffer) {
@@ -150,8 +150,8 @@
                 case None => edits
               }
             }
-          }
-      PIDE.session.update(edits)
+        }
+      )
     }
   }
 }