change_receiver and output_info are used before regular initialisation
authorimmler@in.tum.de
Thu, 27 Aug 2009 10:51:09 +0200
changeset 34673 1a30c075c202
parent 34672 20e8dcd29a8b
child 34674 f9b71bcf2eb7
change_receiver and output_info are used before regular initialisation
src/Tools/jEdit/src/jedit/TheoryView.scala
src/Tools/jEdit/src/prover/Prover.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 =>
--- 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"))