--- a/src/Tools/jEdit/src/jedit/document_model.scala Sat Jun 26 22:19:55 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sat Jun 26 22:44:25 2010 +0200
@@ -140,9 +140,11 @@
/* activation */
+ private val token_marker = new Isabelle_Token_Marker(this)
+
def activate()
{
- buffer.setTokenMarker(new Isabelle_Token_Marker(this))
+ buffer.setTokenMarker(token_marker)
buffer.addBufferListener(buffer_listener)
buffer.propertiesChanged()
@@ -150,6 +152,11 @@
edits_delay()
}
+ def refresh()
+ {
+ buffer.setTokenMarker(token_marker)
+ }
+
def deactivate()
{
buffer.setTokenMarker(buffer.getMode.getTokenMarker)