src/Tools/jEdit/src/raw_output_dockable.scala
changeset 44734 7313e2db3d39
parent 44297 b3bd26fd22d3
child 45633 2cb7e34f6096
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 11:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 11:25:27 2011 +0200
@@ -29,8 +29,6 @@
   private val main_actor = actor {
     loop {
       react {
-        case input: Isabelle_Process.Input =>
-
         case result: Isabelle_Process.Result =>
           if (result.is_stdout)
             Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
@@ -40,6 +38,6 @@
     }
   }
 
-  override def init() { Isabelle.session.raw_messages += main_actor }
-  override def exit() { Isabelle.session.raw_messages -= main_actor }
+  override def init() { Isabelle.session.raw_output_messages += main_actor }
+  override def exit() { Isabelle.session.raw_output_messages -= main_actor }
 }