--- 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/.
--- 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)
+ }
}
--- 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 _)