output is read-only;

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 19:42:32 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 19:50:09 2012 +0200
@@ -92,8 +92,10 @@
     val buffer = text_area.getBuffer
     try {
       buffer.beginCompoundEdit
+      buffer.setReadOnly(false)
       text_area.setText(text)
       text_area.setCaretPosition(0)
+      buffer.setReadOnly(true)
     }
     finally {
       buffer.endCompoundEdit
@@ -120,6 +122,7 @@
   }
 
   text_area.getBuffer.setTokenMarker(new Token_Markup.Marker(true, None))
+  text_area.getBuffer.setReadOnly(true)
   rich_text_area.activate()
   layout(Component.wrap(text_area)) = BorderPanel.Position.Center
 }