# HG changeset patch # User wenzelm # Date 1406107164 -7200 # Node ID 990ffb84489beca75e10d743d25c203b214a78df # Parent b6256ea3b7c5aa6e2bd9490687a1c6e48bc960ee clarified module name: facilitate alternative GUI frameworks; diff -r b6256ea3b7c5 -r 990ffb84489b src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Pure/GUI/gui.scala Wed Jul 23 11:19:24 2014 +0200 @@ -89,7 +89,7 @@ private def simple_dialog(kind: Int, default_title: String, parent: Component, title: String, message: Seq[Any]) { - Swing_Thread.now { + GUI_Thread.now { val java_message = message map { case x: scala.swing.Component => x.peer case x => x } JOptionPane.showMessageDialog(parent, java_message.toArray.asInstanceOf[Array[AnyRef]], @@ -107,7 +107,7 @@ simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message) def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int = - Swing_Thread.now { + GUI_Thread.now { val java_message = message map { case x: scala.swing.Component => x.peer case x => x } JOptionPane.showConfirmDialog(parent, java_message.toArray.asInstanceOf[Array[AnyRef]], title, diff -r b6256ea3b7c5 -r 990ffb84489b src/Pure/GUI/gui_thread.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/GUI/gui_thread.scala Wed Jul 23 11:19:24 2014 +0200 @@ -0,0 +1,57 @@ +/* Title: Pure/GUI/gui_thread.scala + Module: PIDE-GUI + Author: Makarius + +Evaluation within the GUI thread: implementation for AWT/Swing. +*/ + +package isabelle + + +import javax.swing.SwingUtilities + + +object GUI_Thread +{ + /* context check */ + + def assert[A](body: => A) = + { + Predef.assert(SwingUtilities.isEventDispatchThread()) + body + } + + def require[A](body: => A) = + { + Predef.require(SwingUtilities.isEventDispatchThread()) + body + } + + + /* event dispatch queue */ + + def now[A](body: => A): A = + { + if (SwingUtilities.isEventDispatchThread()) body + else { + lazy val result = { assert { Exn.capture(body) } } + SwingUtilities.invokeAndWait(new Runnable { def run = result }) + Exn.release(result) + } + } + + def later(body: => Unit) + { + if (SwingUtilities.isEventDispatchThread()) body + else SwingUtilities.invokeLater(new Runnable { def run = body }) + } + + + /* delayed events */ + + def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay = + Simple_Thread.delay_first(delay) { later { event } } + + def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay = + Simple_Thread.delay_last(delay) { later { event } } +} diff -r b6256ea3b7c5 -r 990ffb84489b src/Pure/GUI/swing_thread.scala --- a/src/Pure/GUI/swing_thread.scala Wed Jul 23 11:08:24 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -/* Title: Pure/GUI/swing_thread.scala - Module: PIDE-GUI - Author: Makarius - -Evaluation within the AWT/Swing thread. -*/ - -package isabelle - - -import javax.swing.SwingUtilities - - -object Swing_Thread -{ - /* context check */ - - def assert[A](body: => A) = - { - Predef.assert(SwingUtilities.isEventDispatchThread()) - body - } - - def require[A](body: => A) = - { - Predef.require(SwingUtilities.isEventDispatchThread()) - body - } - - - /* event dispatch queue */ - - def now[A](body: => A): A = - { - if (SwingUtilities.isEventDispatchThread()) body - else { - lazy val result = { assert { Exn.capture(body) } } - SwingUtilities.invokeAndWait(new Runnable { def run = result }) - Exn.release(result) - } - } - - def later(body: => Unit) - { - if (SwingUtilities.isEventDispatchThread()) body - else SwingUtilities.invokeLater(new Runnable { def run = body }) - } - - - /* delayed events */ - - def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay = - Simple_Thread.delay_first(delay) { later { event } } - - def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay = - Simple_Thread.delay_last(delay) { later { event } } -} diff -r b6256ea3b7c5 -r 990ffb84489b src/Pure/GUI/system_dialog.scala --- a/src/Pure/GUI/system_dialog.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Pure/GUI/system_dialog.scala Wed Jul 23 11:19:24 2014 +0200 @@ -18,7 +18,7 @@ class System_Dialog extends Build.Progress { - /* GUI state -- owned by Swing thread */ + /* component state -- owned by GUI thread */ private var _title = "Isabelle" private var _window: Option[Window] = None @@ -26,7 +26,7 @@ private def check_window(): Window = { - Swing_Thread.require {} + GUI_Thread.require {} _window match { case Some(window) => window @@ -48,7 +48,7 @@ private def conclude() { - Swing_Thread.require {} + GUI_Thread.require {} require(_return_code.isDefined) _window match { @@ -142,7 +142,7 @@ /* exit */ val delay_exit = - Swing_Thread.delay_first(Time.seconds(1.0)) + GUI_Thread.delay_first(Time.seconds(1.0)) { if (can_auto_close) conclude() else { @@ -160,13 +160,13 @@ /* progress operations */ def title(txt: String): Unit = - Swing_Thread.later { + GUI_Thread.later { _title = txt _window.foreach(window => window.title = txt) } def return_code(rc: Int): Unit = - Swing_Thread.later { + GUI_Thread.later { _return_code = Some(rc) _window match { case None => conclude() @@ -175,7 +175,7 @@ } override def echo(txt: String): Unit = - Swing_Thread.later { + GUI_Thread.later { val window = check_window() window.text.append(txt + "\n") val vertical = window.scroll_text.peer.getVerticalScrollBar diff -r b6256ea3b7c5 -r 990ffb84489b src/Pure/PIDE/query_operation.scala --- a/src/Pure/PIDE/query_operation.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Pure/PIDE/query_operation.scala Wed Jul 23 11:19:24 2014 +0200 @@ -28,7 +28,7 @@ private val instance = Document_ID.make().toString - /* implicit state -- owned by Swing thread */ + /* implicit state -- owned by GUI thread */ @volatile private var current_location: Option[Command] = None @volatile private var current_query: List[String] = Nil @@ -62,7 +62,7 @@ private def content_update() { - Swing_Thread.require {} + GUI_Thread.require {} /* snapshot */ @@ -167,11 +167,11 @@ /* query operations */ def cancel_query(): Unit = - Swing_Thread.require { editor.session.cancel_exec(current_exec_id) } + GUI_Thread.require { editor.session.cancel_exec(current_exec_id) } def apply_query(query: List[String]) { - Swing_Thread.require {} + GUI_Thread.require {} editor.current_node_snapshot(editor_context) match { case Some(snapshot) => @@ -196,7 +196,7 @@ def locate_query() { - Swing_Thread.require {} + GUI_Thread.require {} for { command <- current_location @@ -216,7 +216,7 @@ if current_update_pending || (current_status != Query_Operation.Status.FINISHED && changed.commands.contains(command)) => - Swing_Thread.later { content_update() } + GUI_Thread.later { content_update() } case _ => } } diff -r b6256ea3b7c5 -r 990ffb84489b src/Pure/Tools/ml_statistics.scala --- a/src/Pure/Tools/ml_statistics.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Pure/Tools/ml_statistics.scala Wed Jul 23 11:19:24 2014 +0200 @@ -131,7 +131,7 @@ def show_standard_frames(): Unit = ML_Statistics.standard_fields.map(chart(_)).foreach(c => - Swing_Thread.later { + GUI_Thread.later { new Frame { iconImage = GUI.isabelle_image() title = name diff -r b6256ea3b7c5 -r 990ffb84489b src/Pure/Tools/task_statistics.scala --- a/src/Pure/Tools/task_statistics.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Pure/Tools/task_statistics.scala Wed Jul 23 11:19:24 2014 +0200 @@ -51,7 +51,7 @@ } def show_frame(bins: Int = 100): Unit = - Swing_Thread.later { + GUI_Thread.later { new Frame { iconImage = GUI.isabelle_image() title = name diff -r b6256ea3b7c5 -r 990ffb84489b src/Pure/build-jars --- a/src/Pure/build-jars Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Pure/build-jars Wed Jul 23 11:19:24 2014 +0200 @@ -42,10 +42,10 @@ General/xz_file.scala GUI/color_value.scala GUI/gui.scala + GUI/gui_thread.scala GUI/html5_panel.scala GUI/jfx_thread.scala GUI/popup.scala - GUI/swing_thread.scala GUI/system_dialog.scala GUI/wrap_panel.scala Isar/keyword.scala diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/Graphview/src/mutator_event.scala --- a/src/Tools/Graphview/src/mutator_event.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/Graphview/src/mutator_event.scala Wed Jul 23 11:19:24 2014 +0200 @@ -28,8 +28,8 @@ { private val receivers = new mutable.ListBuffer[Receiver] - def += (r: Receiver) { Swing_Thread.require {}; receivers += r } - def -= (r: Receiver) { Swing_Thread.require {}; receivers -= r } - def event(x: Message) { Swing_Thread.require {}; receivers.foreach(r => r(x)) } + def += (r: Receiver) { GUI_Thread.require {}; receivers += r } + def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r } + def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) } } } \ No newline at end of file diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/active.scala Wed Jul 23 11:19:24 2014 +0200 @@ -16,7 +16,7 @@ { def action(view: View, text: String, elem: XML.Elem) { - Swing_Thread.require {} + GUI_Thread.require {} Document_View(view.getTextArea) match { case Some(doc_view) => @@ -45,11 +45,11 @@ isabelle.graphview.Model.decode_graph(body) .transitive_reduction_acyclic } - Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) } + GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) } } case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) => - Swing_Thread.later { + GUI_Thread.later { view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace") } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Wed Jul 23 11:19:24 2014 +0200 @@ -52,7 +52,7 @@ def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] = { - Swing_Thread.require {} + GUI_Thread.require {} text_area.getClientProperty(key) match { case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion) case _ => None @@ -78,7 +78,7 @@ def exit(text_area: JEditTextArea) { - Swing_Thread.require {} + GUI_Thread.require {} apply(text_area) match { case None => case Some(text_area_completion) => @@ -98,7 +98,7 @@ def dismissed(text_area: TextArea): Boolean = { - Swing_Thread.require {} + GUI_Thread.require {} apply(text_area) match { case Some(text_area_completion) => text_area_completion.dismissed() case None => false @@ -108,7 +108,7 @@ class Text_Area private(text_area: JEditTextArea) { - // owned by Swing thread + // owned by GUI thread private var completion_popup: Option[Completion_Popup] = None def active_range: Option[Text.Range] = @@ -255,7 +255,7 @@ private def insert(item: Completion.Item) { - Swing_Thread.require {} + GUI_Thread.require {} val buffer = text_area.getBuffer val range = item.range @@ -425,7 +425,7 @@ def input(evt: KeyEvent) { - Swing_Thread.require {} + GUI_Thread.require {} if (PIDE.options.bool("jedit_completion")) { if (!evt.isConsumed) { @@ -449,7 +449,7 @@ } private val input_delay = - Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { + GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { action() } @@ -458,7 +458,7 @@ def dismissed(): Boolean = { - Swing_Thread.require {} + GUI_Thread.require {} completion_popup match { case Some(completion) => @@ -504,7 +504,7 @@ // see https://forums.oracle.com/thread/1361677 if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret) - // owned by Swing thread + // owned by GUI thread private var completion_popup: Option[Completion_Popup] = None @@ -527,7 +527,7 @@ private def insert(item: Completion.Item) { - Swing_Thread.require {} + GUI_Thread.require {} val range = item.range if (text_field.isEditable) { @@ -606,7 +606,7 @@ } private val process_delay = - Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { + GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { action() } @@ -642,7 +642,7 @@ { completion => - Swing_Thread.require {} + GUI_Thread.require {} require(!items.isEmpty) val multi = items.length > 1 diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Jul 23 11:19:24 2014 +0200 @@ -25,7 +25,7 @@ def apply(buffer: Buffer): Option[Document_Model] = { - Swing_Thread.require {} + GUI_Thread.require {} buffer.getProperty(key) match { case model: Document_Model => Some(model) case _ => None @@ -34,7 +34,7 @@ def exit(buffer: Buffer) { - Swing_Thread.require {} + GUI_Thread.require {} apply(buffer) match { case None => case Some(model) => @@ -46,7 +46,7 @@ def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model = { - Swing_Thread.require {} + GUI_Thread.require {} apply(buffer).map(_.deactivate) val model = new Document_Model(session, buffer, node_name) buffer.setProperty(key, model) @@ -65,7 +65,7 @@ def node_header(): Document.Node.Header = { - Swing_Thread.require {} + GUI_Thread.require {} if (is_theory) { JEdit_Lib.buffer_lock(buffer) { @@ -83,12 +83,12 @@ /* perspective */ - // owned by Swing thread + // owned by GUI thread private var _node_required = false def node_required: Boolean = _node_required def node_required_=(b: Boolean) { - Swing_Thread.require {} + GUI_Thread.require {} if (_node_required != b && is_theory) { _node_required = b PIDE.options_changed() @@ -98,7 +98,7 @@ def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = { - Swing_Thread.require {} + GUI_Thread.require {} if (Isabelle.continuous_checking && is_theory) { val snapshot = this.snapshot() @@ -135,12 +135,12 @@ /* blob */ - private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None // owned by Swing thread + private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None // owned by GUI thread - private def reset_blob(): Unit = Swing_Thread.require { _blob = None } + private def reset_blob(): Unit = GUI_Thread.require { _blob = None } def get_blob(): Option[Document.Blob] = - Swing_Thread.require { + GUI_Thread.require { if (is_theory) None else { val (bytes, chunk) = @@ -184,7 +184,7 @@ /* pending edits */ - private object pending_edits // owned by Swing thread + private object pending_edits // owned by GUI thread { private var pending_clear = false private val pending = new mutable.ListBuffer[Text.Edit] @@ -221,10 +221,10 @@ } def snapshot(): Document.Snapshot = - Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) } + GUI_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) } def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] = - Swing_Thread.require { pending_edits.flushed_edits(doc_blobs) } + GUI_Thread.require { pending_edits.flushed_edits(doc_blobs) } /* buffer listener */ diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Wed Jul 23 11:19:24 2014 +0200 @@ -27,7 +27,7 @@ def apply(text_area: TextArea): Option[Document_View] = { - Swing_Thread.require {} + GUI_Thread.require {} text_area.getClientProperty(key) match { case doc_view: Document_View => Some(doc_view) case _ => None @@ -36,7 +36,7 @@ def exit(text_area: JEditTextArea) { - Swing_Thread.require {} + GUI_Thread.require {} apply(text_area) match { case None => case Some(doc_view) => @@ -71,7 +71,7 @@ def perspective(snapshot: Document.Snapshot): Text.Perspective = { - Swing_Thread.require {} + GUI_Thread.require {} val active_command = { @@ -125,7 +125,7 @@ start: Array[Int], end: Array[Int], y: Int, line_height: Int) { rich_text_area.robust_body(()) { - Swing_Thread.assert {} + GUI_Thread.assert {} val gutter = text_area.getGutter val width = GutterOptionPane.getSelectionAreaWidth @@ -173,7 +173,7 @@ /* caret handling */ private val delay_caret_update = - Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { + GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { session.caret_focus.post(Session.Caret_Focus) } @@ -187,7 +187,7 @@ private object overview extends Text_Overview(this) { val delay_repaint = - Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() } + GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() } } @@ -200,7 +200,7 @@ case changed: Session.Commands_Changed => val buffer = model.buffer - Swing_Thread.later { + GUI_Thread.later { JEdit_Lib.buffer_lock(buffer) { if (model.buffer == text_area.getBuffer) { val snapshot = model.snapshot() diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/font_info.scala --- a/src/Tools/jEdit/src/font_info.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/font_info.scala Wed Jul 23 11:19:24 2014 +0200 @@ -42,7 +42,7 @@ { private def change_size(change: Float => Float) { - Swing_Thread.require {} + GUI_Thread.require {} val size0 = main_size() val size = restrict_size(change(size0)).round @@ -54,9 +54,9 @@ } } - // owned by Swing thread + // owned by GUI thread private var steps = 0 - private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) + private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { change_size(size => { diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -20,7 +20,7 @@ object Graphview_Dockable { - /* implicit arguments -- owned by Swing thread */ + /* implicit arguments -- owned by GUI thread */ private var implicit_snapshot = Document.Snapshot.init @@ -29,7 +29,7 @@ private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph]) { - Swing_Thread.require {} + GUI_Thread.require {} implicit_snapshot = snapshot implicit_graph = graph diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/info_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -20,7 +20,7 @@ object Info_Dockable { - /* implicit arguments -- owned by Swing thread */ + /* implicit arguments -- owned by GUI thread */ private var implicit_snapshot = Document.Snapshot.init private var implicit_results = Command.Results.empty @@ -28,7 +28,7 @@ private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body) { - Swing_Thread.require {} + GUI_Thread.require {} implicit_snapshot = snapshot implicit_results = results @@ -48,7 +48,7 @@ class Info_Dockable(view: View, position: String) extends Dockable(view, position) { - /* component state -- owned by Swing thread */ + /* component state -- owned by GUI thread */ private val snapshot = Info_Dockable.implicit_snapshot private val results = Info_Dockable.implicit_results @@ -72,7 +72,7 @@ private def handle_resize() { - Swing_Thread.require {} + GUI_Thread.require {} pretty_text_area.resize( Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) @@ -82,7 +82,7 @@ /* resize */ private val delay_resize = - Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } @@ -97,7 +97,7 @@ private val main = Session.Consumer[Session.Global_Options](getClass.getName) { - case _: Session.Global_Options => Swing_Thread.later { handle_resize() } + case _: Session.Global_Options => GUI_Thread.later { handle_resize() } } override def init() diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Wed Jul 23 11:19:24 2014 +0200 @@ -153,7 +153,7 @@ def continuous_checking_=(b: Boolean) { - Swing_Thread.require {} + GUI_Thread.require {} if (continuous_checking != b) { PIDE.options.bool(CONTINUOUS_CHECKING) = b @@ -179,7 +179,7 @@ private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false) { - Swing_Thread.require {} + GUI_Thread.require {} PIDE.document_model(view.getBuffer) match { case Some(model) => model.node_required = (if (toggle) !model.node_required else set) diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Jul 23 11:19:24 2014 +0200 @@ -29,7 +29,7 @@ def logic_selector(autosave: Boolean): Option_Component = { - Swing_Thread.require {} + GUI_Thread.require {} val entries = new Logic_Entry("", "default (" + jedit_logic() + ")") :: diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Jul 23 11:19:24 2014 +0200 @@ -149,7 +149,7 @@ override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { val opt_snapshot = - Swing_Thread.now { + GUI_Thread.now { Document_Model(buffer) match { case Some(model) if model.is_theory => Some(model.snapshot) case _ => None diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Jul 23 11:19:24 2014 +0200 @@ -22,15 +22,15 @@ override def session: Session = PIDE.session - // owned by Swing thread + // owned by GUI thread private var removed_nodes = Set.empty[Document.Node.Name] def remove_node(name: Document.Node.Name): Unit = - Swing_Thread.require { removed_nodes += name } + GUI_Thread.require { removed_nodes += name } override def flush() { - Swing_Thread.require {} + GUI_Thread.require {} val doc_blobs = PIDE.document_blobs() val models = PIDE.document_models() @@ -45,7 +45,7 @@ } private val delay_flush = - Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } + GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } def invoke(): Unit = delay_flush.invoke() @@ -53,17 +53,17 @@ /* current situation */ override def current_context: View = - Swing_Thread.require { jEdit.getActiveView() } + GUI_Thread.require { jEdit.getActiveView() } override def current_node(view: View): Option[Document.Node.Name] = - Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) } + GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) } override def current_node_snapshot(view: View): Option[Document.Snapshot] = - Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) } + GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) } override def node_snapshot(name: Document.Node.Name): Document.Snapshot = { - Swing_Thread.require {} + GUI_Thread.require {} JEdit_Lib.jedit_buffer(name) match { case Some(buffer) => @@ -77,7 +77,7 @@ override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = { - Swing_Thread.require {} + GUI_Thread.require {} val text_area = view.getTextArea val buffer = view.getBuffer @@ -138,7 +138,7 @@ def goto_file(view: View, name: String, line: Int = 0, column: Int = 0) { - Swing_Thread.require {} + GUI_Thread.require {} push_position(view) diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Jul 23 11:19:24 2014 +0200 @@ -75,7 +75,7 @@ def window_geometry(outer: Container, inner: Component): Window_Geometry = { - Swing_Thread.require {} + GUI_Thread.require {} val old_content = dummy_window.getContentPane diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_options.scala Wed Jul 23 11:19:24 2014 +0200 @@ -36,7 +36,7 @@ def make_color_component(opt: Options.Opt): Option_Component = { - Swing_Thread.require {} + GUI_Thread.require {} val opt_name = opt.name val opt_title = opt.title("jedit") @@ -55,7 +55,7 @@ def make_component(opt: Options.Opt): Option_Component = { - Swing_Thread.require {} + GUI_Thread.require {} val opt_name = opt.name val opt_title = opt.title("jedit") diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Jul 23 11:19:24 2014 +0200 @@ -62,7 +62,7 @@ override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { - Swing_Thread.now { + GUI_Thread.now { JEdit_Lib.jedit_buffer(name) match { case Some(buffer) => JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) } @@ -113,7 +113,7 @@ override def commit(change: Session.Change) { - if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() } + if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() } } } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -22,13 +22,13 @@ private val rev_stats = Synchronized(Nil: List[Properties.T]) - /* chart data -- owned by Swing thread */ + /* chart data -- owned by GUI thread */ private val chart = ML_Statistics.empty.chart(null, Nil) private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection] private val delay_update = - Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { + GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { ML_Statistics("", rev_stats.value.reverse) .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -20,7 +20,7 @@ class Output_Dockable(view: View, position: String) extends Dockable(view, position) { - /* component state -- owned by Swing thread */ + /* component state -- owned by GUI thread */ private var do_update = true private var current_snapshot = Document.Snapshot.init @@ -41,7 +41,7 @@ private def handle_resize() { - Swing_Thread.require {} + GUI_Thread.require {} pretty_text_area.resize( Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) @@ -49,7 +49,7 @@ private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) { - Swing_Thread.require {} + GUI_Thread.require {} val (new_snapshot, new_command, new_results) = PIDE.editor.current_node_snapshot(view) match { @@ -88,14 +88,14 @@ private val main = Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => - Swing_Thread.later { handle_resize() } + GUI_Thread.later { handle_resize() } case changed: Session.Commands_Changed => val restriction = if (changed.assignment) None else Some(changed.commands) - Swing_Thread.later { handle_update(do_update, restriction) } + GUI_Thread.later { handle_update(do_update, restriction) } case Session.Caret_Focus => - Swing_Thread.later { handle_update(do_update, None) } + GUI_Thread.later { handle_update(do_update, None) } } override def init() @@ -118,7 +118,7 @@ /* resize */ private val delay_resize = - Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Wed Jul 23 11:19:24 2014 +0200 @@ -90,7 +90,7 @@ def exit_models(buffers: List[Buffer]) { - Swing_Thread.now { + GUI_Thread.now { PIDE.editor.flush() buffers.foreach(buffer => JEdit_Lib.buffer_lock(buffer) { @@ -102,7 +102,7 @@ def init_models() { - Swing_Thread.now { + GUI_Thread.now { PIDE.editor.flush() for { @@ -128,7 +128,7 @@ } def init_view(buffer: Buffer, text_area: JEditTextArea): Unit = - Swing_Thread.now { + GUI_Thread.now { JEdit_Lib.buffer_lock(buffer) { document_model(buffer) match { case Some(model) => Document_View.init(model, text_area) @@ -138,7 +138,7 @@ } def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit = - Swing_Thread.now { + GUI_Thread.now { JEdit_Lib.buffer_lock(buffer) { Document_View.exit(text_area) } @@ -147,7 +147,7 @@ /* current document content */ - def snapshot(view: View): Document.Snapshot = Swing_Thread.now + def snapshot(view: View): Document.Snapshot = GUI_Thread.now { val buffer = view.getBuffer document_model(buffer) match { @@ -156,7 +156,7 @@ } } - def rendering(view: View): Rendering = Swing_Thread.now + def rendering(view: View): Rendering = GUI_Thread.now { val text_area = view.getTextArea document_view(text_area) match { @@ -186,7 +186,7 @@ /* theory files */ private lazy val delay_init = - Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) + GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { PIDE.init_models() } @@ -196,7 +196,7 @@ delay_load_active.guarded_access(a => Some((!a, true))) private lazy val delay_load = - Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) + GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { if (Isabelle.continuous_checking && delay_load_activated()) { try { @@ -215,7 +215,7 @@ } yield (model.node_name, Position.none) val thy_info = new Thy_Info(PIDE.resources) - // FIXME avoid I/O in Swing thread!?! + // FIXME avoid I/O on GUI thread!?! val files = thy_info.dependencies("", thys).deps.map(_.name.node). filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file)) @@ -255,7 +255,7 @@ private val session_phase = Session.Consumer[Session.Phase](getClass.getName) { case Session.Inactive | Session.Failed => - Swing_Thread.later { + GUI_Thread.later { GUI.error_dialog(jEdit.getActiveView, "Prover process terminated", "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content())) } @@ -277,7 +277,7 @@ override def handleMessage(message: EBMessage) { - Swing_Thread.assert {} + GUI_Thread.assert {} if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) { message match { diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Jul 23 11:19:24 2014 +0200 @@ -68,7 +68,7 @@ { text_area => - Swing_Thread.require {} + GUI_Thread.require {} private var current_font_info: Font_Info = Font_Info.main() private var current_body: XML.Body = Nil @@ -83,13 +83,13 @@ get_search_pattern _, caret_visible = false, enable_hovering = true) private var current_search_pattern: Option[Regex] = None - def get_search_pattern(): Option[Regex] = Swing_Thread.require { current_search_pattern } + def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern } def get_background(): Option[Color] = None def refresh() { - Swing_Thread.require {} + GUI_Thread.require {} val font = current_font_info.font getPainter.setFont(font) @@ -137,7 +137,7 @@ catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } Exn.Interrupt.expose() - Swing_Thread.later { + GUI_Thread.later { current_rendering = rendering JEdit_Lib.buffer_edit(getBuffer) { rich_text_area.active_reset() @@ -154,7 +154,7 @@ def resize(font_info: Font_Info) { - Swing_Thread.require {} + GUI_Thread.require {} current_font_info = font_info refresh() @@ -162,7 +162,7 @@ def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body) { - Swing_Thread.require {} + GUI_Thread.require {} require(!base_snapshot.is_outdated) current_base_snapshot = base_snapshot @@ -173,7 +173,7 @@ def detach { - Swing_Thread.require {} + GUI_Thread.require {} Info_Dockable(view, current_base_snapshot, current_base_results, current_body) } @@ -191,7 +191,7 @@ Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") { private val input_delay = - Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { + GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { search_action(this) } getDocument.addDocumentListener(new DocumentListener { diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Jul 23 11:19:24 2014 +0200 @@ -25,19 +25,19 @@ { /* tooltip hierarchy */ - // owned by Swing thread + // owned by GUI thread private var stack: List[Pretty_Tooltip] = Nil private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] = { - Swing_Thread.require {} + GUI_Thread.require {} if (stack.contains(tip)) Some(stack.span(_ != tip)) else None } private def descendant(parent: JComponent): Option[Pretty_Tooltip] = - Swing_Thread.require { stack.find(tip => tip.original_parent == parent) } + GUI_Thread.require { stack.find(tip => tip.original_parent == parent) } def apply( view: View, @@ -47,7 +47,7 @@ results: Command.Results, info: Text.Info[XML.Body]) { - Swing_Thread.require {} + GUI_Thread.require {} stack match { case top :: _ if top.results == results && top.info == info => @@ -71,13 +71,13 @@ } - /* pending event and active state */ // owned by Swing thread + /* pending event and active state */ // owned by GUI thread private var pending: Option[() => Unit] = None private var active = true private val pending_delay = - Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { + GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { pending match { case Some(body) => pending = None; body() case None => @@ -85,7 +85,7 @@ } def invoke(body: () => Unit): Unit = - Swing_Thread.require { + GUI_Thread.require { if (active) { pending = Some(body) pending_delay.invoke() @@ -93,18 +93,18 @@ } def revoke(): Unit = - Swing_Thread.require { + GUI_Thread.require { pending = None pending_delay.revoke() } private lazy val reactivate_delay = - Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { + GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { active = true } private def deactivate(): Unit = - Swing_Thread.require { + GUI_Thread.require { revoke() active = false reactivate_delay.invoke() @@ -113,7 +113,7 @@ /* dismiss */ - private lazy val focus_delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) + private lazy val focus_delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { dismiss_unfocused() } @@ -173,7 +173,7 @@ { tip => - Swing_Thread.require {} + GUI_Thread.require {} /* controls */ diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/protocol_dockable.scala --- a/src/Tools/jEdit/src/protocol_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/protocol_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -25,10 +25,10 @@ private val main = Session.Consumer[Prover.Message](getClass.getName) { case input: Prover.Input => - Swing_Thread.later { text_area.append(input.toString + "\n\n") } + GUI_Thread.later { text_area.append(input.toString + "\n\n") } case output: Prover.Output => - Swing_Thread.later { text_area.append(output.message.toString + "\n\n") } + GUI_Thread.later { text_area.append(output.message.toString + "\n\n") } } override def init() { PIDE.session.all_messages += main } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/query_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -307,7 +307,7 @@ /* resize */ private def handle_resize(): Unit = - Swing_Thread.require { + GUI_Thread.require { for (op <- operations) { op.pretty_text_area.resize( Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) @@ -315,7 +315,7 @@ } private val delay_resize = - Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } @@ -326,7 +326,7 @@ private val main = Session.Consumer[Session.Global_Options](getClass.getName) { - case _: Session.Global_Options => Swing_Thread.later { handle_resize() } + case _: Session.Global_Options => GUI_Thread.later { handle_resize() } } override def init() diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/raw_output_dockable.scala --- a/src/Tools/jEdit/src/raw_output_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -25,7 +25,7 @@ private val main = Session.Consumer[Prover.Output](getClass.getName) { case output: Prover.Output => - Swing_Thread.later { + GUI_Thread.later { text_area.append(XML.content(output.message)) if (!output.is_stdout && !output.is_stderr) text_area.append("\n") } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Jul 23 11:19:24 2014 +0200 @@ -43,7 +43,7 @@ def robust_body[A](default: A)(body: => A): A = { try { - Swing_Thread.require {} + GUI_Thread.require {} if (buffer == text_area.getBuffer) body else { Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer")) @@ -143,7 +143,7 @@ def reset { update(None) } } - // owned by Swing thread + // owned by GUI thread private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _, None) diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/scala_console.scala Wed Jul 23 11:19:24 2014 +0200 @@ -57,7 +57,7 @@ } - /* global state -- owned by Swing thread */ + /* global state -- owned by GUI thread */ @volatile private var interpreters = Map.empty[Console, Interpreter] @@ -72,7 +72,7 @@ { val s = buf.synchronized { val s = buf.toString; buf.clear; s } val str = UTF8.decode_permissive(s) - Swing_Thread.later { + GUI_Thread.later { if (global_out == null) System.out.print(str) else global_out.writeAttrs(null, str) } @@ -124,7 +124,7 @@ private def report_error(str: String) { if (global_console == null || global_err == null) System.err.println(str) - else Swing_Thread.later { global_err.print(global_console.getErrorColor, str) } + else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) } } @@ -167,7 +167,7 @@ running.change(_ => None) Thread.interrupted() } - Swing_Thread.later { + GUI_Thread.later { if (err != null) err.commandDone() out.commandDone() } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -20,9 +20,9 @@ class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) { - Swing_Thread.require {} + GUI_Thread.require {} - /* component state -- owned by Swing thread */ + /* component state -- owned by GUI thread */ private var current_snapshot = Document.State.init.snapshot() private var current_command = Command.empty @@ -37,7 +37,7 @@ private def update_contents() { - Swing_Thread.require {} + GUI_Thread.require {} val snapshot = current_snapshot val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results) @@ -71,7 +71,7 @@ private def do_paint() { - Swing_Thread.later { + GUI_Thread.later { text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale"))) } } @@ -111,21 +111,21 @@ private val main = Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => - Swing_Thread.later { handle_resize() } + GUI_Thread.later { handle_resize() } case changed: Session.Commands_Changed => - Swing_Thread.later { handle_update(do_update) } + GUI_Thread.later { handle_update(do_update) } case Session.Caret_Focus => - Swing_Thread.later { handle_update(do_update) } + GUI_Thread.later { handle_update(do_update) } case Simplifier_Trace.Event => - Swing_Thread.later { handle_update(do_update) } + GUI_Thread.later { handle_update(do_update) } } override def init() { - Swing_Thread.require {} + GUI_Thread.require {} PIDE.session.global_options += main PIDE.session.commands_changed += main @@ -136,7 +136,7 @@ override def exit() { - Swing_Thread.require {} + GUI_Thread.require {} PIDE.session.global_options -= main PIDE.session.commands_changed -= main @@ -149,7 +149,7 @@ /* resize */ private val delay_resize = - Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/simplifier_trace_window.scala --- a/src/Tools/jEdit/src/simplifier_trace_window.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Wed Jul 23 11:19:24 2014 +0200 @@ -136,7 +136,7 @@ class Simplifier_Trace_Window( view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame { - Swing_Thread.require {} + GUI_Thread.require {} private val pretty_text_area = new Pretty_Text_Area(view) private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() } @@ -167,7 +167,7 @@ def do_paint() { - Swing_Thread.later { + GUI_Thread.later { pretty_text_area.resize( Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) } @@ -182,7 +182,7 @@ /* resize */ private val delay_resize = - Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } peer.addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -55,14 +55,14 @@ private def handle_resize() { - Swing_Thread.require {} + GUI_Thread.require {} pretty_text_area.resize( Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) } private val delay_resize = - Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } @@ -135,7 +135,7 @@ private val main = Session.Consumer[Session.Global_Options](getClass.getName) { - case _: Session.Global_Options => Swing_Thread.later { update_provers(); handle_resize() } + case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() } } override def init() diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/spell_checker.scala --- a/src/Tools/jEdit/src/spell_checker.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/spell_checker.scala Wed Jul 23 11:19:24 2014 +0200 @@ -105,7 +105,7 @@ def dictionaries_selector(): Option_Component = { - Swing_Thread.require {} + GUI_Thread.require {} val option_name = "spell_checker_dictionary" val opt = PIDE.options.value.check_name(option_name) diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -70,7 +70,7 @@ val search_space = (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList val search_delay = - Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { + GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { val search_words = Word.explode(Word.lowercase(search_field.text)) val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0 val results = diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/syslog_dockable.scala --- a/src/Tools/jEdit/src/syslog_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/syslog_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -20,7 +20,7 @@ private val syslog = new TextArea() - private def syslog_delay = Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) + private def syslog_delay = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { val text = PIDE.session.syslog_content() if (text != syslog.text) syslog.text = text diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/text_overview.scala Wed Jul 23 11:19:24 2014 +0200 @@ -64,7 +64,7 @@ override def paintComponent(gfx: Graphics) { super.paintComponent(gfx) - Swing_Thread.assert {} + GUI_Thread.assert {} doc_view.rich_text_area.robust_body(()) { JEdit_Lib.buffer_lock(buffer) { diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -73,7 +73,7 @@ private def handle_phase(phase: Session.Phase) { - Swing_Thread.require {} + GUI_Thread.require {} session_phase.text = " " + phase_text(phase) + " " } @@ -87,7 +87,7 @@ add(controls.peer, BorderLayout.NORTH) - /* component state -- owned by Swing thread */ + /* component state -- owned by GUI thread */ private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty private var nodes_required: Set[Document.Node.Name] = Set.empty @@ -192,7 +192,7 @@ private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) { - Swing_Thread.require {} + GUI_Thread.require {} val snapshot = PIDE.session.snapshot() @@ -220,10 +220,10 @@ private val main = Session.Consumer[Any](getClass.getName) { case phase: Session.Phase => - Swing_Thread.later { handle_phase(phase) } + GUI_Thread.later { handle_phase(phase) } case _: Session.Global_Options => - Swing_Thread.later { + GUI_Thread.later { continuous_checking.load() logic.load () update_nodes_required() @@ -231,7 +231,7 @@ } case changed: Session.Commands_Changed => - Swing_Thread.later { handle_update(Some(changed.nodes)) } + GUI_Thread.later { handle_update(Some(changed.nodes)) } } override def init() diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Jul 23 11:19:24 2014 +0200 @@ -145,13 +145,13 @@ add(controls.peer, BorderLayout.NORTH) - /* component state -- owned by Swing thread */ + /* component state -- owned by GUI thread */ private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing] private def make_entries(): List[Entry] = { - Swing_Thread.require {} + GUI_Thread.require {} val name = Document_View(view.getTextArea) match { @@ -174,7 +174,7 @@ private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) { - Swing_Thread.require {} + GUI_Thread.require {} val snapshot = PIDE.session.snapshot() @@ -204,7 +204,7 @@ private val main = Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => - Swing_Thread.later { handle_update(Some(changed.nodes)) } + GUI_Thread.later { handle_update(Some(changed.nodes)) } } override def init() diff -r b6256ea3b7c5 -r 990ffb84489b src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Wed Jul 23 11:08:24 2014 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Wed Jul 23 11:19:24 2014 +0200 @@ -42,7 +42,7 @@ def edit_control_style(text_area: TextArea, control: String) { - Swing_Thread.assert {} + GUI_Thread.assert {} val buffer = text_area.getBuffer