src/Tools/jEdit/src/pretty_text_area.scala

 import javax.swing.event.{DocumentListener, DocumentEvent}
 
 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}
 
 
 object Pretty_Text_Area
 {

 
           GUI_Thread.later {
             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)
             }
           }
         })
     }
   }

   }
 
 
   /* 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) =>
       {
         evt.getKeyCode match {
           case KeyEvent.VK_C | KeyEvent.VK_INSERT

 
   getPainter.setStructureHighlightEnabled(false)
   getPainter.setLineHighlightEnabled(false)
 
   getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
-  getBuffer.setReadOnly(true)
   getBuffer.setStringProperty("noWordSep", "_'.?")
 
   rich_text_area.activate()
 }
-