--- 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)
}
}