# HG changeset patch
# User wenzelm
# Date 1284817829 -7200
# Node ID 8a70e91650a6872f0bb39be48f4a03dbd12db6e1
# Parent  57ceabb0bb8e5949e75294a63f894a5ab9ab1d4f
non-editable text area;

diff -r 57ceabb0bb8e -r 8a70e91650a6 src/Tools/jEdit/src/jedit/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Sat Sep 18 14:28:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Sat Sep 18 15:50:29 2010 +0200
@@ -19,6 +19,7 @@
   extends Dockable(view: View, position: String)
 {
   private val text_area = new TextArea
+  text_area.editable = false
   set_content(new ScrollPane(text_area))
 
 
diff -r 57ceabb0bb8e -r 8a70e91650a6 src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Sat Sep 18 14:28:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Sat Sep 18 15:50:29 2010 +0200
@@ -18,6 +18,7 @@
 class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
 {
   private val text_area = new TextArea("Isabelle session")
+  text_area.editable = false
   set_content(new ScrollPane(text_area))