# HG changeset patch
# User wenzelm
# Date 1446653657 -3600
# Node ID f26a4d5e82b58c93d61d21bb60807828b0d782a7
# Parent  947ce60a06e1df66ac67034073141e5b19262891
dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;

diff -r 947ce60a06e1 -r f26a4d5e82b5 src/Tools/jEdit/src/pretty_text_area.scala
--- 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()
 }
-