proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
authorwenzelm
Wed, 08 Jun 2016 19:36:45 +0200
changeset 63261 90a44d271683
parent 63260 0edec65d0633
child 63262 e497387de7af
child 63263 c6c95d64607a
child 63266 3837a9ace1c7
proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
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()
 }