equal
deleted
inserted
replaced
150 /* key listener */ |
150 /* key listener */ |
151 |
151 |
152 private val key_listener = new KeyAdapter { |
152 private val key_listener = new KeyAdapter { |
153 override def keyTyped(evt: KeyEvent) |
153 override def keyTyped(evt: KeyEvent) |
154 { |
154 { |
155 if (evt.getKeyChar == 27) Pretty_Tooltip.dismiss_all() |
155 if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all()) |
|
156 evt.consume |
156 } |
157 } |
157 } |
158 } |
158 |
159 |
159 |
160 |
160 /* caret handling */ |
161 /* caret handling */ |