equal
deleted
inserted
replaced
54 } |
54 } |
55 } |
55 } |
56 |
56 |
57 // owned by GUI thread |
57 // owned by GUI thread |
58 private var steps = 0 |
58 private var steps = 0 |
59 private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) |
59 private val delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) |
60 { |
60 { |
61 change_size(size => |
61 change_size(size => |
62 { |
62 { |
63 var i = size.round |
63 var i = size.round |
64 while (steps != 0 && i > 0) { |
64 while (steps != 0 && i > 0) { |