93 /* pending text edits */ |
93 /* pending text edits */ |
94 |
94 |
95 private object pending_edits // owned by Swing thread |
95 private object pending_edits // owned by Swing thread |
96 { |
96 { |
97 private val pending = new mutable.ListBuffer[Text.Edit] |
97 private val pending = new mutable.ListBuffer[Text.Edit] |
98 private var pending_perspective = false |
|
99 private var last_perspective: Text.Perspective = Text.Perspective.empty |
98 private var last_perspective: Text.Perspective = Text.Perspective.empty |
100 |
99 |
101 def snapshot(): List[Text.Edit] = pending.toList |
100 def snapshot(): List[Text.Edit] = pending.toList |
102 |
101 |
103 def flush() |
102 def flush() |
104 { |
103 { |
105 Swing_Thread.require() |
104 Swing_Thread.require() |
106 |
105 |
107 val new_perspective = |
106 val edits = snapshot() |
108 if (pending_perspective) { pending_perspective = false; perspective() } |
107 val new_perspective = perspective() |
109 else last_perspective |
108 if (!edits.isEmpty || last_perspective != new_perspective) { |
110 |
109 pending.clear |
111 snapshot() match { |
110 last_perspective = new_perspective |
112 case Nil if last_perspective == new_perspective => |
111 session.edit_node(name, node_header(), new_perspective, edits) |
113 case edits => |
|
114 pending.clear |
|
115 last_perspective = new_perspective |
|
116 session.edit_node(name, node_header(), new_perspective, edits) |
|
117 } |
112 } |
118 } |
113 } |
119 |
114 |
120 private val delay_flush = |
115 private val delay_flush = |
121 Swing_Thread.delay_last(session.input_delay) { flush() } |
116 Swing_Thread.delay_last(session.input_delay) { flush() } |