--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Wed Jul 08 13:29:43 2009 +0200
@@ -40,13 +40,6 @@
theory_view = new TheoryView(view.getTextArea, prover)
prover.set_document(theory_view.change_receiver, buffer.getName)
- theory_view.activate
- val MAX = TheoryView.MAX_CHANGE_LENGTH
- for (i <- 0 to buffer.getLength / MAX) {
- prover ! new isabelle.proofdocument.Text.Change(
- Isabelle.system.id(), i * MAX,
- buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), "")
- }
// register output-view
prover.output_info += (text =>
@@ -82,7 +75,6 @@
def deactivate
{
- buffer.setTokenMarker(buffer.getMode.getTokenMarker)
theory_view.deactivate
prover.stop
}
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:43 2009 +0200
@@ -12,7 +12,7 @@
import scala.actors.Actor._
import isabelle.proofdocument.Text
-import isabelle.prover.{Prover, Command}
+import isabelle.prover.{Prover, ProverEvents, Command}
import java.awt.Graphics2D
import java.awt.event.{ActionEvent, ActionListener}
@@ -22,7 +22,7 @@
import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.SyntaxStyle
+import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
object TheoryView
@@ -51,7 +51,6 @@
private val buffer = text_area.getBuffer
private val prover = Isabelle.prover_setup(buffer).get.prover
- buffer.addBufferListener(this)
private var col: Text.Change = null
@@ -84,9 +83,19 @@
text_area.addLeftOfScrollBar(phase_overview)
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
+ buffer.addBufferListener(this)
+
+ val MAX = TheoryView.MAX_CHANGE_LENGTH
+ for (i <- 0 to buffer.getLength / MAX) {
+ prover ! new isabelle.proofdocument.Text.Change(
+ Isabelle.system.id(), i * MAX,
+ buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), "")
+ }
}
def deactivate() {
+ buffer.setTokenMarker(buffer.getMode.getTokenMarker)
+ buffer.removeBufferListener(this)
text_area.getPainter.removeExtension(this)
text_area.removeLeftOfScrollBar(phase_overview)
text_area.removeCaretListener(selected_state_controller)
@@ -101,10 +110,13 @@
val change_receiver = actor {
loop {
react {
- case _ =>
+ case ProverEvents.Activate =>
+ activate()
+ case c: Command =>
update_delay()
repaint_delay()
phase_overview.repaint_delay()
+ case x => System.err.println("warning: change_receiver ignored " + x)
}
}
}
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Wed Jul 08 13:29:43 2009 +0200
@@ -40,7 +40,7 @@
val empty =
new ProofDocument(isabelle.jedit.Isabelle.system.id(),
- LinearSet(), Map(), LinearSet(), false, _ => false)
+ LinearSet(), Map(), LinearSet(), _ => false)
}
@@ -49,19 +49,11 @@
val tokens: LinearSet[Token],
val token_start: Map[Token, Int],
val commands: LinearSet[Command],
- val active: Boolean,
is_command_keyword: String => Boolean)
{
- def mark_active: ProofDocument =
- new ProofDocument(id, tokens, token_start, commands, true, is_command_keyword)
- def activate: (ProofDocument, StructureChange) = {
- val (doc, change) =
- text_changed(new Text.Change(isabelle.jedit.Isabelle.system.id(), 0, content, content))
- return (doc.mark_active, change)
- }
def set_command_keyword(f: String => Boolean): ProofDocument =
- new ProofDocument(isabelle.jedit.Isabelle.system.id(), tokens, token_start, commands, active, f)
+ new ProofDocument(id, tokens, token_start, commands, f)
def content = Token.string_from_tokens(Nil ++ tokens, token_start)
/** token view **/
@@ -222,7 +214,7 @@
val doc =
new ProofDocument(new_id, new_tokenset, new_token_start,
- new_commandset, active, is_command_keyword)
+ new_commandset, is_command_keyword)
return (doc, change)
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 13:29:43 2009 +0200
@@ -47,7 +47,8 @@
mutable.SynchronizedMap[IsarDocument.State_ID, Command]
private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
- private var document_versions = List(ProofDocument.empty)
+ private var document_versions =
+ List(ProofDocument.empty.set_command_keyword(command_decls.contains))
private val document_id0 = ProofDocument.empty.id
def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
@@ -85,7 +86,6 @@
/* event handling */
- val activated = new EventBus[Unit]
val output_info = new EventBus[String]
var change_receiver: Actor = null
@@ -138,7 +138,7 @@
case XML.Elem(Markup.READY, _, _)
if !initialized =>
initialized = true
- Swing_Thread.now { this ! ProverEvents.Activate }
+ change_receiver ! ProverEvents.Activate
// document edits
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
@@ -230,18 +230,6 @@
import ProverEvents._
loop {
react {
- case Activate => {
- val old = document
- val (doc, structure_change) = old.activate
- document_versions ::= doc
- edit_document(old.id, doc.id, structure_change)
- }
- case SetIsCommandKeyword(f) => {
- val old = document
- val doc = old.set_command_keyword(f)
- document_versions ::= doc
- edit_document(old.id, doc.id, StructureChange(None, Nil, Nil))
- }
case change: Text.Change => {
val old = document
val (doc, structure_change) = old.text_changed(change)
@@ -258,7 +246,6 @@
def set_document(change_receiver: Actor, path: String) {
this.change_receiver = change_receiver
- this ! ProverEvents.SetIsCommandKeyword(command_decls.contains)
process.begin_document(document_id0, path)
}