src/Tools/jEdit/src/protocol_dockable.scala
changeset 46918 1752164d916b
parent 46774 38f113b052b1
child 50205 788c8263e634
     1.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Wed Mar 14 14:49:43 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Mar 14 15:09:33 2012 +0100
     1.3 @@ -29,10 +29,10 @@
     1.4      loop {
     1.5        react {
     1.6          case input: Isabelle_Process.Input =>
     1.7 -          Swing_Thread.now { text_area.append(input.toString + "\n") }
     1.8 +          Swing_Thread.later { text_area.append(input.toString + "\n") }
     1.9  
    1.10          case output: Isabelle_Process.Output =>
    1.11 -          Swing_Thread.now { text_area.append(output.message.toString + "\n") }
    1.12 +          Swing_Thread.later { text_area.append(output.message.toString + "\n") }
    1.13  
    1.14          case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    1.15        }