tuned signature -- avoid warning during jEdit startup;
authorwenzelm
Mon, 04 Sep 2017 20:55:06 +0200
changeset 66603 f6a1274be674
parent 66602 180b2e72601f
child 66604 1af360d1cad2
tuned signature -- avoid warning during jEdit startup;
src/Tools/jEdit/src-base/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala	Mon Sep 04 15:25:25 2017 +0200
+++ b/src/Tools/jEdit/src-base/plugin.scala	Mon Sep 04 20:55:06 2017 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import org.gjt.sp.jedit.{Debug, EBPlugin}
+import org.gjt.sp.jedit.{EBMessage, Debug, EBPlugin}
 import org.gjt.sp.util.SyntaxUtilities
 
 
@@ -28,4 +28,6 @@
   {
     Syntax_Style.set_style_extender(new SyntaxUtilities.StyleExtender)
   }
+
+  override def handleMessage(message: EBMessage) { }
 }