--- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Jun 01 13:54:33 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Jun 01 17:27:38 2010 +0200
@@ -19,6 +19,7 @@
import org.gjt.sp.jedit.gui.RolloverButton
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.syntax.SyntaxStyle
object Document_View
@@ -78,6 +79,24 @@
private val session = model.session
+ /* extended token styles */
+
+ private var styles: Array[SyntaxStyle] = null // owned by Swing thread
+
+ def extend_styles()
+ {
+ Swing_Thread.assert()
+ styles = Isabelle_Token_Marker.extend_styles(text_area.getPainter.getStyles)
+ }
+ extend_styles()
+
+ def set_styles()
+ {
+ Swing_Thread.assert()
+ text_area.getPainter.setStyles(styles)
+ }
+
+
/* commands_changed_actor */
private val commands_changed_actor = actor {