src/Pure/GUI/system_dialog.scala
changeset 57612 990ffb84489b
parent 56662 f373fb77e0a4
child 59201 702e0971d617
     1.1 --- a/src/Pure/GUI/system_dialog.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Pure/GUI/system_dialog.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  class System_Dialog extends Build.Progress
     1.6  {
     1.7 -  /* GUI state -- owned by Swing thread */
     1.8 +  /* component state -- owned by GUI thread */
     1.9  
    1.10    private var _title = "Isabelle"
    1.11    private var _window: Option[Window] = None
    1.12 @@ -26,7 +26,7 @@
    1.13  
    1.14    private def check_window(): Window =
    1.15    {
    1.16 -    Swing_Thread.require {}
    1.17 +    GUI_Thread.require {}
    1.18  
    1.19      _window match {
    1.20        case Some(window) => window
    1.21 @@ -48,7 +48,7 @@
    1.22  
    1.23    private def conclude()
    1.24    {
    1.25 -    Swing_Thread.require {}
    1.26 +    GUI_Thread.require {}
    1.27      require(_return_code.isDefined)
    1.28  
    1.29      _window match {
    1.30 @@ -142,7 +142,7 @@
    1.31      /* exit */
    1.32  
    1.33      val delay_exit =
    1.34 -      Swing_Thread.delay_first(Time.seconds(1.0))
    1.35 +      GUI_Thread.delay_first(Time.seconds(1.0))
    1.36        {
    1.37          if (can_auto_close) conclude()
    1.38          else {
    1.39 @@ -160,13 +160,13 @@
    1.40    /* progress operations */
    1.41  
    1.42    def title(txt: String): Unit =
    1.43 -    Swing_Thread.later {
    1.44 +    GUI_Thread.later {
    1.45        _title = txt
    1.46        _window.foreach(window => window.title = txt)
    1.47      }
    1.48  
    1.49    def return_code(rc: Int): Unit =
    1.50 -    Swing_Thread.later {
    1.51 +    GUI_Thread.later {
    1.52        _return_code = Some(rc)
    1.53        _window match {
    1.54          case None => conclude()
    1.55 @@ -175,7 +175,7 @@
    1.56      }
    1.57  
    1.58    override def echo(txt: String): Unit =
    1.59 -    Swing_Thread.later {
    1.60 +    GUI_Thread.later {
    1.61        val window = check_window()
    1.62        window.text.append(txt + "\n")
    1.63        val vertical = window.scroll_text.peer.getVerticalScrollBar