| changeset 49475 | 8f3a3adadd5a |
| parent 49472 | ba2c0d0cd429 |
| child 49492 | 2e3e7ea5ce8e |
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Sep 20 21:57:37 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Sep 20 22:25:30 2012 +0200 @@ -150,8 +150,11 @@ override def isCaretVisible: Boolean = false getPainter.setStructureHighlightEnabled(false) + getPainter.setLineHighlightEnabled(false) + getBuffer.setTokenMarker(new Token_Markup.Marker(true, None)) getBuffer.setReadOnly(true) + rich_text_area.activate() }