# HG changeset patch
# User wenzelm
# Date 1253026821 -7200
# Node ID 5bf8f82007627b41eef4bec6b606392de5d3cbc3
# Parent  e3df9c8699ea0d3064367fbdb1996eeff7d7a851
misc tuning;

diff -r e3df9c8699ea -r 5bf8f8200762 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Sep 15 15:37:19 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Sep 15 17:00:21 2009 +0200
@@ -7,12 +7,8 @@
 package isabelle.jedit
 
 
-import org.w3c.dom.Document
-
 import org.gjt.sp.jedit.{Buffer, View}
 
-import javax.swing.JTextArea
-
 import isabelle.prover.Prover
 
 
@@ -21,7 +17,6 @@
   var prover: Prover = null
   var theory_view: TheoryView = null
 
-
   def activate(view: View)
   {
     // TheoryView starts prover
@@ -29,14 +24,12 @@
     prover = theory_view.prover
 
     theory_view.activate()
-    prover.set_document(buffer.getName)
-
+    prover.begin_document(buffer.getName)
   }
 
-  def deactivate
+  def deactivate()
   {
     theory_view.deactivate
     prover.stop
   }
-
 }
diff -r e3df9c8699ea -r 5bf8f8200762 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Sep 15 15:37:19 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Sep 15 17:00:21 2009 +0200
@@ -141,21 +141,15 @@
 
   /* document changes */
 
-  def handle_change(change: Change) {
-    val old = document(change.parent.get.id).get
-    val (doc, structure_change) = old.text_changed(change)
-    document_versions ::= doc
-    edit_document(old, doc, structure_change)
-    document_change.event(doc)
-  }
-
-  def set_document(path: String) {
+  def begin_document(path: String) {
     process.begin_document(document_0.id, path)
   }
 
-  private def edit_document(old: ProofDocument, doc: ProofDocument,
-    changes: ProofDocument.StructureChange) =
-  {
+  def handle_change(change: Change) {
+    val old = document(change.parent.get.id).get
+    val (doc, changes) = old.text_changed(change)
+    document_versions ::= doc
+
     val id_changes = changes map { case (c1, c2) =>
       (c1.map(_.id).getOrElse(document_0.id),
       c2 match {
@@ -167,5 +161,7 @@
       })
     }
     process.edit_document(old.id, doc.id, id_changes)
+
+    document_change.event(doc)
   }
 }