author | wenzelm |
Thu, 20 Sep 2012 20:27:47 +0200 | |
changeset 49472 | ba2c0d0cd429 |
parent 49471 | 97964515a676 |
child 49473 | ca7e2c21b104 |
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Sep 20 20:13:42 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Sep 20 20:27:47 2012 +0200 @@ -147,6 +147,9 @@ /* init */ + override def isCaretVisible: Boolean = false + + getPainter.setStructureHighlightEnabled(false) getBuffer.setTokenMarker(new Token_Markup.Marker(true, None)) getBuffer.setReadOnly(true) rich_text_area.activate()