equal
deleted
inserted
replaced
57 case None => |
57 case None => |
58 case Some((_, fields)) => ML_Statistics(statistics.toList).update_data(data, fields) |
58 case Some((_, fields)) => ML_Statistics(statistics.toList).update_data(data, fields) |
59 } |
59 } |
60 |
60 |
61 private val input_delay = |
61 private val input_delay = |
62 GUI_Thread.delay_first(PIDE.options.seconds("editor_input_delay")) { update_chart } |
62 Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart } |
63 |
63 |
64 private val update_delay = |
64 private val update_delay = |
65 GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart } |
65 Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart } |
66 |
66 |
67 |
67 |
68 /* controls */ |
68 /* controls */ |
69 |
69 |
70 private val ml_stats = new Isabelle.ML_Stats |
70 private val ml_stats = new Isabelle.ML_Stats |