| changeset 56662 | f373fb77e0a4 |
| parent 56278 | 2576d3a40ed6 |
| child 57126 | 3a928dffc37f |
--- a/src/Tools/jEdit/src/token_markup.scala Tue Apr 22 23:31:45 2014 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Tue Apr 22 23:49:15 2014 +0200 @@ -42,7 +42,7 @@ def edit_control_style(text_area: TextArea, control: String) { - Swing_Thread.assert() + Swing_Thread.assert {} val buffer = text_area.getBuffer