# HG changeset patch
# User wenzelm
# Date 1397508683 -7200
# Node ID cdd609ea595dfd794399495fba8845d97db82bb8
# Parent  2b38472a469543379bb83e93ae29b1ace52d12ac
full repaint after dictionary update;

diff -r 2b38472a4695 -r cdd609ea595d src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Apr 14 21:51:41 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Apr 14 22:51:23 2014 +0200
@@ -299,9 +299,19 @@
       spell_checker <- PIDE.spell_checker.get
       doc_view <- PIDE.document_view(text_area)
       Text.Info(_, word) <- Spell_Checker.current_word(text_area, doc_view.get_rendering())
-    } spell_checker.update(word, include, permanent)
+    } {
+      spell_checker.update(word, include, permanent)
+      JEdit_Lib.jedit_views().foreach(_.repaint())
+    }
   }
 
-  def reset_dictionary(): Unit = PIDE.spell_checker.get.foreach(_.reset())
+  def reset_dictionary(view: View)
+  {
+    for (spell_checker <- PIDE.spell_checker.get)
+    {
+      spell_checker.reset()
+      JEdit_Lib.jedit_views().foreach(_.repaint())
+    }
+  }
 }