author | wenzelm |
Wed, 19 May 2010 18:05:34 +0200 | |
changeset 36987 | 8af34e160968 |
parent 36986 | 942532de16f6 |
child 36988 | fd641bc85222 |
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Wed May 19 17:39:22 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Wed May 19 18:05:34 2010 +0200 @@ -33,7 +33,7 @@ loop { react { case result: Isabelle_Process.Result => - Swing_Thread.now { text_area.append(result.toString + "\n") } + Swing_Thread.now { text_area.append(result.message.toString + "\n") } case bad => System.err.println("raw_actor: ignoring bad message " + bad) }