tuned;
authorwenzelm
Mon, 29 Jul 2013 14:49:32 +0200
changeset 52768 1df3e32af79a
parent 52767 9c28559e5fff
child 52769 0827b6f5de44
tuned;
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)
+        }
+      )
     }
   }
 }