imitate "noWordSep" of isabelle mode, e.g. relevant for word selection via double-click;
authorwenzelm
Tue, 13 Aug 2013 12:48:06 +0200
changeset 53002 9dd1a6dcebfd
parent 53001 0ef4699b2502
child 53003 39da27fc6101
imitate "noWordSep" of isabelle mode, e.g. relevant for word selection via double-click;
src/Tools/jEdit/src/pretty_text_area.scala
--- 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()
 }