# HG changeset patch
# User wenzelm
# Date 1313754932 -7200
# Node ID b3bd26fd22d365f5c34118259778aec22ca68ce1
# Parent  0c4411e2fc9058199f39c12c20bad96cb4cd899b
editable raw text areas: allow user to clear content;

diff -r 0c4411e2fc90 -r b3bd26fd22d3 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 13:32:27 2011 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 13:55:32 2011 +0200
@@ -21,7 +21,6 @@
   extends Dockable(view: View, position: String)
 {
   private val text_area = new TextArea
-  text_area.editable = false
   set_content(new ScrollPane(text_area))
 
 
diff -r 0c4411e2fc90 -r b3bd26fd22d3 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 13:32:27 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 13:55:32 2011 +0200
@@ -28,7 +28,6 @@
   readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
 
   private val syslog = new TextArea(Isabelle.session.syslog())
-  syslog.editable = false
 
   private val tabs = new TabbedPane {
     pages += new TabbedPane.Page("README", Component.wrap(readme))