--- a/src/Tools/jEdit/src/monitor_dockable.scala Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Mon Sep 05 22:09:52 2016 +0200
@@ -33,7 +33,7 @@
statistics = statistics.enqueue(stats)
statistics_length += 1
limit_data.text match {
- case Properties.Value.Int(limit) =>
+ case Value.Int(limit) =>
while (statistics_length > limit) {
statistics = statistics.dequeue._2
statistics_length -= 1
@@ -91,7 +91,7 @@
private val limit_data = new TextField("200", 5) {
tooltip = "Limit for accumulated data"
verifier = (s: String) =>
- s match { case Properties.Value.Int(x) => x > 0 case _ => false }
+ s match { case Value.Int(x) => x > 0 case _ => false }
reactions += { case ValueChanged(_) => input_delay.invoke() }
}