# HG changeset patch
# User wenzelm
# Date 1274285134 -7200
# Node ID 8af34e1609680eb205c4a8b7e6db13479e09f74c
# Parent  942532de16f62c23366c2b653416cfc917f8ed8d
show fully detailed protocol messages;

diff -r 942532de16f6 -r 8af34e160968 src/Tools/jEdit/src/jedit/protocol_dockable.scala
--- 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)
       }