# HG changeset patch # User wenzelm # Date 1569922143 -7200 # Node ID 97d3485028b675a23b17c78e8e3599a6c038313a # Parent 64751a7abfa64dcd9babae9beaf2ce3a6d515c4a more sequential access to Session.manager.global_state: avoid minor divergence of tip version; diff -r 64751a7abfa6 -r 97d3485028b6 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Mon Sep 30 21:01:08 2019 +0200 +++ b/src/Pure/PIDE/headless.scala Tue Oct 01 11:29:03 2019 +0200 @@ -318,7 +318,7 @@ def check_state(beyond_limit: Boolean = false) { - val state = session.current_state() + val state = session.get_state() for (version <- state.stable_tip_version) { val (load_theories, share_common_data) = use_theories_state.change_result(_.check(state, version, beyond_limit)) diff -r 64751a7abfa6 -r 97d3485028b6 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Mon Sep 30 21:01:08 2019 +0200 +++ b/src/Pure/PIDE/session.scala Tue Oct 01 11:29:03 2019 +0200 @@ -197,6 +197,7 @@ private case class Start(start_prover: Prover.Receiver => Prover) private case object Stop + private case class Get_State(promise: Promise[Document.State]) private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Protocol_Command(name: String, args: List[String]) private case class Update_Options(options: Options) @@ -218,18 +219,11 @@ def is_ready: Boolean = phase == Session.Ready - /* global state */ + /* syslog */ private val syslog = new Session.Syslog(syslog_limit) def syslog_content(): String = syslog.content - private val global_state = Synchronized(Document.State.init) - def current_state(): Document.State = global_state.value - - def recent_syntax(name: Document.Node.Name): Outer_Syntax = - global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse - resources.session_base.overall_syntax - /* pipelined change parsing */ @@ -390,6 +384,10 @@ private val manager: Consumer_Thread[Any] = { + /* global state */ + val global_state = Synchronized(Document.State.init) + + /* raw edits */ def handle_raw_edits( @@ -604,6 +602,9 @@ prover.get.terminate } + case Get_State(promise) => + promise.fulfill(global_state.value) + case Consolidate_Execution => if (prover.defined) { val state = global_state.value @@ -668,9 +669,20 @@ /* main operations */ + def get_state(): Document.State = + { + val promise = Future.promise[Document.State] + manager.send_wait(Get_State(promise)) + promise.join + } + def snapshot(name: Document.Node.Name = Document.Node.Name.empty, pending_edits: List[Text.Edit] = Nil): Document.Snapshot = - global_state.value.snapshot(name, pending_edits) + get_state().snapshot(name, pending_edits) + + def recent_syntax(name: Document.Node.Name): Outer_Syntax = + get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse + resources.session_base.overall_syntax @tailrec final def await_stable_snapshot(): Document.Snapshot = { diff -r 64751a7abfa6 -r 97d3485028b6 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Mon Sep 30 21:01:08 2019 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Oct 01 11:29:03 2019 +0200 @@ -233,7 +233,7 @@ val stable_tip_version = if (st.models.forall(entry => entry._2.is_stable)) - session.current_state().stable_tip_version + session.get_state().stable_tip_version else None val aux_files = diff -r 64751a7abfa6 -r 97d3485028b6 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Sep 30 21:01:08 2019 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Tue Oct 01 11:29:03 2019 +0200 @@ -141,7 +141,7 @@ if (options.bool("jedit_auto_resolve")) { val stable_tip_version = if (models.forall(p => p._2.is_stable)) - session.current_state().stable_tip_version + session.get_state().stable_tip_version else None stable_tip_version match { case Some(version) => resources.undefined_blobs(version.nodes)