# HG changeset patch
# User wenzelm
# Date 1384716277 -3600
# Node ID b0074321bf1418726d3c835ffcd5759a6b4c622a
# Parent  faad28e65b48f1952ae902affc3f93141ed4fae0
tuned;

diff -r faad28e65b48 -r b0074321bf14 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 17 17:46:06 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Nov 17 20:24:37 2013 +0100
@@ -156,8 +156,6 @@
 
     def flushed_edits(): List[Document.Edit_Text] =
     {
-      Swing_Thread.require()
-
       val clear = pending_clear
       val edits = snapshot()
       val perspective = node_perspective()
@@ -172,8 +170,6 @@
 
     def edit(clear: Boolean, e: Text.Edit)
     {
-      Swing_Thread.require()
-
       if (clear) {
         pending_clear = true
         pending.clear
@@ -183,16 +179,11 @@
     }
   }
 
-  def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
-
-
-  /* snapshot */
+  def snapshot(): Document.Snapshot =
+    Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
 
-  def snapshot(): Document.Snapshot =
-  {
-    Swing_Thread.require()
-    session.snapshot(node_name, pending_edits.snapshot())
-  }
+  def flushed_edits(): List[Document.Edit_Text] =
+    Swing_Thread.require { pending_edits.flushed_edits() }
 
 
   /* buffer listener */