# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID 1a30c075c202b80dc1e73910c648c178eea62be8
# Parent  20e8dcd29a8bd9b6bf98fcf8503c25ead97986fc
change_receiver and output_info are used before regular initialisation

diff -r 20e8dcd29a8b -r 1a30c075c202 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -108,7 +108,7 @@
   val update_delay = Swing_Thread.delay(500){ buffer.propertiesChanged() }
   val repaint_delay = Swing_Thread.delay(100){ repaint_all() }
   
-  val change_receiver = actor {
+  lazy val change_receiver = actor {
     loop {
       react {
         case ProverEvents.Activate =>
diff -r 20e8dcd29a8b -r 1a30c075c202 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -85,7 +85,7 @@
 
 
   /* event handling */
-  val output_info = new EventBus[Isabelle_Process.Result]
+  lazy val output_info = new EventBus[Isabelle_Process.Result]
 
   val output_text_view = new JTextArea
   output_info += (result => output_text_view.append(result.toString + "\n"))