# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID 20e8dcd29a8bd9b6bf98fcf8503c25ead97986fc
# Parent  d179fcb04cbc9c497c08ac9b30da7015dfa85a06
TheoryView starts Prover

diff -r d179fcb04cbc -r 20e8dcd29a8b src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -19,7 +19,7 @@
 import javax.swing.{JTextArea, JScrollPane}
 
 
-class ProverSetup(buffer: JEditBuffer)
+class ProverSetup(buffer: Buffer)
 {
   var prover: Prover = null
   var theory_view: TheoryView = null
@@ -27,13 +27,12 @@
 
   def activate(view: View)
   {
-    prover = new Prover(Isabelle.system, Isabelle.default_logic)
-    prover.start() // start actor
-    val buffer = view.getBuffer
+    // TheoryView starts prover
+    theory_view = new TheoryView(view.getTextArea)
+    prover = theory_view.prover
 
-    theory_view = new TheoryView(view.getTextArea, prover)
     theory_view.activate()
-    prover.set_document(theory_view.change_receiver, buffer.getName)
+    prover.set_document(buffer.getName)
 
   }
 
diff -r d179fcb04cbc -r 20e8dcd29a8b 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
@@ -39,14 +39,17 @@
 }
 
 
-class TheoryView (text_area: JEditTextArea, document_actor: Actor)
+class TheoryView (text_area: JEditTextArea)
     extends TextAreaExtension with BufferListener
 {
 
   def id() = Isabelle.system.id()
   
   private val buffer = text_area.getBuffer
-  private val prover = Isabelle.prover_setup(buffer).get.prover
+
+  // start prover
+  val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic, change_receiver)
+  prover.start() // start actor
 
 
   private var edits: List[Edit] = Nil
@@ -207,7 +210,7 @@
 
   /* history of changes - TODO: seperate class?*/
 
-  val change_0 = new Change(prover.document_0.id, None, Nil)
+  val change_0: Change = new Change(prover.document_0.id, None, Nil)
   private var changes = List(change_0)
   private var current_change = change_0
   def get_changes = changes
@@ -271,7 +274,7 @@
     if (!edits.isEmpty) {
       val change = new Change(Isabelle.system.id(), Some(current_change), edits)
       changes ::= change
-      document_actor ! change
+      prover ! change
       current_change = change
     }
     edits = Nil
diff -r d179fcb04cbc -r 20e8dcd29a8b 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
@@ -26,7 +26,8 @@
   case class Activate
 }
 
-class Prover(isabelle_system: Isabelle_System, logic: String) extends Actor
+class Prover(isabelle_system: Isabelle_System, logic: String, change_receiver: Actor)
+extends Actor
 {
   /* prover process */
 
@@ -85,7 +86,6 @@
 
   /* event handling */
   val output_info = new EventBus[Isabelle_Process.Result]
-  var change_receiver: Actor = null
 
   val output_text_view = new JTextArea
   output_info += (result => output_text_view.append(result.toString + "\n"))
@@ -242,8 +242,7 @@
     }
   }
   
-  def set_document(change_receiver: Actor, path: String) {
-    this.change_receiver = change_receiver
+  def set_document(path: String) {
     process.begin_document(document_0.id, path)
   }