# HG changeset patch
# User wenzelm
# Date 1397510812 -7200
# Node ID e73723b39c829354c7bb353582318a968a810181
# Parent  58d7960058f5d98048bd2bb16dc97038934374a3
proper signature for dynamic BeanShell action;

diff -r 58d7960058f5 -r e73723b39c82 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Apr 14 23:24:05 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Apr 14 23:26:52 2014 +0200
@@ -307,7 +307,7 @@
     }
   }
 
-  def reset_dictionary(view: View)
+  def reset_dictionary()
   {
     for (spell_checker <- PIDE.spell_checker.get)
     {