# HG changeset patch
# User wenzelm
# Date 1504270699 -7200
# Node ID 8e1aac4eed1135bd272a46ee28935af2afd4b5db
# Parent  b884c42694e02197299ae983dace213848a31336
more robust;

diff -r b884c42694e0 -r 8e1aac4eed11 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 01 12:57:24 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 01 14:58:19 2017 +0200
@@ -354,6 +354,7 @@
   init_resources "${RESOURCES_BASE[@]}"
   compile_sources "${SOURCES_BASE[@]}"
   make_jar "$TARGET_BASE"
+  classpath "$PWD/$TARGET_BASE"
 
   init_resources "${RESOURCES[@]}"
   cp src/jEdit.props dist/properties/.
diff -r b884c42694e0 -r 8e1aac4eed11 src/Tools/jEdit/src-base/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala	Fri Sep 01 12:57:24 2017 +0200
+++ b/src/Tools/jEdit/src-base/plugin.scala	Fri Sep 01 14:58:19 2017 +0200
@@ -21,4 +21,9 @@
 
     SyntaxUtilities.setStyleExtender(Syntax_Style.Dummy_Extender)
   }
+
+  override def stop()
+  {
+    SyntaxUtilities.setStyleExtender(new SyntaxUtilities.StyleExtender)
+  }
 }
diff -r b884c42694e0 -r 8e1aac4eed11 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 01 12:57:24 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 01 14:58:19 2017 +0200
@@ -454,6 +454,7 @@
   {
     http_server.stop
 
+    SyntaxUtilities.setStyleExtender(isabelle.jedit_base.Syntax_Style.Dummy_Extender)
     exit_mode_provider()
     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)