diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -59,7 +59,7 @@
 {
   text_area =>
 
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   private var current_font_info: Font_Info = Font_Info.main()
   private var current_body: XML.Body = Nil
@@ -77,7 +77,7 @@
 
   def refresh()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val font = current_font_info.font
     getPainter.setFont(font)
@@ -142,7 +142,7 @@
 
   def resize(font_info: Font_Info)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     current_font_info = font_info
     refresh()
@@ -150,7 +150,7 @@
 
   def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     require(!base_snapshot.is_outdated)
 
     current_base_snapshot = base_snapshot