clarified module name: facilitate alternative GUI frameworks;
authorwenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612990ffb84489b
parent 57611 b6256ea3b7c5
child 57613 4c6d44a3a079
clarified module name: facilitate alternative GUI frameworks;
src/Pure/GUI/gui.scala
src/Pure/GUI/gui_thread.scala
src/Pure/GUI/swing_thread.scala
src/Pure/GUI/system_dialog.scala
src/Pure/PIDE/query_operation.scala
src/Pure/Tools/ml_statistics.scala
src/Pure/Tools/task_statistics.scala
src/Pure/build-jars
src/Tools/Graphview/src/mutator_event.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_logic.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_options.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/monitor_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/protocol_dockable.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/scala_console.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/spell_checker.scala
src/Tools/jEdit/src/symbols_dockable.scala
src/Tools/jEdit/src/syslog_dockable.scala
src/Tools/jEdit/src/text_overview.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Pure/GUI/gui.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4    private def simple_dialog(kind: Int, default_title: String,
     1.5      parent: Component, title: String, message: Seq[Any])
     1.6    {
     1.7 -    Swing_Thread.now {
     1.8 +    GUI_Thread.now {
     1.9        val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
    1.10        JOptionPane.showMessageDialog(parent,
    1.11          java_message.toArray.asInstanceOf[Array[AnyRef]],
    1.12 @@ -107,7 +107,7 @@
    1.13      simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
    1.14  
    1.15    def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
    1.16 -    Swing_Thread.now {
    1.17 +    GUI_Thread.now {
    1.18        val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
    1.19        JOptionPane.showConfirmDialog(parent,
    1.20          java_message.toArray.asInstanceOf[Array[AnyRef]], title,
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/GUI/gui_thread.scala	Wed Jul 23 11:19:24 2014 +0200
     2.3 @@ -0,0 +1,57 @@
     2.4 +/*  Title:      Pure/GUI/gui_thread.scala
     2.5 +    Module:     PIDE-GUI
     2.6 +    Author:     Makarius
     2.7 +
     2.8 +Evaluation within the GUI thread: implementation for AWT/Swing.
     2.9 +*/
    2.10 +
    2.11 +package isabelle
    2.12 +
    2.13 +
    2.14 +import javax.swing.SwingUtilities
    2.15 +
    2.16 +
    2.17 +object GUI_Thread
    2.18 +{
    2.19 +  /* context check */
    2.20 +
    2.21 +  def assert[A](body: => A) =
    2.22 +  {
    2.23 +    Predef.assert(SwingUtilities.isEventDispatchThread())
    2.24 +    body
    2.25 +  }
    2.26 +
    2.27 +  def require[A](body: => A) =
    2.28 +  {
    2.29 +    Predef.require(SwingUtilities.isEventDispatchThread())
    2.30 +    body
    2.31 +  }
    2.32 +
    2.33 +
    2.34 +  /* event dispatch queue */
    2.35 +
    2.36 +  def now[A](body: => A): A =
    2.37 +  {
    2.38 +    if (SwingUtilities.isEventDispatchThread()) body
    2.39 +    else {
    2.40 +      lazy val result = { assert { Exn.capture(body) } }
    2.41 +      SwingUtilities.invokeAndWait(new Runnable { def run = result })
    2.42 +      Exn.release(result)
    2.43 +    }
    2.44 +  }
    2.45 +
    2.46 +  def later(body: => Unit)
    2.47 +  {
    2.48 +    if (SwingUtilities.isEventDispatchThread()) body
    2.49 +    else SwingUtilities.invokeLater(new Runnable { def run = body })
    2.50 +  }
    2.51 +
    2.52 +
    2.53 +  /* delayed events */
    2.54 +
    2.55 +  def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay =
    2.56 +    Simple_Thread.delay_first(delay) { later { event } }
    2.57 +
    2.58 +  def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay =
    2.59 +    Simple_Thread.delay_last(delay) { later { event } }
    2.60 +}
     3.1 --- a/src/Pure/GUI/swing_thread.scala	Wed Jul 23 11:08:24 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,57 +0,0 @@
     3.4 -/*  Title:      Pure/GUI/swing_thread.scala
     3.5 -    Module:     PIDE-GUI
     3.6 -    Author:     Makarius
     3.7 -
     3.8 -Evaluation within the AWT/Swing thread.
     3.9 -*/
    3.10 -
    3.11 -package isabelle
    3.12 -
    3.13 -
    3.14 -import javax.swing.SwingUtilities
    3.15 -
    3.16 -
    3.17 -object Swing_Thread
    3.18 -{
    3.19 -  /* context check */
    3.20 -
    3.21 -  def assert[A](body: => A) =
    3.22 -  {
    3.23 -    Predef.assert(SwingUtilities.isEventDispatchThread())
    3.24 -    body
    3.25 -  }
    3.26 -
    3.27 -  def require[A](body: => A) =
    3.28 -  {
    3.29 -    Predef.require(SwingUtilities.isEventDispatchThread())
    3.30 -    body
    3.31 -  }
    3.32 -
    3.33 -
    3.34 -  /* event dispatch queue */
    3.35 -
    3.36 -  def now[A](body: => A): A =
    3.37 -  {
    3.38 -    if (SwingUtilities.isEventDispatchThread()) body
    3.39 -    else {
    3.40 -      lazy val result = { assert { Exn.capture(body) } }
    3.41 -      SwingUtilities.invokeAndWait(new Runnable { def run = result })
    3.42 -      Exn.release(result)
    3.43 -    }
    3.44 -  }
    3.45 -
    3.46 -  def later(body: => Unit)
    3.47 -  {
    3.48 -    if (SwingUtilities.isEventDispatchThread()) body
    3.49 -    else SwingUtilities.invokeLater(new Runnable { def run = body })
    3.50 -  }
    3.51 -
    3.52 -
    3.53 -  /* delayed events */
    3.54 -
    3.55 -  def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay =
    3.56 -    Simple_Thread.delay_first(delay) { later { event } }
    3.57 -
    3.58 -  def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay =
    3.59 -    Simple_Thread.delay_last(delay) { later { event } }
    3.60 -}
     4.1 --- a/src/Pure/GUI/system_dialog.scala	Wed Jul 23 11:08:24 2014 +0200
     4.2 +++ b/src/Pure/GUI/system_dialog.scala	Wed Jul 23 11:19:24 2014 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4  
     4.5  class System_Dialog extends Build.Progress
     4.6  {
     4.7 -  /* GUI state -- owned by Swing thread */
     4.8 +  /* component state -- owned by GUI thread */
     4.9  
    4.10    private var _title = "Isabelle"
    4.11    private var _window: Option[Window] = None
    4.12 @@ -26,7 +26,7 @@
    4.13  
    4.14    private def check_window(): Window =
    4.15    {
    4.16 -    Swing_Thread.require {}
    4.17 +    GUI_Thread.require {}
    4.18  
    4.19      _window match {
    4.20        case Some(window) => window
    4.21 @@ -48,7 +48,7 @@
    4.22  
    4.23    private def conclude()
    4.24    {
    4.25 -    Swing_Thread.require {}
    4.26 +    GUI_Thread.require {}
    4.27      require(_return_code.isDefined)
    4.28  
    4.29      _window match {
    4.30 @@ -142,7 +142,7 @@
    4.31      /* exit */
    4.32  
    4.33      val delay_exit =
    4.34 -      Swing_Thread.delay_first(Time.seconds(1.0))
    4.35 +      GUI_Thread.delay_first(Time.seconds(1.0))
    4.36        {
    4.37          if (can_auto_close) conclude()
    4.38          else {
    4.39 @@ -160,13 +160,13 @@
    4.40    /* progress operations */
    4.41  
    4.42    def title(txt: String): Unit =
    4.43 -    Swing_Thread.later {
    4.44 +    GUI_Thread.later {
    4.45        _title = txt
    4.46        _window.foreach(window => window.title = txt)
    4.47      }
    4.48  
    4.49    def return_code(rc: Int): Unit =
    4.50 -    Swing_Thread.later {
    4.51 +    GUI_Thread.later {
    4.52        _return_code = Some(rc)
    4.53        _window match {
    4.54          case None => conclude()
    4.55 @@ -175,7 +175,7 @@
    4.56      }
    4.57  
    4.58    override def echo(txt: String): Unit =
    4.59 -    Swing_Thread.later {
    4.60 +    GUI_Thread.later {
    4.61        val window = check_window()
    4.62        window.text.append(txt + "\n")
    4.63        val vertical = window.scroll_text.peer.getVerticalScrollBar
     5.1 --- a/src/Pure/PIDE/query_operation.scala	Wed Jul 23 11:08:24 2014 +0200
     5.2 +++ b/src/Pure/PIDE/query_operation.scala	Wed Jul 23 11:19:24 2014 +0200
     5.3 @@ -28,7 +28,7 @@
     5.4    private val instance = Document_ID.make().toString
     5.5  
     5.6  
     5.7 -  /* implicit state -- owned by Swing thread */
     5.8 +  /* implicit state -- owned by GUI thread */
     5.9  
    5.10    @volatile private var current_location: Option[Command] = None
    5.11    @volatile private var current_query: List[String] = Nil
    5.12 @@ -62,7 +62,7 @@
    5.13  
    5.14    private def content_update()
    5.15    {
    5.16 -    Swing_Thread.require {}
    5.17 +    GUI_Thread.require {}
    5.18  
    5.19  
    5.20      /* snapshot */
    5.21 @@ -167,11 +167,11 @@
    5.22    /* query operations */
    5.23  
    5.24    def cancel_query(): Unit =
    5.25 -    Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
    5.26 +    GUI_Thread.require { editor.session.cancel_exec(current_exec_id) }
    5.27  
    5.28    def apply_query(query: List[String])
    5.29    {
    5.30 -    Swing_Thread.require {}
    5.31 +    GUI_Thread.require {}
    5.32  
    5.33      editor.current_node_snapshot(editor_context) match {
    5.34        case Some(snapshot) =>
    5.35 @@ -196,7 +196,7 @@
    5.36  
    5.37    def locate_query()
    5.38    {
    5.39 -    Swing_Thread.require {}
    5.40 +    GUI_Thread.require {}
    5.41  
    5.42      for {
    5.43        command <- current_location
    5.44 @@ -216,7 +216,7 @@
    5.45            if current_update_pending ||
    5.46              (current_status != Query_Operation.Status.FINISHED &&
    5.47                changed.commands.contains(command)) =>
    5.48 -            Swing_Thread.later { content_update() }
    5.49 +            GUI_Thread.later { content_update() }
    5.50            case _ =>
    5.51          }
    5.52      }
     6.1 --- a/src/Pure/Tools/ml_statistics.scala	Wed Jul 23 11:08:24 2014 +0200
     6.2 +++ b/src/Pure/Tools/ml_statistics.scala	Wed Jul 23 11:19:24 2014 +0200
     6.3 @@ -131,7 +131,7 @@
     6.4  
     6.5    def show_standard_frames(): Unit =
     6.6      ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
     6.7 -      Swing_Thread.later {
     6.8 +      GUI_Thread.later {
     6.9          new Frame {
    6.10            iconImage = GUI.isabelle_image()
    6.11            title = name
     7.1 --- a/src/Pure/Tools/task_statistics.scala	Wed Jul 23 11:08:24 2014 +0200
     7.2 +++ b/src/Pure/Tools/task_statistics.scala	Wed Jul 23 11:19:24 2014 +0200
     7.3 @@ -51,7 +51,7 @@
     7.4    }
     7.5  
     7.6    def show_frame(bins: Int = 100): Unit =
     7.7 -    Swing_Thread.later {
     7.8 +    GUI_Thread.later {
     7.9        new Frame {
    7.10          iconImage = GUI.isabelle_image()
    7.11          title = name
     8.1 --- a/src/Pure/build-jars	Wed Jul 23 11:08:24 2014 +0200
     8.2 +++ b/src/Pure/build-jars	Wed Jul 23 11:19:24 2014 +0200
     8.3 @@ -42,10 +42,10 @@
     8.4    General/xz_file.scala
     8.5    GUI/color_value.scala
     8.6    GUI/gui.scala
     8.7 +  GUI/gui_thread.scala
     8.8    GUI/html5_panel.scala
     8.9    GUI/jfx_thread.scala
    8.10    GUI/popup.scala
    8.11 -  GUI/swing_thread.scala
    8.12    GUI/system_dialog.scala
    8.13    GUI/wrap_panel.scala
    8.14    Isar/keyword.scala
     9.1 --- a/src/Tools/Graphview/src/mutator_event.scala	Wed Jul 23 11:08:24 2014 +0200
     9.2 +++ b/src/Tools/Graphview/src/mutator_event.scala	Wed Jul 23 11:19:24 2014 +0200
     9.3 @@ -28,8 +28,8 @@
     9.4    {
     9.5      private val receivers = new mutable.ListBuffer[Receiver]
     9.6  
     9.7 -    def += (r: Receiver) { Swing_Thread.require {}; receivers += r }
     9.8 -    def -= (r: Receiver) { Swing_Thread.require {}; receivers -= r }
     9.9 -    def event(x: Message) { Swing_Thread.require {}; receivers.foreach(r => r(x)) }
    9.10 +    def += (r: Receiver) { GUI_Thread.require {}; receivers += r }
    9.11 +    def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r }
    9.12 +    def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) }
    9.13    }
    9.14  }
    9.15 \ No newline at end of file
    10.1 --- a/src/Tools/jEdit/src/active.scala	Wed Jul 23 11:08:24 2014 +0200
    10.2 +++ b/src/Tools/jEdit/src/active.scala	Wed Jul 23 11:19:24 2014 +0200
    10.3 @@ -16,7 +16,7 @@
    10.4  {
    10.5    def action(view: View, text: String, elem: XML.Elem)
    10.6    {
    10.7 -    Swing_Thread.require {}
    10.8 +    GUI_Thread.require {}
    10.9  
   10.10      Document_View(view.getTextArea) match {
   10.11        case Some(doc_view) =>
   10.12 @@ -45,11 +45,11 @@
   10.13                        isabelle.graphview.Model.decode_graph(body)
   10.14                          .transitive_reduction_acyclic
   10.15                      }
   10.16 -                  Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
   10.17 +                  GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
   10.18                  }
   10.19  
   10.20                case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
   10.21 -                Swing_Thread.later {
   10.22 +                GUI_Thread.later {
   10.23                    view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
   10.24                  }
   10.25  
    11.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jul 23 11:08:24 2014 +0200
    11.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jul 23 11:19:24 2014 +0200
    11.3 @@ -52,7 +52,7 @@
    11.4  
    11.5      def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
    11.6      {
    11.7 -      Swing_Thread.require {}
    11.8 +      GUI_Thread.require {}
    11.9        text_area.getClientProperty(key) match {
   11.10          case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
   11.11          case _ => None
   11.12 @@ -78,7 +78,7 @@
   11.13  
   11.14      def exit(text_area: JEditTextArea)
   11.15      {
   11.16 -      Swing_Thread.require {}
   11.17 +      GUI_Thread.require {}
   11.18        apply(text_area) match {
   11.19          case None =>
   11.20          case Some(text_area_completion) =>
   11.21 @@ -98,7 +98,7 @@
   11.22  
   11.23      def dismissed(text_area: TextArea): Boolean =
   11.24      {
   11.25 -      Swing_Thread.require {}
   11.26 +      GUI_Thread.require {}
   11.27        apply(text_area) match {
   11.28          case Some(text_area_completion) => text_area_completion.dismissed()
   11.29          case None => false
   11.30 @@ -108,7 +108,7 @@
   11.31  
   11.32    class Text_Area private(text_area: JEditTextArea)
   11.33    {
   11.34 -    // owned by Swing thread
   11.35 +    // owned by GUI thread
   11.36      private var completion_popup: Option[Completion_Popup] = None
   11.37  
   11.38      def active_range: Option[Text.Range] =
   11.39 @@ -255,7 +255,7 @@
   11.40  
   11.41      private def insert(item: Completion.Item)
   11.42      {
   11.43 -      Swing_Thread.require {}
   11.44 +      GUI_Thread.require {}
   11.45  
   11.46        val buffer = text_area.getBuffer
   11.47        val range = item.range
   11.48 @@ -425,7 +425,7 @@
   11.49  
   11.50      def input(evt: KeyEvent)
   11.51      {
   11.52 -      Swing_Thread.require {}
   11.53 +      GUI_Thread.require {}
   11.54  
   11.55        if (PIDE.options.bool("jedit_completion")) {
   11.56          if (!evt.isConsumed) {
   11.57 @@ -449,7 +449,7 @@
   11.58      }
   11.59  
   11.60      private val input_delay =
   11.61 -      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   11.62 +      GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   11.63          action()
   11.64        }
   11.65  
   11.66 @@ -458,7 +458,7 @@
   11.67  
   11.68      def dismissed(): Boolean =
   11.69      {
   11.70 -      Swing_Thread.require {}
   11.71 +      GUI_Thread.require {}
   11.72  
   11.73        completion_popup match {
   11.74          case Some(completion) =>
   11.75 @@ -504,7 +504,7 @@
   11.76      // see https://forums.oracle.com/thread/1361677
   11.77      if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
   11.78  
   11.79 -    // owned by Swing thread
   11.80 +    // owned by GUI thread
   11.81      private var completion_popup: Option[Completion_Popup] = None
   11.82  
   11.83  
   11.84 @@ -527,7 +527,7 @@
   11.85  
   11.86      private def insert(item: Completion.Item)
   11.87      {
   11.88 -      Swing_Thread.require {}
   11.89 +      GUI_Thread.require {}
   11.90  
   11.91        val range = item.range
   11.92        if (text_field.isEditable) {
   11.93 @@ -606,7 +606,7 @@
   11.94      }
   11.95  
   11.96      private val process_delay =
   11.97 -      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   11.98 +      GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   11.99          action()
  11.100        }
  11.101  
  11.102 @@ -642,7 +642,7 @@
  11.103  {
  11.104    completion =>
  11.105  
  11.106 -  Swing_Thread.require {}
  11.107 +  GUI_Thread.require {}
  11.108  
  11.109    require(!items.isEmpty)
  11.110    val multi = items.length > 1
    12.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 11:08:24 2014 +0200
    12.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 11:19:24 2014 +0200
    12.3 @@ -25,7 +25,7 @@
    12.4  
    12.5    def apply(buffer: Buffer): Option[Document_Model] =
    12.6    {
    12.7 -    Swing_Thread.require {}
    12.8 +    GUI_Thread.require {}
    12.9      buffer.getProperty(key) match {
   12.10        case model: Document_Model => Some(model)
   12.11        case _ => None
   12.12 @@ -34,7 +34,7 @@
   12.13  
   12.14    def exit(buffer: Buffer)
   12.15    {
   12.16 -    Swing_Thread.require {}
   12.17 +    GUI_Thread.require {}
   12.18      apply(buffer) match {
   12.19        case None =>
   12.20        case Some(model) =>
   12.21 @@ -46,7 +46,7 @@
   12.22  
   12.23    def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
   12.24    {
   12.25 -    Swing_Thread.require {}
   12.26 +    GUI_Thread.require {}
   12.27      apply(buffer).map(_.deactivate)
   12.28      val model = new Document_Model(session, buffer, node_name)
   12.29      buffer.setProperty(key, model)
   12.30 @@ -65,7 +65,7 @@
   12.31  
   12.32    def node_header(): Document.Node.Header =
   12.33    {
   12.34 -    Swing_Thread.require {}
   12.35 +    GUI_Thread.require {}
   12.36  
   12.37      if (is_theory) {
   12.38        JEdit_Lib.buffer_lock(buffer) {
   12.39 @@ -83,12 +83,12 @@
   12.40  
   12.41    /* perspective */
   12.42  
   12.43 -  // owned by Swing thread
   12.44 +  // owned by GUI thread
   12.45    private var _node_required = false
   12.46    def node_required: Boolean = _node_required
   12.47    def node_required_=(b: Boolean)
   12.48    {
   12.49 -    Swing_Thread.require {}
   12.50 +    GUI_Thread.require {}
   12.51      if (_node_required != b && is_theory) {
   12.52        _node_required = b
   12.53        PIDE.options_changed()
   12.54 @@ -98,7 +98,7 @@
   12.55  
   12.56    def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
   12.57    {
   12.58 -    Swing_Thread.require {}
   12.59 +    GUI_Thread.require {}
   12.60  
   12.61      if (Isabelle.continuous_checking && is_theory) {
   12.62        val snapshot = this.snapshot()
   12.63 @@ -135,12 +135,12 @@
   12.64  
   12.65    /* blob */
   12.66  
   12.67 -  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by Swing thread
   12.68 +  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by GUI thread
   12.69  
   12.70 -  private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
   12.71 +  private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
   12.72  
   12.73    def get_blob(): Option[Document.Blob] =
   12.74 -    Swing_Thread.require {
   12.75 +    GUI_Thread.require {
   12.76        if (is_theory) None
   12.77        else {
   12.78          val (bytes, chunk) =
   12.79 @@ -184,7 +184,7 @@
   12.80  
   12.81    /* pending edits */
   12.82  
   12.83 -  private object pending_edits  // owned by Swing thread
   12.84 +  private object pending_edits  // owned by GUI thread
   12.85    {
   12.86      private var pending_clear = false
   12.87      private val pending = new mutable.ListBuffer[Text.Edit]
   12.88 @@ -221,10 +221,10 @@
   12.89    }
   12.90  
   12.91    def snapshot(): Document.Snapshot =
   12.92 -    Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
   12.93 +    GUI_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
   12.94  
   12.95    def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   12.96 -    Swing_Thread.require { pending_edits.flushed_edits(doc_blobs) }
   12.97 +    GUI_Thread.require { pending_edits.flushed_edits(doc_blobs) }
   12.98  
   12.99  
  12.100    /* buffer listener */
    13.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Jul 23 11:08:24 2014 +0200
    13.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jul 23 11:19:24 2014 +0200
    13.3 @@ -27,7 +27,7 @@
    13.4  
    13.5    def apply(text_area: TextArea): Option[Document_View] =
    13.6    {
    13.7 -    Swing_Thread.require {}
    13.8 +    GUI_Thread.require {}
    13.9      text_area.getClientProperty(key) match {
   13.10        case doc_view: Document_View => Some(doc_view)
   13.11        case _ => None
   13.12 @@ -36,7 +36,7 @@
   13.13  
   13.14    def exit(text_area: JEditTextArea)
   13.15    {
   13.16 -    Swing_Thread.require {}
   13.17 +    GUI_Thread.require {}
   13.18      apply(text_area) match {
   13.19        case None =>
   13.20        case Some(doc_view) =>
   13.21 @@ -71,7 +71,7 @@
   13.22  
   13.23    def perspective(snapshot: Document.Snapshot): Text.Perspective =
   13.24    {
   13.25 -    Swing_Thread.require {}
   13.26 +    GUI_Thread.require {}
   13.27  
   13.28      val active_command =
   13.29      {
   13.30 @@ -125,7 +125,7 @@
   13.31        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   13.32      {
   13.33        rich_text_area.robust_body(()) {
   13.34 -        Swing_Thread.assert {}
   13.35 +        GUI_Thread.assert {}
   13.36  
   13.37          val gutter = text_area.getGutter
   13.38          val width = GutterOptionPane.getSelectionAreaWidth
   13.39 @@ -173,7 +173,7 @@
   13.40    /* caret handling */
   13.41  
   13.42    private val delay_caret_update =
   13.43 -    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   13.44 +    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   13.45        session.caret_focus.post(Session.Caret_Focus)
   13.46      }
   13.47  
   13.48 @@ -187,7 +187,7 @@
   13.49    private object overview extends Text_Overview(this)
   13.50    {
   13.51      val delay_repaint =
   13.52 -      Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
   13.53 +      GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
   13.54    }
   13.55  
   13.56  
   13.57 @@ -200,7 +200,7 @@
   13.58  
   13.59        case changed: Session.Commands_Changed =>
   13.60          val buffer = model.buffer
   13.61 -        Swing_Thread.later {
   13.62 +        GUI_Thread.later {
   13.63            JEdit_Lib.buffer_lock(buffer) {
   13.64              if (model.buffer == text_area.getBuffer) {
   13.65                val snapshot = model.snapshot()
    14.1 --- a/src/Tools/jEdit/src/font_info.scala	Wed Jul 23 11:08:24 2014 +0200
    14.2 +++ b/src/Tools/jEdit/src/font_info.scala	Wed Jul 23 11:19:24 2014 +0200
    14.3 @@ -42,7 +42,7 @@
    14.4    {
    14.5      private def change_size(change: Float => Float)
    14.6      {
    14.7 -      Swing_Thread.require {}
    14.8 +      GUI_Thread.require {}
    14.9  
   14.10        val size0 = main_size()
   14.11        val size = restrict_size(change(size0)).round
   14.12 @@ -54,9 +54,9 @@
   14.13        }
   14.14      }
   14.15  
   14.16 -    // owned by Swing thread
   14.17 +    // owned by GUI thread
   14.18      private var steps = 0
   14.19 -    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
   14.20 +    private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
   14.21      {
   14.22        change_size(size =>
   14.23          {
    15.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    15.3 @@ -20,7 +20,7 @@
    15.4  
    15.5  object Graphview_Dockable
    15.6  {
    15.7 -  /* implicit arguments -- owned by Swing thread */
    15.8 +  /* implicit arguments -- owned by GUI thread */
    15.9  
   15.10    private var implicit_snapshot = Document.Snapshot.init
   15.11  
   15.12 @@ -29,7 +29,7 @@
   15.13  
   15.14    private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
   15.15    {
   15.16 -    Swing_Thread.require {}
   15.17 +    GUI_Thread.require {}
   15.18  
   15.19      implicit_snapshot = snapshot
   15.20      implicit_graph = graph
    16.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    16.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    16.3 @@ -20,7 +20,7 @@
    16.4  
    16.5  object Info_Dockable
    16.6  {
    16.7 -  /* implicit arguments -- owned by Swing thread */
    16.8 +  /* implicit arguments -- owned by GUI thread */
    16.9  
   16.10    private var implicit_snapshot = Document.Snapshot.init
   16.11    private var implicit_results = Command.Results.empty
   16.12 @@ -28,7 +28,7 @@
   16.13  
   16.14    private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
   16.15    {
   16.16 -    Swing_Thread.require {}
   16.17 +    GUI_Thread.require {}
   16.18  
   16.19      implicit_snapshot = snapshot
   16.20      implicit_results = results
   16.21 @@ -48,7 +48,7 @@
   16.22  
   16.23  class Info_Dockable(view: View, position: String) extends Dockable(view, position)
   16.24  {
   16.25 -  /* component state -- owned by Swing thread */
   16.26 +  /* component state -- owned by GUI thread */
   16.27  
   16.28    private val snapshot = Info_Dockable.implicit_snapshot
   16.29    private val results = Info_Dockable.implicit_results
   16.30 @@ -72,7 +72,7 @@
   16.31  
   16.32    private def handle_resize()
   16.33    {
   16.34 -    Swing_Thread.require {}
   16.35 +    GUI_Thread.require {}
   16.36  
   16.37      pretty_text_area.resize(
   16.38        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   16.39 @@ -82,7 +82,7 @@
   16.40    /* resize */
   16.41  
   16.42    private val delay_resize =
   16.43 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   16.44 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   16.45  
   16.46    addComponentListener(new ComponentAdapter {
   16.47      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   16.48 @@ -97,7 +97,7 @@
   16.49  
   16.50    private val main =
   16.51      Session.Consumer[Session.Global_Options](getClass.getName) {
   16.52 -      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
   16.53 +      case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
   16.54      }
   16.55  
   16.56    override def init()
    17.1 --- a/src/Tools/jEdit/src/isabelle.scala	Wed Jul 23 11:08:24 2014 +0200
    17.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Wed Jul 23 11:19:24 2014 +0200
    17.3 @@ -153,7 +153,7 @@
    17.4  
    17.5    def continuous_checking_=(b: Boolean)
    17.6    {
    17.7 -    Swing_Thread.require {}
    17.8 +    GUI_Thread.require {}
    17.9  
   17.10      if (continuous_checking != b) {
   17.11        PIDE.options.bool(CONTINUOUS_CHECKING) = b
   17.12 @@ -179,7 +179,7 @@
   17.13  
   17.14    private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
   17.15    {
   17.16 -    Swing_Thread.require {}
   17.17 +    GUI_Thread.require {}
   17.18      PIDE.document_model(view.getBuffer) match {
   17.19        case Some(model) =>
   17.20          model.node_required = (if (toggle) !model.node_required else set)
    18.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Wed Jul 23 11:08:24 2014 +0200
    18.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Wed Jul 23 11:19:24 2014 +0200
    18.3 @@ -29,7 +29,7 @@
    18.4  
    18.5    def logic_selector(autosave: Boolean): Option_Component =
    18.6    {
    18.7 -    Swing_Thread.require {}
    18.8 +    GUI_Thread.require {}
    18.9  
   18.10      val entries =
   18.11        new Logic_Entry("", "default (" + jedit_logic() + ")") ::
    19.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Jul 23 11:08:24 2014 +0200
    19.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Jul 23 11:19:24 2014 +0200
    19.3 @@ -149,7 +149,7 @@
    19.4    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
    19.5    {
    19.6      val opt_snapshot =
    19.7 -      Swing_Thread.now {
    19.8 +      GUI_Thread.now {
    19.9          Document_Model(buffer) match {
   19.10            case Some(model) if model.is_theory => Some(model.snapshot)
   19.11            case _ => None
    20.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:08:24 2014 +0200
    20.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:19:24 2014 +0200
    20.3 @@ -22,15 +22,15 @@
    20.4  
    20.5    override def session: Session = PIDE.session
    20.6  
    20.7 -  // owned by Swing thread
    20.8 +  // owned by GUI thread
    20.9    private var removed_nodes = Set.empty[Document.Node.Name]
   20.10  
   20.11    def remove_node(name: Document.Node.Name): Unit =
   20.12 -    Swing_Thread.require { removed_nodes += name }
   20.13 +    GUI_Thread.require { removed_nodes += name }
   20.14  
   20.15    override def flush()
   20.16    {
   20.17 -    Swing_Thread.require {}
   20.18 +    GUI_Thread.require {}
   20.19  
   20.20      val doc_blobs = PIDE.document_blobs()
   20.21      val models = PIDE.document_models()
   20.22 @@ -45,7 +45,7 @@
   20.23    }
   20.24  
   20.25    private val delay_flush =
   20.26 -    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
   20.27 +    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
   20.28  
   20.29    def invoke(): Unit = delay_flush.invoke()
   20.30  
   20.31 @@ -53,17 +53,17 @@
   20.32    /* current situation */
   20.33  
   20.34    override def current_context: View =
   20.35 -    Swing_Thread.require { jEdit.getActiveView() }
   20.36 +    GUI_Thread.require { jEdit.getActiveView() }
   20.37  
   20.38    override def current_node(view: View): Option[Document.Node.Name] =
   20.39 -    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
   20.40 +    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
   20.41  
   20.42    override def current_node_snapshot(view: View): Option[Document.Snapshot] =
   20.43 -    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
   20.44 +    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
   20.45  
   20.46    override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
   20.47    {
   20.48 -    Swing_Thread.require {}
   20.49 +    GUI_Thread.require {}
   20.50  
   20.51      JEdit_Lib.jedit_buffer(name) match {
   20.52        case Some(buffer) =>
   20.53 @@ -77,7 +77,7 @@
   20.54  
   20.55    override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
   20.56    {
   20.57 -    Swing_Thread.require {}
   20.58 +    GUI_Thread.require {}
   20.59  
   20.60      val text_area = view.getTextArea
   20.61      val buffer = view.getBuffer
   20.62 @@ -138,7 +138,7 @@
   20.63  
   20.64    def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   20.65    {
   20.66 -    Swing_Thread.require {}
   20.67 +    GUI_Thread.require {}
   20.68  
   20.69      push_position(view)
   20.70  
    21.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Jul 23 11:08:24 2014 +0200
    21.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Jul 23 11:19:24 2014 +0200
    21.3 @@ -75,7 +75,7 @@
    21.4  
    21.5    def window_geometry(outer: Container, inner: Component): Window_Geometry =
    21.6    {
    21.7 -    Swing_Thread.require {}
    21.8 +    GUI_Thread.require {}
    21.9  
   21.10      val old_content = dummy_window.getContentPane
   21.11  
    22.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Wed Jul 23 11:08:24 2014 +0200
    22.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Jul 23 11:19:24 2014 +0200
    22.3 @@ -36,7 +36,7 @@
    22.4  
    22.5    def make_color_component(opt: Options.Opt): Option_Component =
    22.6    {
    22.7 -    Swing_Thread.require {}
    22.8 +    GUI_Thread.require {}
    22.9  
   22.10      val opt_name = opt.name
   22.11      val opt_title = opt.title("jedit")
   22.12 @@ -55,7 +55,7 @@
   22.13  
   22.14    def make_component(opt: Options.Opt): Option_Component =
   22.15    {
   22.16 -    Swing_Thread.require {}
   22.17 +    GUI_Thread.require {}
   22.18  
   22.19      val opt_name = opt.name
   22.20      val opt_title = opt.title("jedit")
    23.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Jul 23 11:08:24 2014 +0200
    23.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Jul 23 11:19:24 2014 +0200
    23.3 @@ -62,7 +62,7 @@
    23.4  
    23.5    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    23.6    {
    23.7 -    Swing_Thread.now {
    23.8 +    GUI_Thread.now {
    23.9        JEdit_Lib.jedit_buffer(name) match {
   23.10          case Some(buffer) =>
   23.11            JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
   23.12 @@ -113,7 +113,7 @@
   23.13  
   23.14    override def commit(change: Session.Change)
   23.15    {
   23.16 -    if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
   23.17 +    if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() }
   23.18    }
   23.19  }
   23.20  
    24.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    24.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    24.3 @@ -22,13 +22,13 @@
    24.4    private val rev_stats = Synchronized(Nil: List[Properties.T])
    24.5  
    24.6  
    24.7 -  /* chart data -- owned by Swing thread */
    24.8 +  /* chart data -- owned by GUI thread */
    24.9  
   24.10    private val chart = ML_Statistics.empty.chart(null, Nil)
   24.11    private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
   24.12  
   24.13    private val delay_update =
   24.14 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
   24.15 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
   24.16        ML_Statistics("", rev_stats.value.reverse)
   24.17          .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
   24.18      }
    25.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    25.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    25.3 @@ -20,7 +20,7 @@
    25.4  
    25.5  class Output_Dockable(view: View, position: String) extends Dockable(view, position)
    25.6  {
    25.7 -  /* component state -- owned by Swing thread */
    25.8 +  /* component state -- owned by GUI thread */
    25.9  
   25.10    private var do_update = true
   25.11    private var current_snapshot = Document.Snapshot.init
   25.12 @@ -41,7 +41,7 @@
   25.13  
   25.14    private def handle_resize()
   25.15    {
   25.16 -    Swing_Thread.require {}
   25.17 +    GUI_Thread.require {}
   25.18  
   25.19      pretty_text_area.resize(
   25.20        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   25.21 @@ -49,7 +49,7 @@
   25.22  
   25.23    private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
   25.24    {
   25.25 -    Swing_Thread.require {}
   25.26 +    GUI_Thread.require {}
   25.27  
   25.28      val (new_snapshot, new_command, new_results) =
   25.29        PIDE.editor.current_node_snapshot(view) match {
   25.30 @@ -88,14 +88,14 @@
   25.31    private val main =
   25.32      Session.Consumer[Any](getClass.getName) {
   25.33        case _: Session.Global_Options =>
   25.34 -        Swing_Thread.later { handle_resize() }
   25.35 +        GUI_Thread.later { handle_resize() }
   25.36  
   25.37        case changed: Session.Commands_Changed =>
   25.38          val restriction = if (changed.assignment) None else Some(changed.commands)
   25.39 -        Swing_Thread.later { handle_update(do_update, restriction) }
   25.40 +        GUI_Thread.later { handle_update(do_update, restriction) }
   25.41  
   25.42        case Session.Caret_Focus =>
   25.43 -        Swing_Thread.later { handle_update(do_update, None) }
   25.44 +        GUI_Thread.later { handle_update(do_update, None) }
   25.45      }
   25.46  
   25.47    override def init()
   25.48 @@ -118,7 +118,7 @@
   25.49    /* resize */
   25.50  
   25.51    private val delay_resize =
   25.52 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   25.53 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   25.54  
   25.55    addComponentListener(new ComponentAdapter {
   25.56      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    26.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Jul 23 11:08:24 2014 +0200
    26.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jul 23 11:19:24 2014 +0200
    26.3 @@ -90,7 +90,7 @@
    26.4  
    26.5    def exit_models(buffers: List[Buffer])
    26.6    {
    26.7 -    Swing_Thread.now {
    26.8 +    GUI_Thread.now {
    26.9        PIDE.editor.flush()
   26.10        buffers.foreach(buffer =>
   26.11          JEdit_Lib.buffer_lock(buffer) {
   26.12 @@ -102,7 +102,7 @@
   26.13  
   26.14    def init_models()
   26.15    {
   26.16 -    Swing_Thread.now {
   26.17 +    GUI_Thread.now {
   26.18        PIDE.editor.flush()
   26.19  
   26.20        for {
   26.21 @@ -128,7 +128,7 @@
   26.22    }
   26.23  
   26.24    def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
   26.25 -    Swing_Thread.now {
   26.26 +    GUI_Thread.now {
   26.27        JEdit_Lib.buffer_lock(buffer) {
   26.28          document_model(buffer) match {
   26.29            case Some(model) => Document_View.init(model, text_area)
   26.30 @@ -138,7 +138,7 @@
   26.31      }
   26.32  
   26.33    def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
   26.34 -    Swing_Thread.now {
   26.35 +    GUI_Thread.now {
   26.36        JEdit_Lib.buffer_lock(buffer) {
   26.37          Document_View.exit(text_area)
   26.38        }
   26.39 @@ -147,7 +147,7 @@
   26.40  
   26.41    /* current document content */
   26.42  
   26.43 -  def snapshot(view: View): Document.Snapshot = Swing_Thread.now
   26.44 +  def snapshot(view: View): Document.Snapshot = GUI_Thread.now
   26.45    {
   26.46      val buffer = view.getBuffer
   26.47      document_model(buffer) match {
   26.48 @@ -156,7 +156,7 @@
   26.49      }
   26.50    }
   26.51  
   26.52 -  def rendering(view: View): Rendering = Swing_Thread.now
   26.53 +  def rendering(view: View): Rendering = GUI_Thread.now
   26.54    {
   26.55      val text_area = view.getTextArea
   26.56      document_view(text_area) match {
   26.57 @@ -186,7 +186,7 @@
   26.58    /* theory files */
   26.59  
   26.60    private lazy val delay_init =
   26.61 -    Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   26.62 +    GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   26.63      {
   26.64        PIDE.init_models()
   26.65      }
   26.66 @@ -196,7 +196,7 @@
   26.67      delay_load_active.guarded_access(a => Some((!a, true)))
   26.68  
   26.69    private lazy val delay_load =
   26.70 -    Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   26.71 +    GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   26.72      {
   26.73        if (Isabelle.continuous_checking && delay_load_activated()) {
   26.74          try {
   26.75 @@ -215,7 +215,7 @@
   26.76                } yield (model.node_name, Position.none)
   26.77  
   26.78              val thy_info = new Thy_Info(PIDE.resources)
   26.79 -            // FIXME avoid I/O in Swing thread!?!
   26.80 +            // FIXME avoid I/O on GUI thread!?!
   26.81              val files = thy_info.dependencies("", thys).deps.map(_.name.node).
   26.82                filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
   26.83  
   26.84 @@ -255,7 +255,7 @@
   26.85    private val session_phase =
   26.86      Session.Consumer[Session.Phase](getClass.getName) {
   26.87        case Session.Inactive | Session.Failed =>
   26.88 -        Swing_Thread.later {
   26.89 +        GUI_Thread.later {
   26.90            GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
   26.91              "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
   26.92          }
   26.93 @@ -277,7 +277,7 @@
   26.94  
   26.95    override def handleMessage(message: EBMessage)
   26.96    {
   26.97 -    Swing_Thread.assert {}
   26.98 +    GUI_Thread.assert {}
   26.99  
  26.100      if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
  26.101        message match {
    27.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jul 23 11:08:24 2014 +0200
    27.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jul 23 11:19:24 2014 +0200
    27.3 @@ -68,7 +68,7 @@
    27.4  {
    27.5    text_area =>
    27.6  
    27.7 -  Swing_Thread.require {}
    27.8 +  GUI_Thread.require {}
    27.9  
   27.10    private var current_font_info: Font_Info = Font_Info.main()
   27.11    private var current_body: XML.Body = Nil
   27.12 @@ -83,13 +83,13 @@
   27.13        get_search_pattern _, caret_visible = false, enable_hovering = true)
   27.14  
   27.15    private var current_search_pattern: Option[Regex] = None
   27.16 -  def get_search_pattern(): Option[Regex] = Swing_Thread.require { current_search_pattern }
   27.17 +  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
   27.18  
   27.19    def get_background(): Option[Color] = None
   27.20  
   27.21    def refresh()
   27.22    {
   27.23 -    Swing_Thread.require {}
   27.24 +    GUI_Thread.require {}
   27.25  
   27.26      val font = current_font_info.font
   27.27      getPainter.setFont(font)
   27.28 @@ -137,7 +137,7 @@
   27.29              catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
   27.30            Exn.Interrupt.expose()
   27.31  
   27.32 -          Swing_Thread.later {
   27.33 +          GUI_Thread.later {
   27.34              current_rendering = rendering
   27.35              JEdit_Lib.buffer_edit(getBuffer) {
   27.36                rich_text_area.active_reset()
   27.37 @@ -154,7 +154,7 @@
   27.38  
   27.39    def resize(font_info: Font_Info)
   27.40    {
   27.41 -    Swing_Thread.require {}
   27.42 +    GUI_Thread.require {}
   27.43  
   27.44      current_font_info = font_info
   27.45      refresh()
   27.46 @@ -162,7 +162,7 @@
   27.47  
   27.48    def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
   27.49    {
   27.50 -    Swing_Thread.require {}
   27.51 +    GUI_Thread.require {}
   27.52      require(!base_snapshot.is_outdated)
   27.53  
   27.54      current_base_snapshot = base_snapshot
   27.55 @@ -173,7 +173,7 @@
   27.56  
   27.57    def detach
   27.58    {
   27.59 -    Swing_Thread.require {}
   27.60 +    GUI_Thread.require {}
   27.61      Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
   27.62    }
   27.63  
   27.64 @@ -191,7 +191,7 @@
   27.65      Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
   27.66        {
   27.67          private val input_delay =
   27.68 -          Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   27.69 +          GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   27.70              search_action(this)
   27.71            }
   27.72          getDocument.addDocumentListener(new DocumentListener {
    28.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jul 23 11:08:24 2014 +0200
    28.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jul 23 11:19:24 2014 +0200
    28.3 @@ -25,19 +25,19 @@
    28.4  {
    28.5    /* tooltip hierarchy */
    28.6  
    28.7 -  // owned by Swing thread
    28.8 +  // owned by GUI thread
    28.9    private var stack: List[Pretty_Tooltip] = Nil
   28.10  
   28.11    private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] =
   28.12    {
   28.13 -    Swing_Thread.require {}
   28.14 +    GUI_Thread.require {}
   28.15  
   28.16      if (stack.contains(tip)) Some(stack.span(_ != tip))
   28.17      else None
   28.18    }
   28.19  
   28.20    private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
   28.21 -    Swing_Thread.require { stack.find(tip => tip.original_parent == parent) }
   28.22 +    GUI_Thread.require { stack.find(tip => tip.original_parent == parent) }
   28.23  
   28.24    def apply(
   28.25      view: View,
   28.26 @@ -47,7 +47,7 @@
   28.27      results: Command.Results,
   28.28      info: Text.Info[XML.Body])
   28.29    {
   28.30 -    Swing_Thread.require {}
   28.31 +    GUI_Thread.require {}
   28.32  
   28.33      stack match {
   28.34        case top :: _ if top.results == results && top.info == info =>
   28.35 @@ -71,13 +71,13 @@
   28.36    }
   28.37  
   28.38  
   28.39 -  /* pending event and active state */  // owned by Swing thread
   28.40 +  /* pending event and active state */  // owned by GUI thread
   28.41  
   28.42    private var pending: Option[() => Unit] = None
   28.43    private var active = true
   28.44  
   28.45    private val pending_delay =
   28.46 -    Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
   28.47 +    GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
   28.48        pending match {
   28.49          case Some(body) => pending = None; body()
   28.50          case None =>
   28.51 @@ -85,7 +85,7 @@
   28.52      }
   28.53  
   28.54    def invoke(body: () => Unit): Unit =
   28.55 -    Swing_Thread.require {
   28.56 +    GUI_Thread.require {
   28.57        if (active) {
   28.58          pending = Some(body)
   28.59          pending_delay.invoke()
   28.60 @@ -93,18 +93,18 @@
   28.61      }
   28.62  
   28.63    def revoke(): Unit =
   28.64 -    Swing_Thread.require {
   28.65 +    GUI_Thread.require {
   28.66        pending = None
   28.67        pending_delay.revoke()
   28.68      }
   28.69  
   28.70    private lazy val reactivate_delay =
   28.71 -    Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
   28.72 +    GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
   28.73        active = true
   28.74      }
   28.75  
   28.76    private def deactivate(): Unit =
   28.77 -    Swing_Thread.require {
   28.78 +    GUI_Thread.require {
   28.79        revoke()
   28.80        active = false
   28.81        reactivate_delay.invoke()
   28.82 @@ -113,7 +113,7 @@
   28.83  
   28.84    /* dismiss */
   28.85  
   28.86 -  private lazy val focus_delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
   28.87 +  private lazy val focus_delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
   28.88    {
   28.89      dismiss_unfocused()
   28.90    }
   28.91 @@ -173,7 +173,7 @@
   28.92  {
   28.93    tip =>
   28.94  
   28.95 -  Swing_Thread.require {}
   28.96 +  GUI_Thread.require {}
   28.97  
   28.98  
   28.99    /* controls */
    29.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    29.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    29.3 @@ -25,10 +25,10 @@
    29.4    private val main =
    29.5      Session.Consumer[Prover.Message](getClass.getName) {
    29.6        case input: Prover.Input =>
    29.7 -        Swing_Thread.later { text_area.append(input.toString + "\n\n") }
    29.8 +        GUI_Thread.later { text_area.append(input.toString + "\n\n") }
    29.9  
   29.10        case output: Prover.Output =>
   29.11 -        Swing_Thread.later { text_area.append(output.message.toString + "\n\n") }
   29.12 +        GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
   29.13      }
   29.14  
   29.15    override def init() { PIDE.session.all_messages += main }
    30.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    30.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    30.3 @@ -307,7 +307,7 @@
    30.4    /* resize */
    30.5  
    30.6    private def handle_resize(): Unit =
    30.7 -    Swing_Thread.require {
    30.8 +    GUI_Thread.require {
    30.9        for (op <- operations) {
   30.10          op.pretty_text_area.resize(
   30.11            Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   30.12 @@ -315,7 +315,7 @@
   30.13      }
   30.14  
   30.15    private val delay_resize =
   30.16 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   30.17 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   30.18  
   30.19    addComponentListener(new ComponentAdapter {
   30.20      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   30.21 @@ -326,7 +326,7 @@
   30.22  
   30.23    private val main =
   30.24      Session.Consumer[Session.Global_Options](getClass.getName) {
   30.25 -      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
   30.26 +      case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
   30.27      }
   30.28  
   30.29    override def init()
    31.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    31.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    31.3 @@ -25,7 +25,7 @@
    31.4    private val main =
    31.5      Session.Consumer[Prover.Output](getClass.getName) {
    31.6        case output: Prover.Output =>
    31.7 -        Swing_Thread.later {
    31.8 +        GUI_Thread.later {
    31.9            text_area.append(XML.content(output.message))
   31.10            if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
   31.11          }
    32.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Jul 23 11:08:24 2014 +0200
    32.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Jul 23 11:19:24 2014 +0200
    32.3 @@ -43,7 +43,7 @@
    32.4    def robust_body[A](default: A)(body: => A): A =
    32.5    {
    32.6      try {
    32.7 -      Swing_Thread.require {}
    32.8 +      GUI_Thread.require {}
    32.9        if (buffer == text_area.getBuffer) body
   32.10        else {
   32.11          Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
   32.12 @@ -143,7 +143,7 @@
   32.13      def reset { update(None) }
   32.14    }
   32.15  
   32.16 -  // owned by Swing thread
   32.17 +  // owned by GUI thread
   32.18  
   32.19    private val highlight_area =
   32.20      new Active_Area[Color]((r: Rendering) => r.highlight _, None)
    33.1 --- a/src/Tools/jEdit/src/scala_console.scala	Wed Jul 23 11:08:24 2014 +0200
    33.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Wed Jul 23 11:19:24 2014 +0200
    33.3 @@ -57,7 +57,7 @@
    33.4    }
    33.5  
    33.6  
    33.7 -  /* global state -- owned by Swing thread */
    33.8 +  /* global state -- owned by GUI thread */
    33.9  
   33.10    @volatile private var interpreters = Map.empty[Console, Interpreter]
   33.11  
   33.12 @@ -72,7 +72,7 @@
   33.13      {
   33.14        val s = buf.synchronized { val s = buf.toString; buf.clear; s }
   33.15        val str = UTF8.decode_permissive(s)
   33.16 -      Swing_Thread.later {
   33.17 +      GUI_Thread.later {
   33.18          if (global_out == null) System.out.print(str)
   33.19          else global_out.writeAttrs(null, str)
   33.20        }
   33.21 @@ -124,7 +124,7 @@
   33.22    private def report_error(str: String)
   33.23    {
   33.24      if (global_console == null || global_err == null) System.err.println(str)
   33.25 -    else Swing_Thread.later { global_err.print(global_console.getErrorColor, str) }
   33.26 +    else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
   33.27    }
   33.28  
   33.29  
   33.30 @@ -167,7 +167,7 @@
   33.31              running.change(_ => None)
   33.32              Thread.interrupted()
   33.33            }
   33.34 -          Swing_Thread.later {
   33.35 +          GUI_Thread.later {
   33.36              if (err != null) err.commandDone()
   33.37              out.commandDone()
   33.38            }
    34.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    34.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    34.3 @@ -20,9 +20,9 @@
    34.4  
    34.5  class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
    34.6  {
    34.7 -  Swing_Thread.require {}
    34.8 +  GUI_Thread.require {}
    34.9  
   34.10 -  /* component state -- owned by Swing thread */
   34.11 +  /* component state -- owned by GUI thread */
   34.12  
   34.13    private var current_snapshot = Document.State.init.snapshot()
   34.14    private var current_command = Command.empty
   34.15 @@ -37,7 +37,7 @@
   34.16    private def update_contents()
   34.17    {
   34.18  
   34.19 -    Swing_Thread.require {}
   34.20 +    GUI_Thread.require {}
   34.21  
   34.22      val snapshot = current_snapshot
   34.23      val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
   34.24 @@ -71,7 +71,7 @@
   34.25  
   34.26    private def do_paint()
   34.27    {
   34.28 -    Swing_Thread.later {
   34.29 +    GUI_Thread.later {
   34.30        text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
   34.31      }
   34.32    }
   34.33 @@ -111,21 +111,21 @@
   34.34    private val main =
   34.35      Session.Consumer[Any](getClass.getName) {
   34.36        case _: Session.Global_Options =>
   34.37 -        Swing_Thread.later { handle_resize() }
   34.38 +        GUI_Thread.later { handle_resize() }
   34.39  
   34.40        case changed: Session.Commands_Changed =>
   34.41 -        Swing_Thread.later { handle_update(do_update) }
   34.42 +        GUI_Thread.later { handle_update(do_update) }
   34.43  
   34.44        case Session.Caret_Focus =>
   34.45 -        Swing_Thread.later { handle_update(do_update) }
   34.46 +        GUI_Thread.later { handle_update(do_update) }
   34.47  
   34.48        case Simplifier_Trace.Event =>
   34.49 -        Swing_Thread.later { handle_update(do_update) }
   34.50 +        GUI_Thread.later { handle_update(do_update) }
   34.51      }
   34.52  
   34.53    override def init()
   34.54    {
   34.55 -    Swing_Thread.require {}
   34.56 +    GUI_Thread.require {}
   34.57  
   34.58      PIDE.session.global_options += main
   34.59      PIDE.session.commands_changed += main
   34.60 @@ -136,7 +136,7 @@
   34.61  
   34.62    override def exit()
   34.63    {
   34.64 -    Swing_Thread.require {}
   34.65 +    GUI_Thread.require {}
   34.66  
   34.67      PIDE.session.global_options -= main
   34.68      PIDE.session.commands_changed -= main
   34.69 @@ -149,7 +149,7 @@
   34.70    /* resize */
   34.71  
   34.72    private val delay_resize =
   34.73 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   34.74 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   34.75  
   34.76    addComponentListener(new ComponentAdapter {
   34.77      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    35.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed Jul 23 11:08:24 2014 +0200
    35.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed Jul 23 11:19:24 2014 +0200
    35.3 @@ -136,7 +136,7 @@
    35.4  class Simplifier_Trace_Window(
    35.5    view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
    35.6  {
    35.7 -  Swing_Thread.require {}
    35.8 +  GUI_Thread.require {}
    35.9  
   35.10    private val pretty_text_area = new Pretty_Text_Area(view)
   35.11    private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
   35.12 @@ -167,7 +167,7 @@
   35.13  
   35.14    def do_paint()
   35.15    {
   35.16 -    Swing_Thread.later {
   35.17 +    GUI_Thread.later {
   35.18        pretty_text_area.resize(
   35.19          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   35.20      }
   35.21 @@ -182,7 +182,7 @@
   35.22    /* resize */
   35.23  
   35.24    private val delay_resize =
   35.25 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   35.26 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   35.27  
   35.28    peer.addComponentListener(new ComponentAdapter {
   35.29      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    36.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    36.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    36.3 @@ -55,14 +55,14 @@
    36.4  
    36.5    private def handle_resize()
    36.6    {
    36.7 -    Swing_Thread.require {}
    36.8 +    GUI_Thread.require {}
    36.9  
   36.10      pretty_text_area.resize(
   36.11        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   36.12    }
   36.13  
   36.14    private val delay_resize =
   36.15 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   36.16 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   36.17  
   36.18    addComponentListener(new ComponentAdapter {
   36.19      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   36.20 @@ -135,7 +135,7 @@
   36.21  
   36.22    private val main =
   36.23      Session.Consumer[Session.Global_Options](getClass.getName) {
   36.24 -      case _: Session.Global_Options => Swing_Thread.later { update_provers(); handle_resize() }
   36.25 +      case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() }
   36.26      }
   36.27  
   36.28    override def init()
    37.1 --- a/src/Tools/jEdit/src/spell_checker.scala	Wed Jul 23 11:08:24 2014 +0200
    37.2 +++ b/src/Tools/jEdit/src/spell_checker.scala	Wed Jul 23 11:19:24 2014 +0200
    37.3 @@ -105,7 +105,7 @@
    37.4  
    37.5    def dictionaries_selector(): Option_Component =
    37.6    {
    37.7 -    Swing_Thread.require {}
    37.8 +    GUI_Thread.require {}
    37.9  
   37.10      val option_name = "spell_checker_dictionary"
   37.11      val opt = PIDE.options.value.check_name(option_name)
    38.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    38.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    38.3 @@ -70,7 +70,7 @@
    38.4          val search_space =
    38.5            (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
    38.6          val search_delay =
    38.7 -          Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    38.8 +          GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    38.9              val search_words = Word.explode(Word.lowercase(search_field.text))
   38.10              val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
   38.11              val results =
    39.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    39.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    39.3 @@ -20,7 +20,7 @@
    39.4  
    39.5    private val syslog = new TextArea()
    39.6  
    39.7 -  private def syslog_delay = Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
    39.8 +  private def syslog_delay = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
    39.9    {
   39.10      val text = PIDE.session.syslog_content()
   39.11      if (text != syslog.text) syslog.text = text
    40.1 --- a/src/Tools/jEdit/src/text_overview.scala	Wed Jul 23 11:08:24 2014 +0200
    40.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Wed Jul 23 11:19:24 2014 +0200
    40.3 @@ -64,7 +64,7 @@
    40.4    override def paintComponent(gfx: Graphics)
    40.5    {
    40.6      super.paintComponent(gfx)
    40.7 -    Swing_Thread.assert {}
    40.8 +    GUI_Thread.assert {}
    40.9  
   40.10      doc_view.rich_text_area.robust_body(()) {
   40.11        JEdit_Lib.buffer_lock(buffer) {
    41.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    41.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    41.3 @@ -73,7 +73,7 @@
    41.4  
    41.5    private def handle_phase(phase: Session.Phase)
    41.6    {
    41.7 -    Swing_Thread.require {}
    41.8 +    GUI_Thread.require {}
    41.9      session_phase.text = " " + phase_text(phase) + " "
   41.10    }
   41.11  
   41.12 @@ -87,7 +87,7 @@
   41.13    add(controls.peer, BorderLayout.NORTH)
   41.14  
   41.15  
   41.16 -  /* component state -- owned by Swing thread */
   41.17 +  /* component state -- owned by GUI thread */
   41.18  
   41.19    private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
   41.20    private var nodes_required: Set[Document.Node.Name] = Set.empty
   41.21 @@ -192,7 +192,7 @@
   41.22  
   41.23    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   41.24    {
   41.25 -    Swing_Thread.require {}
   41.26 +    GUI_Thread.require {}
   41.27  
   41.28      val snapshot = PIDE.session.snapshot()
   41.29  
   41.30 @@ -220,10 +220,10 @@
   41.31    private val main =
   41.32      Session.Consumer[Any](getClass.getName) {
   41.33        case phase: Session.Phase =>
   41.34 -        Swing_Thread.later { handle_phase(phase) }
   41.35 +        GUI_Thread.later { handle_phase(phase) }
   41.36  
   41.37        case _: Session.Global_Options =>
   41.38 -        Swing_Thread.later {
   41.39 +        GUI_Thread.later {
   41.40            continuous_checking.load()
   41.41            logic.load ()
   41.42            update_nodes_required()
   41.43 @@ -231,7 +231,7 @@
   41.44          }
   41.45  
   41.46        case changed: Session.Commands_Changed =>
   41.47 -        Swing_Thread.later { handle_update(Some(changed.nodes)) }
   41.48 +        GUI_Thread.later { handle_update(Some(changed.nodes)) }
   41.49      }
   41.50  
   41.51    override def init()
    42.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
    42.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
    42.3 @@ -145,13 +145,13 @@
    42.4    add(controls.peer, BorderLayout.NORTH)
    42.5  
    42.6  
    42.7 -  /* component state -- owned by Swing thread */
    42.8 +  /* component state -- owned by GUI thread */
    42.9  
   42.10    private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
   42.11  
   42.12    private def make_entries(): List[Entry] =
   42.13    {
   42.14 -    Swing_Thread.require {}
   42.15 +    GUI_Thread.require {}
   42.16  
   42.17      val name =
   42.18        Document_View(view.getTextArea) match {
   42.19 @@ -174,7 +174,7 @@
   42.20  
   42.21    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   42.22    {
   42.23 -    Swing_Thread.require {}
   42.24 +    GUI_Thread.require {}
   42.25  
   42.26      val snapshot = PIDE.session.snapshot()
   42.27  
   42.28 @@ -204,7 +204,7 @@
   42.29    private val main =
   42.30      Session.Consumer[Session.Commands_Changed](getClass.getName) {
   42.31        case changed =>
   42.32 -        Swing_Thread.later { handle_update(Some(changed.nodes)) }
   42.33 +        GUI_Thread.later { handle_update(Some(changed.nodes)) }
   42.34      }
   42.35  
   42.36    override def init()
    43.1 --- a/src/Tools/jEdit/src/token_markup.scala	Wed Jul 23 11:08:24 2014 +0200
    43.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Wed Jul 23 11:19:24 2014 +0200
    43.3 @@ -42,7 +42,7 @@
    43.4  
    43.5    def edit_control_style(text_area: TextArea, control: String)
    43.6    {
    43.7 -    Swing_Thread.assert {}
    43.8 +    GUI_Thread.assert {}
    43.9  
   43.10      val buffer = text_area.getBuffer
   43.11