# HG changeset patch
# User wenzelm
# Date 1347990609 -7200
# Node ID 0988d31e91408506080a6b4a04f6337ace96fd70
# Parent  32cb1f1a6a5d66ead3bf5fc47824faa624d02b47
output is read-only;

diff -r 32cb1f1a6a5d -r 0988d31e9140 src/Tools/jEdit/src/pretty_text_area.scala
--- 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
 }