# 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)