# HG changeset patch
# User wenzelm
# Date 1497621567 -7200
# Node ID 24658c9d7c78860b10cce640bc541d96e28bad91
# Parent  4401129596319a9c27b16e4d6410516a816a299b
more general dispatcher operations;

diff -r 440112959631 -r 24658c9d7c78 src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Wed Jun 14 16:03:02 2017 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Fri Jun 16 15:59:27 2017 +0200
@@ -33,6 +33,7 @@
 
   private val thread = Standard_Thread.fork(name, daemon) { main_loop(Nil) }
   def is_active: Boolean = active && thread.isAlive
+  def check_thread: Boolean = Thread.currentThread == thread
 
   private def failure(exn: Throwable): Unit =
     Output.error_message(
diff -r 440112959631 -r 24658c9d7c78 src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Wed Jun 14 16:03:02 2017 +0200
+++ b/src/Pure/GUI/gui_thread.scala	Fri Jun 16 15:59:27 2017 +0200
@@ -14,13 +14,13 @@
 {
   /* context check */
 
-  def assert[A](body: => A) =
+  def assert[A](body: => A): A =
   {
     Predef.assert(SwingUtilities.isEventDispatchThread())
     body
   }
 
-  def require[A](body: => A) =
+  def require[A](body: => A): A =
   {
     Predef.require(SwingUtilities.isEventDispatchThread())
     body
diff -r 440112959631 -r 24658c9d7c78 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Wed Jun 14 16:03:02 2017 +0200
+++ b/src/Pure/PIDE/editor.scala	Fri Jun 16 15:59:27 2017 +0200
@@ -45,4 +45,12 @@
   def hyperlink_command(
     focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
       : Option[Hyperlink]
+
+
+  /* dispatcher thread */
+
+  def assert_dispatcher[A](body: => A): A
+  def require_dispatcher[A](body: => A): A
+  def send_dispatcher(body: => Unit): Unit
+  def send_wait_dispatcher(body: => Unit): Unit
 }
diff -r 440112959631 -r 24658c9d7c78 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Wed Jun 14 16:03:02 2017 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Fri Jun 16 15:59:27 2017 +0200
@@ -48,7 +48,7 @@
   private val print_function = operation_name + "_query"
 
 
-  /* implicit state -- owned by GUI thread */
+  /* implicit state -- owned by editor thread */
 
   private val current_state = Synchronized(Query_Operation.State.empty)
 
@@ -67,7 +67,7 @@
 
   private def content_update()
   {
-    GUI_Thread.require {}
+    editor.require_dispatcher {}
 
 
     /* snapshot */
@@ -174,11 +174,11 @@
   /* query operations */
 
   def cancel_query(): Unit =
-    GUI_Thread.require { editor.session.cancel_exec(current_state.value.exec_id) }
+    editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) }
 
   def apply_query(query: List[String])
   {
-    GUI_Thread.require {}
+    editor.require_dispatcher {}
 
     editor.current_node_snapshot(editor_context) match {
       case Some(snapshot) =>
@@ -202,7 +202,7 @@
 
   def locate_query()
   {
-    GUI_Thread.require {}
+    editor.require_dispatcher {}
 
     val state = current_state.value
     for {
@@ -224,7 +224,7 @@
           if state.update_pending ||
             (state.status != Query_Operation.Status.FINISHED &&
               changed.commands.contains(command)) =>
-            GUI_Thread.later { content_update() }
+            editor.send_dispatcher { content_update() }
           case _ =>
         }
     }
diff -r 440112959631 -r 24658c9d7c78 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Jun 14 16:03:02 2017 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Jun 16 15:59:27 2017 +0200
@@ -136,11 +136,38 @@
   def reparse_limit: Int = session_options.int("editor_reparse_limit")
 
 
-  /* outlets */
+  /* dispatcher */
 
   private val dispatcher =
     Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
 
+  def assert_dispatcher[A](body: => A): A =
+  {
+    assert(dispatcher.check_thread)
+    body
+  }
+
+  def require_dispatcher[A](body: => A): A =
+  {
+    require(dispatcher.check_thread)
+    body
+  }
+
+  def send_dispatcher(body: => Unit): Unit =
+  {
+    if (dispatcher.check_thread) body
+    else dispatcher.send(() => body)
+  }
+
+  def send_wait_dispatcher(body: => Unit): Unit =
+  {
+    if (dispatcher.check_thread) body
+    else dispatcher.send_wait(() => body)
+  }
+
+
+  /* outlets */
+
   val statistics = new Session.Outlet[Session.Statistics](dispatcher)
   val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
   val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
diff -r 440112959631 -r 24658c9d7c78 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Jun 14 16:03:02 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Fri Jun 16 15:59:27 2017 +0200
@@ -458,5 +458,10 @@
     override def hyperlink_command(
       focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
         : Option[Hyperlink] = None
+
+    override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body)
+    override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body)
+    override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body)
+    override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body)
   }
 }
diff -r 440112959631 -r 24658c9d7c78 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jun 14 16:03:02 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Jun 16 15:59:27 2017 +0200
@@ -284,4 +284,12 @@
         hyperlink_command(focus, snapshot, id, range.start)
       case _ => None
     }
+
+
+  /* dispatcher thread */
+
+  override def assert_dispatcher[A](body: => A): A = GUI_Thread.assert(body)
+  override def require_dispatcher[A](body: => A): A = GUI_Thread.require(body)
+  override def send_dispatcher(body: => Unit): Unit = GUI_Thread.later(body)
+  override def send_wait_dispatcher(body: => Unit): Unit = GUI_Thread.now(body)
 }