editable raw text areas: allow user to clear content;
authorwenzelm
Fri, 19 Aug 2011 13:55:32 +0200
changeset 44297 b3bd26fd22d3
parent 44296 0c4411e2fc90
child 44298 b8f8488704e2
editable raw text areas: allow user to clear content;
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/session_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))
 
 
--- 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))