--- 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) {
--- 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())
--- 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)
--- 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)
--- 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)