--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jun 07 21:48:24 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Tue Jun 08 13:51:25 2010 +0200
@@ -155,9 +155,11 @@
def to: Int => Int = model.to_current(document, _)
def from: Int => Int = model.from_current(document, _)
+ /* FIXME
for (text_area <- Isabelle.jedit_text_areas(model.buffer)
if Document_View(text_area).isDefined)
Document_View(text_area).get.set_styles()
+ */
def handle_token(style: Byte, offset: Int, length: Int) =
handler.handleToken(line_segment, style, offset, length, context)