changeset 56662 | f373fb77e0a4 |
parent 56428 | 1acf2d76ac23 |
child 56729 | 1da2272a06a4 |
--- a/src/Tools/jEdit/src/active.scala Tue Apr 22 23:31:45 2014 +0200 +++ b/src/Tools/jEdit/src/active.scala Tue Apr 22 23:49:15 2014 +0200 @@ -16,7 +16,7 @@ { def action(view: View, text: String, elem: XML.Elem) { - Swing_Thread.require() + Swing_Thread.require {} Document_View(view.getTextArea) match { case Some(doc_view) =>