45 |
import java.awt.Point; |
import java.awt.Point; |
46 |
import java.awt.Rectangle; |
import java.awt.Rectangle; |
47 |
import java.awt.Shape; |
import java.awt.Shape; |
48 |
|
import java.awt.event.FocusEvent; |
49 |
|
import java.awt.event.FocusListener; |
50 |
import java.beans.PropertyChangeEvent; |
import java.beans.PropertyChangeEvent; |
51 |
import java.beans.PropertyChangeListener; |
import java.beans.PropertyChangeListener; |
52 |
|
|
230 |
caret.setBlinkRate(defaults.getInt(prefix + ".caretBlinkRate")); |
caret.setBlinkRate(defaults.getInt(prefix + ".caretBlinkRate")); |
231 |
} |
} |
232 |
|
|
233 |
|
private FocusListener focuslistener = new FocusListener() { |
234 |
|
public void focusGained(FocusEvent e) |
235 |
|
{ |
236 |
|
textComponent.repaint(); |
237 |
|
} |
238 |
|
public void focusLost(FocusEvent e) |
239 |
|
{ |
240 |
|
textComponent.repaint(); |
241 |
|
} |
242 |
|
}; |
243 |
|
|
244 |
protected void installListeners() |
protected void installListeners() |
245 |
{ |
{ |
246 |
// Do nothing here. |
textComponent.addFocusListener(focuslistener); |
247 |
} |
} |
248 |
|
|
249 |
protected String getKeymapName() |
protected String getKeymapName() |
341 |
|
|
342 |
protected void uninstallListeners() |
protected void uninstallListeners() |
343 |
{ |
{ |
344 |
// Do nothing here. |
textComponent.removeFocusListener(focuslistener); |
345 |
} |
} |
346 |
|
|
347 |
protected void uninstallKeyboardActions() |
protected void uninstallKeyboardActions() |
380 |
|
|
381 |
rootView.paint(g, getVisibleEditorRect()); |
rootView.paint(g, getVisibleEditorRect()); |
382 |
|
|
383 |
if (caret != null) |
if (caret != null && textComponent.hasFocus()) |
384 |
caret.paint(g); |
caret.paint(g); |
385 |
} |
} |
386 |
|
|