author | wenzelm |
Tue, 13 Aug 2013 12:48:06 +0200 | |
changeset 53002 | 9dd1a6dcebfd |
parent 53001 | 0ef4699b2502 |
child 53003 | 39da27fc6101 |
--- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Aug 13 12:19:45 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Aug 13 12:48:06 2013 +0200 @@ -198,6 +198,7 @@ getBuffer.setTokenMarker(new Token_Markup.Marker(true, None)) getBuffer.setReadOnly(true) + getBuffer.setStringProperty("noWordSep", "_'.?") rich_text_area.activate() }