557 |
|
|
558 |
public static final String DEFAULT_KEYMAP = "default"; |
public static final String DEFAULT_KEYMAP = "default"; |
559 |
public static final String FOCUS_ACCELERATOR_KEY = "focusAcceleratorKey"; |
public static final String FOCUS_ACCELERATOR_KEY = "focusAcceleratorKey"; |
560 |
|
|
561 |
private static Hashtable keymaps = new Hashtable(); |
private static Hashtable keymaps = new Hashtable(); |
562 |
private Keymap keymap; |
private Keymap keymap; |
563 |
|
|
932 |
{ |
{ |
933 |
try |
try |
934 |
{ |
{ |
935 |
return doc.getText(getSelectionStart(), getSelectionEnd()); |
return doc.getText(getSelectionStart(), getSelectionEnd()); |
936 |
} |
} |
937 |
catch (BadLocationException e) |
catch (BadLocationException e) |
938 |
{ |
{ |
939 |
// This should never happen. |
// This should never happen. |
940 |
return null; |
return null; |
941 |
} |
} |
942 |
} |
} |
943 |
|
|
1246 |
|
|
1247 |
try |
try |
1248 |
{ |
{ |
1249 |
int start = getSelectionStart(); |
int start = getSelectionStart(); |
1250 |
int end = getSelectionEnd(); |
int end = getSelectionEnd(); |
1251 |
|
|
1252 |
// Remove selected text. |
// Remove selected text. |
1253 |
if (dot != mark) |
if (dot != mark) |
1254 |
doc.remove(start, end - start); |
doc.remove(start, end - start); |
1255 |
|
|
1256 |
// Insert new text. |
// Insert new text. |
1257 |
doc.insertString(start, content, null); |
doc.insertString(start, content, null); |
1258 |
|
|
1259 |
// Set dot to new position. |
// Set dot to new position. |
1260 |
setCaretPosition(start + content.length()); |
setCaretPosition(start + content.length()); |
1261 |
} |
} |
1262 |
catch (BadLocationException e) |
catch (BadLocationException e) |
1263 |
{ |
{ |