dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Nov 04 15:07:23 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Nov 04 17:14:17 2015 +0100
@@ -18,9 +18,11 @@
import scala.swing.{Label, Component}
import scala.util.matching.Regex
-import org.gjt.sp.jedit.{jEdit, View, Registers}
+import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
+import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler}
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
import org.gjt.sp.jedit.syntax.SyntaxStyle
+import org.gjt.sp.jedit.gui.KeyEventTranslator
import org.gjt.sp.util.{SyntaxUtilities, Log}
@@ -139,11 +141,9 @@
current_rendering = rendering
JEdit_Lib.buffer_edit(getBuffer) {
rich_text_area.active_reset()
- getBuffer.setReadOnly(false)
getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
setText(text)
setCaretPosition(0)
- getBuffer.setReadOnly(true)
}
}
})
@@ -224,6 +224,14 @@
/* key handling */
+ inputHandlerProvider =
+ new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) {
+ override def getAction(action: String): JEditBeanShellAction =
+ text_area.getActionContext.getAction(action)
+ override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean) {}
+ override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false
+ })
+
addKeyListener(JEdit_Lib.key_listener(
key_pressed = (evt: KeyEvent) =>
{
@@ -260,9 +268,7 @@
getPainter.setLineHighlightEnabled(false)
getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
- getBuffer.setReadOnly(true)
getBuffer.setStringProperty("noWordSep", "_'.?")
rich_text_area.activate()
}
-