# HG changeset patch
# User wenzelm
# Date 1465407405 -7200
# Node ID 90a44d2716837bef7fb1579ca17ea8d8c138cc34
# Parent  0edec65d0633a44dad56d1a5f8614ebd549b612e
proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);

diff -r 0edec65d0633 -r 90a44d271683 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jun 08 18:46:09 2016 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jun 08 19:36:45 2016 +0200
@@ -271,7 +271,7 @@
   getPainter.setLineHighlightEnabled(false)
 
   getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
-  getBuffer.setStringProperty("noWordSep", "_'.?")
+  getBuffer.setStringProperty("noWordSep", "_'?⇩")
 
   rich_text_area.activate()
 }