misc tuning;
authorwenzelm
Tue, 15 Sep 2009 17:00:21 +0200
changeset 34729 5bf8f8200762
parent 34728 e3df9c8699ea
child 34730 819862460a12
misc tuning;
src/Tools/jEdit/src/jedit/ProverSetup.scala
src/Tools/jEdit/src/prover/Prover.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
   }
-
 }
--- 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)
   }
 }