--- 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,
--- /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 } }
+}
--- 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 } }
-}
--- 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
--- 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 _ =>
}
}
--- 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
--- 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
--- 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
--- 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
--- 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")
}
--- 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
--- 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 */
--- 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()
--- 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 =>
{
--- 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
--- 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()
--- 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)
--- 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() + ")") ::
--- 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
--- 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)
--- 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
--- 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")
--- 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() }
}
}
--- 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
}
--- 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() }
--- 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 {
--- 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 {
--- 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 */
--- 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 }
--- 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()
--- 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")
}
--- 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)
--- 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()
}
--- 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() }
--- 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() }
--- 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()
--- 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)
--- 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 =
--- 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
--- 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) {
--- 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()
--- 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()
--- 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