editable raw text areas: allow user to clear content;
authorwenzelm
Fri, 19 Aug 2011 13:55:32 +0200
changeset 45172b3bd26fd22d3
parent 45171 0c4411e2fc90
child 45173 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
     1.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 13:32:27 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 13:55:32 2011 +0200
     1.3 @@ -21,7 +21,6 @@
     1.4    extends Dockable(view: View, position: String)
     1.5  {
     1.6    private val text_area = new TextArea
     1.7 -  text_area.editable = false
     1.8    set_content(new ScrollPane(text_area))
     1.9  
    1.10  
     2.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 13:32:27 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 13:55:32 2011 +0200
     2.3 @@ -28,7 +28,6 @@
     2.4    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
     2.5  
     2.6    private val syslog = new TextArea(Isabelle.session.syslog())
     2.7 -  syslog.editable = false
     2.8  
     2.9    private val tabs = new TabbedPane {
    2.10      pages += new TabbedPane.Page("README", Component.wrap(readme))