# HG changeset patch
# User wenzelm
# Date 1253014382 -7200
# Node ID 3ec545c964d5afe4f1305f0636b2cdc923d4f904
# Parent  da2bd88f6cdd07662c23ae94a721d960b799a524
single instance of rule_set;

diff -r da2bd88f6cdd -r 3ec545c964d5 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- 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 */