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