# HG changeset patch
# User wenzelm
# Date 1376390886 -7200
# Node ID 9dd1a6dcebfd9a7ffe90c88f8aaa058848efd78f
# Parent  0ef4699b2502c46ccdd94a39b47a880c11b1539b
imitate "noWordSep" of isabelle mode, e.g. relevant for word selection via double-click;

diff -r 0ef4699b2502 -r 9dd1a6dcebfd 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()
 }