# 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()) + } + } }