diff --git a/source/org/thdl/tib/input/DuffPane.java b/source/org/thdl/tib/input/DuffPane.java index 1174371..c991d0a 100644 --- a/source/org/thdl/tib/input/DuffPane.java +++ b/source/org/thdl/tib/input/DuffPane.java @@ -882,13 +882,18 @@ class RTFSelection implements ClipboardOwner, Transferable { ThdlDebug.noteIffyCode(); } } - if (remove) + if (remove) { + // Respect setEditable(boolean): + if (!this.isEditable()) + return; + try { getDocument().remove(p1, p2-p1); } catch (BadLocationException ble) { ble.printStackTrace(); ThdlDebug.noteIffyCode(); } + } } /** @@ -902,6 +907,9 @@ class RTFSelection implements ClipboardOwner, Transferable { * @param offset the position in the document you want to paste to */ public void paste(int offset) { + // Respect setEditable(boolean): + if (!this.isEditable()) + return; try { Transferable contents = rtfBoard.getContents(this); if (contents.isDataFlavorSupported(rtfFlavor)) { @@ -971,9 +979,7 @@ public void paste(int offset) { if (e.isActionKey()) initKeyboard(); - int code = e.getKeyCode(); - - switch (code) { + switch (e.getKeyCode()) { case KeyEvent.VK_ESCAPE: e.consume(); initKeyboard(); @@ -1041,9 +1047,7 @@ public void paste(int offset) { * and init the keyboard here in key released * though i don't really know why... */ - int code = e.getKeyCode(); - - if (code == KeyEvent.VK_BACK_SPACE) + if (e.getKeyCode() == KeyEvent.VK_BACK_SPACE) initKeyboard(); } @@ -1060,6 +1064,10 @@ public void paste(int offset) { public void keyTyped(KeyEvent e) { e.consume(); + // Respect setEditable(boolean): + if (!this.isEditable()) + return; + if (isTibetan) processTibetan(e); else { diff --git a/source/org/thdl/tib/input/Jskad.java b/source/org/thdl/tib/input/Jskad.java index 1e27e4a..a9a3974 100644 --- a/source/org/thdl/tib/input/Jskad.java +++ b/source/org/thdl/tib/input/Jskad.java @@ -277,6 +277,17 @@ public class Jskad extends JPanel implements DocumentListener { toolsMenu.add(importItem); } + if (ThdlOptions.getBooleanOption("thdl.add.developer.options.to.menu")) { + toolsMenu.addSeparator(); + JMenuItem DevelItem = new JMenuItem("Toggle read-only"); + DevelItem.addActionListener(new ThdlActionListener() { + public void theRealActionPerformed(ActionEvent e) { + dp.setEditable(!dp.isEditable()); + } + }); + toolsMenu.add(DevelItem); + } + menuBar.add(toolsMenu); JMenu infoMenu = new JMenu("Info");