changeset 52081 | 29566b6810f7 |
parent 50715 | 8cfd585b9162 |
child 52530 | 99dd8b4ef3fe |
--- a/src/Tools/jEdit/src/active.scala Mon May 20 13:38:48 2013 +0200 +++ b/src/Tools/jEdit/src/active.scala Mon May 20 13:54:24 2013 +0200 @@ -77,14 +77,10 @@ else text_area.setSelectedText(text) } + case Protocol.Dialog(id, serial, result) => + model.session.dialog_result(id, serial, result) + case _ => - // FIXME pattern match problem in scala-2.9.2 (!??) - elem match { - case Protocol.Dialog(id, serial, result) => - model.session.dialog_result(id, serial, result) - - case _ => - } } } }