discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
--- 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 _ =>
- }
}
}
}
--- a/src/Tools/jEdit/src/rendering.scala Mon May 20 13:38:48 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Mon May 20 13:54:24 2013 +0200
@@ -481,17 +481,12 @@
(None, Some(bad_color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
(None, Some(intensify_color))
- case (acc, Text.Info(_, elem @ XML.Elem(Markup(Markup.DIALOG, _), _))) =>
- // FIXME pattern match problem in scala-2.9.2 (!??)
- elem match {
- case Protocol.Dialog(_, serial, result) =>
- command_state.results.get(serial) match {
- case Some(Protocol.Dialog_Result(res)) if res == result =>
- (None, Some(active_result_color))
- case _ =>
- (None, Some(active_color))
- }
- case _ => acc
+ case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
+ command_state.results.get(serial) match {
+ case Some(Protocol.Dialog_Result(res)) if res == result =>
+ (None, Some(active_result_color))
+ case _ =>
+ (None, Some(active_color))
}
case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
(None, Some(active_color))