author | wenzelm |
Wed, 08 Jun 2016 19:36:45 +0200 | |
changeset 63261 | 90a44d271683 |
parent 63260 | 0edec65d0633 |
child 63262 | e497387de7af |
child 63263 | c6c95d64607a |
child 63266 | 3837a9ace1c7 |
--- 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() }