full repaint after dictionary update;
authorwenzelm
Mon, 14 Apr 2014 22:51:23 +0200
changeset 56575 cdd609ea595d
parent 56574 2b38472a4695
child 56576 86148ca3c4fd
full repaint after dictionary update;
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())
+    }
+  }
 }