# HG changeset patch
# User wenzelm
# Date 1504101215 -7200
# Node ID 39257f39c7daf4aa124796d34a51dd931131d7c8
# Parent  19bf4d5966dce39d88ff958d000a1ae2cfafc625
more robust: fall-back for SyntaxUtilities.StyleExtender when Isabelle plugin is unloaded;

diff -r 19bf4d5966dc -r 39257f39c7da src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 29 20:34:43 2017 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 30 15:53:35 2017 +0200
@@ -22,6 +22,7 @@
 declare -a SOURCES_BASE=(
   "src-base/isabelle_encoding.scala"
   "src-base/plugin.scala"
+  "src-base/syntax_style.scala"
 )
 
 declare -a RESOURCES_BASE=(
diff -r 19bf4d5966dc -r 39257f39c7da src/Tools/jEdit/src-base/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala	Tue Aug 29 20:34:43 2017 +0100
+++ b/src/Tools/jEdit/src-base/plugin.scala	Wed Aug 30 15:53:35 2017 +0200
@@ -10,6 +10,7 @@
 import isabelle._
 
 import org.gjt.sp.jedit.EBPlugin
+import org.gjt.sp.util.SyntaxUtilities
 
 
 class Plugin extends EBPlugin
@@ -17,5 +18,7 @@
   override def start()
   {
     Isabelle_System.init()
+
+    SyntaxUtilities.setStyleExtender(Syntax_Style.Dummy_Extender)
   }
 }
diff -r 19bf4d5966dc -r 39257f39c7da src/Tools/jEdit/src-base/syntax_style.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/syntax_style.scala	Wed Aug 30 15:53:35 2017 +0200
@@ -0,0 +1,32 @@
+/*  Title:      Tools/jEdit/src-base/syntax_style.scala
+    Author:     Makarius
+
+Extended syntax styles: dummy version.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import org.gjt.sp.util.SyntaxUtilities
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
+
+
+object Syntax_Style
+{
+  private val plain_range: Int = JEditToken.ID_COUNT
+  private val full_range = 6 * plain_range + 1
+
+  object Dummy_Extender extends SyntaxUtilities.StyleExtender
+  {
+    override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
+    {
+      val new_styles = new Array[SyntaxStyle](full_range)
+      for (i <- 0 until full_range) {
+        new_styles(i) = styles(i % plain_range)
+      }
+      new_styles
+    }
+  }
+}