strict initialization of plugin.session: no user errors to be expected before session.start;
--- a/src/Tools/jEdit/src/plugin.scala Wed Mar 15 14:29:55 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Mar 15 15:39:15 2017 +0100
@@ -33,8 +33,7 @@
def options: JEdit_Options = plugin.options
def resources: JEdit_Resources = plugin.resources
-
- @volatile var session: Session = new Session(JEdit_Resources.empty)
+ def session: Session = plugin.session
/* semantic document content */
@@ -85,6 +84,22 @@
def resources: JEdit_Resources = _resources
+ /* session */
+
+ private var _session: Session = null
+ private def init_session()
+ {
+ _session =
+ new Session(resources) {
+ override def output_delay = options.seconds("editor_output_delay")
+ override def prune_delay = options.seconds("editor_prune_delay")
+ override def syslog_limit = options.int("editor_syslog_limit")
+ override def reparse_limit = options.int("editor_reparse_limit")
+ }
+ }
+ def session: Session = _session
+
+
/* misc support */
val completion_history = new Completion.History_Variable
@@ -95,7 +110,7 @@
def options_changed()
{
- PIDE.session.global_options.post(Session.Global_Options(options.value))
+ session.global_options.post(Session.Global_Options(options.value))
delay_load.invoke()
}
@@ -136,7 +151,7 @@
if (options.bool("jedit_auto_resolve")) {
val stable_tip_version =
if (models.forall(p => p._2.is_stable))
- PIDE.session.current_state().stable_tip_version
+ session.current_state().stable_tip_version
else None
stable_tip_version match {
case Some(version) => resources.undefined_blobs(version.nodes)
@@ -158,7 +173,7 @@
GUI_Thread.later {
try {
- Document_Model.provide_files(PIDE.session, loaded_files)
+ Document_Model.provide_files(session, loaded_files)
delay_init.invoke()
}
finally { delay_load_active.change(_ => false) }
@@ -189,11 +204,11 @@
case Session.Terminated(_) =>
GUI_Thread.later {
GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
- "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
+ "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
}
case Session.Ready =>
- PIDE.session.update_options(options.value)
+ session.update_options(options.value)
init_models()
if (!Isabelle.continuous_checking) {
@@ -248,7 +263,7 @@
if (buffer.isLoaded) {
JEdit_Lib.buffer_lock(buffer) {
val node_name = resources.node_name(buffer)
- val model = Document_Model.init(PIDE.session, node_name, buffer)
+ val model = Document_Model.init(session, node_name, buffer)
for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
if Document_View.get(text_area).map(_.model) != Some(model)
@@ -327,7 +342,7 @@
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
- if (PIDE.session.is_ready) {
+ if (session.is_ready) {
delay_init.invoke()
delay_load.invoke()
}
@@ -344,7 +359,7 @@
if (buffer != null && text_area != null) {
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED) {
- if (PIDE.session.is_ready)
+ if (session.is_ready)
init_view(buffer, text_area)
}
else {
@@ -370,7 +385,7 @@
}
spell_checker.update(options.value)
- PIDE.session.update_options(options.value)
+ session.update_options(options.value)
case _ =>
}
@@ -414,6 +429,7 @@
init_options()
init_resources()
+ init_session()
PIDE._plugin = this
jEdit.setProperty("plugin-error.start-error", orig_plugin_error)
@@ -429,14 +445,6 @@
init_mode_provider()
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
- PIDE.session.stop()
- PIDE.session = new Session(resources) {
- override def output_delay = options.seconds("editor_output_delay")
- override def prune_delay = options.seconds("editor_prune_delay")
- override def syslog_limit = options.int("editor_syslog_limit")
- override def reparse_limit = options.int("editor_reparse_limit")
- }
-
startup_failure = None
}
catch {
@@ -459,7 +467,7 @@
}
exit_models(JEdit_Lib.jedit_buffers().toList)
- PIDE.session.stop()
+ session.stop()
file_watcher.shutdown()
PIDE._plugin = null