--- a/src/Tools/jEdit/src/jedit/document_model.scala Tue Sep 07 22:28:58 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Tue Sep 07 23:06:52 2010 +0200
@@ -272,7 +272,7 @@
handler.handleToken(line_segment, style, offset, length, context)
val syntax = session.current_syntax()
- val token_markup: PartialFunction[Text.Info[Any], Byte] =
+ val token_markup: Markup_Tree.Select[Byte] =
{
case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
if syntax.keyword_kind(name).isDefined =>