src/Tools/jEdit/src/active.scala
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 _ =>
-                }
             }
           }
         }