# HG changeset patch
# User wenzelm
# Date 1489521021 -3600
# Node ID 509a9b0ad02e42ceb2027e719ce668e0630f3ada
# Parent  02037d14cb4260f6cdeb38b16cd2460523cfd861
avoid global variables with implicit initialization;

diff -r 02037d14cb42 -r 509a9b0ad02e src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Mar 14 20:39:50 2017 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Mar 14 20:50:21 2017 +0100
@@ -294,7 +294,7 @@
       val buffer = text_area.getBuffer
       val painter = text_area.getPainter
 
-      val history = PIDE.completion_history.value
+      val history = PIDE.plugin.completion_history.value
       val decode = Isabelle_Encoding.is_active(buffer)
 
       def open_popup(result: Completion.Result)
@@ -316,7 +316,7 @@
             new Completion_Popup(Some(range), layered, loc2, font, items)
             {
               override def complete(item: Completion.Item) {
-                PIDE.completion_history.update(item)
+                PIDE.plugin.completion_history.update(item)
                 insert(item)
               }
               override def propagate(evt: KeyEvent) {
@@ -536,7 +536,7 @@
     {
       GUI.layered_pane(text_field) match {
         case Some(layered) if text_field.isEditable =>
-          val history = PIDE.completion_history.value
+          val history = PIDE.plugin.completion_history.value
 
           val caret = text_field.getCaret.getDot
           val text = text_field.getText
@@ -554,7 +554,7 @@
                 new Completion_Popup(None, layered, loc, text_field.getFont, items)
                 {
                   override def complete(item: Completion.Item) {
-                    PIDE.completion_history.update(item)
+                    PIDE.plugin.completion_history.update(item)
                     insert(item)
                   }
                   override def propagate(evt: KeyEvent) {
diff -r 02037d14cb42 -r 509a9b0ad02e src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 14 20:39:50 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 14 20:50:21 2017 +0100
@@ -415,7 +415,7 @@
   def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
   {
     for {
-      spell_checker <- PIDE.spell_checker.get
+      spell_checker <- PIDE.plugin.spell_checker.get
       doc_view <- Document_View.get(text_area)
       rendering = doc_view.get_rendering()
       range = JEdit_Lib.caret_range(text_area)
@@ -428,7 +428,7 @@
 
   def reset_dictionary()
   {
-    for (spell_checker <- PIDE.spell_checker.get)
+    for (spell_checker <- PIDE.plugin.spell_checker.get)
     {
       spell_checker.reset()
       JEdit_Lib.jedit_views().foreach(_.repaint())
diff -r 02037d14cb42 -r 509a9b0ad02e src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Tue Mar 14 20:39:50 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Tue Mar 14 20:50:21 2017 +0100
@@ -39,7 +39,7 @@
       : Option[Completion.Result] =
   {
     for {
-      spell_checker <- PIDE.spell_checker.get
+      spell_checker <- PIDE.plugin.spell_checker.get
       if explicit
       range = JEdit_Lib.before_caret_range(text_area, rendering)
       word <- current_word(text_area, rendering, range)
@@ -58,7 +58,7 @@
   {
     val result =
       for {
-        spell_checker <- PIDE.spell_checker.get
+        spell_checker <- PIDE.plugin.spell_checker.get
         doc_view <- Document_View.get(text_area)
         rendering = doc_view.get_rendering()
         range = JEdit_Lib.point_range(text_area.getBuffer, offset)
diff -r 02037d14cb42 -r 509a9b0ad02e src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 20:39:50 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 20:50:21 2017 +0100
@@ -36,9 +36,6 @@
     else _plugin
   def options: JEdit_Options = plugin.options
 
-  val completion_history = new Completion.History_Variable
-  val spell_checker = new Spell_Checker_Variable
-
   @volatile var startup_failure: Option[Throwable] = None
   @volatile var startup_notified = false
 
@@ -167,6 +164,10 @@
 
     options
   }
+
+  val completion_history = new Completion.History_Variable
+  val spell_checker = new Spell_Checker_Variable
+
   PIDE._plugin = this
 
 
@@ -388,7 +389,7 @@
             if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area)
           }
 
-          PIDE.spell_checker.update(PIDE.options.value)
+          PIDE.plugin.spell_checker.update(PIDE.options.value)
           PIDE.session.update_options(PIDE.options.value)
 
         case _ =>
@@ -401,8 +402,8 @@
     try {
       Debug.DISABLE_SEARCH_DIALOG_POOL = true
 
-      PIDE.completion_history.load()
-      PIDE.spell_checker.update(PIDE.options.value)
+      PIDE.plugin.completion_history.load()
+      PIDE.plugin.spell_checker.update(PIDE.options.value)
 
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])
@@ -436,7 +437,7 @@
 
     if (PIDE.startup_failure.isEmpty) {
       PIDE.options.value.save_prefs()
-      PIDE.completion_history.value.save()
+      PIDE.plugin.completion_history.value.save()
     }
 
     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
diff -r 02037d14cb42 -r 509a9b0ad02e src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Mar 14 20:39:50 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Mar 14 20:50:21 2017 +0100
@@ -343,7 +343,7 @@
 
             // spell checker
             for {
-              spell_checker <- PIDE.spell_checker.get
+              spell_checker <- PIDE.plugin.spell_checker.get
               spell_range <- rendering.spell_checker_ranges(line_range)
               text <- JEdit_Lib.try_get_text(buffer, spell_range)
               info <- spell_checker.marked_words(spell_range.start, text)