src/Tools/jEdit/src/syslog_dockable.scala
changeset 53177 dcac8d837b9c
parent 50205 788c8263e634
child 55618 995162143ef4
     1.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     1.3 @@ -23,10 +23,10 @@
     1.4  
     1.5    private def update_syslog()
     1.6    {
     1.7 -    Swing_Thread.later {
     1.8 -      val text = PIDE.session.current_syslog()
     1.9 -      if (text != syslog.text) syslog.text = text
    1.10 -    }
    1.11 +    Swing_Thread.require()
    1.12 +
    1.13 +    val text = PIDE.session.current_syslog()
    1.14 +    if (text != syslog.text) syslog.text = text
    1.15    }
    1.16  
    1.17    set_content(syslog)
    1.18 @@ -38,7 +38,7 @@
    1.19      loop {
    1.20        react {
    1.21          case output: Isabelle_Process.Output =>
    1.22 -          if (output.is_syslog) update_syslog()
    1.23 +          if (output.is_syslog) Swing_Thread.later { update_syslog() }
    1.24  
    1.25          case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
    1.26        }