--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sun Sep 13 23:03:55 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Sep 15 13:33:02 2009 +0200
@@ -24,8 +24,9 @@
{
/* line context */
+ private val rule_set = new ParserRuleSet("isabelle", "MAIN")
private class LineContext(val line: Int, prev: LineContext)
- extends TokenMarker.LineContext(new ParserRuleSet("isabelle", "MAIN"), prev)
+ extends TokenMarker.LineContext(rule_set, prev)
/* mapping to jEdit token types */