--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 13:29:44 2009 +0200
@@ -106,14 +106,13 @@
val start = buffer.getLineStartOffset(line)
val stop = start + line_segment.count
- val document = prover.document
val theory_view = Isabelle.prover_setup(buffer).get.theory_view
+ val document = theory_view.current_document()
def to: Int => Int = theory_view.to_current(document.id, _)
def from: Int => Int = theory_view.from_current(document.id, _)
+ var command = document.find_command_at(from(start))
var next_x = start
-
- var command = document.find_command_at(from(start))
while (command != null && command.start(document) < from(stop)) {
for {
markup <- command.highlight_node.flatten
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Wed Jul 08 13:29:44 2009 +0200
@@ -48,8 +48,8 @@
if (!prover.isDefined || !theory_view_opt.isDefined) null
else if (prover.get == null || theory_view_opt.get == null) null
else {
- val document = prover.get.document
val theory_view = theory_view_opt.get
+ val document = theory_view.current_document()
val offset = theory_view.from_current(document, original_offset)
val cmd = document.find_command_at(offset)
if (cmd != null) {
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Wed Jul 08 13:29:44 2009 +0200
@@ -32,7 +32,7 @@
val prover_setup = Isabelle.plugin.prover_setup(buffer)
if (prover_setup.isDefined) {
- val document = prover_setup.get.prover.document
+ val document = prover_setup.get.theory_view.current_document()
for (command <- document.commands)
data.root.add(command.markup_root.swing_node(document))
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Jul 08 13:29:44 2009 +0200
@@ -79,9 +79,9 @@
override def paintComponent(gfx : Graphics) {
super.paintComponent(gfx)
-
val buffer = textarea.getBuffer
- val document = prover.document
+ val theory_view = Isabelle.prover_setup(buffer).get.theory_view
+ val document = theory_view.current_document()
for (c <- document.commands)
paintCommand(c, buffer, document, gfx)
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:44 2009 +0200
@@ -54,6 +54,8 @@
private var col: Text.Change = null
+ private var doc_id: IsarDocument.Document_ID = prover.document(null).id
+ def current_document() = prover.document(doc_id)
private val col_timer = new Timer(300, new ActionListener() {
override def actionPerformed(e: ActionEvent) = commit
@@ -70,7 +72,7 @@
private val selected_state_controller = new CaretListener {
override def caretUpdate(e: CaretEvent) = {
- val doc = prover.document
+ val doc = current_document()
val cmd = doc.find_command_at(e.getDot)
if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
Isabelle.prover_setup(buffer).get.selected_state != cmd)
@@ -85,12 +87,9 @@
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), "")
- }
+ col = Text.Change(doc_id, Isabelle.system.id(), 0,
+ buffer.getText(0, buffer.getLength), "")
+ commit
}
def deactivate() {
@@ -124,7 +123,7 @@
def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int =
changes match {
case Nil => pos
- case Text.Change(id, start, added, removed) :: rest_changes => {
+ case Text.Change(_, id, start, added, removed) :: rest_changes => {
val shifted =
if (start <= pos)
if (pos < start + added.length) start
@@ -138,7 +137,7 @@
def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int =
changes match {
case Nil => pos
- case Text.Change(id, start, added, removed) :: rest_changes => {
+ case Text.Change(_, id, start, added, removed) :: rest_changes => {
val shifted = _to_current(from_id, rest_changes, pos)
if (id == from_id) pos
else if (start <= shifted) {
@@ -159,7 +158,7 @@
def repaint(cmd: Command) =
{
- val document = prover.document
+ val document = current_document()
if (text_area != null) {
val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document)))
val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1)
@@ -202,7 +201,7 @@
override def paintValidLine(gfx: Graphics2D,
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
- val document = prover.document
+ val document = current_document()
def from_current(pos: Int) = this.from_current(document.id, pos)
def to_current(pos: Int) = this.to_current(document.id, pos)
val saved_color = gfx.getColor
@@ -222,7 +221,7 @@
}
override def getToolTipText(x: Int, y: Int) = {
- val document = prover.document
+ val document = current_document()
val offset = from_current(document.id, text_area.xyToOffset(x, y))
val cmd = document.find_command_at(offset)
if (cmd != null) {
@@ -240,12 +239,13 @@
def split_changes(c: Text.Change): List[Text.Change] = {
val MAX = TheoryView.MAX_CHANGE_LENGTH
if (c.added.length <= MAX) List(c)
- else Text.Change(c.id, c.start, c.added.substring(0, MAX), c.removed) ::
- split_changes(new Text.Change(id(), c.start + MAX, c.added.substring(MAX), c.removed))
+ else Text.Change(c.base_id, c.id, c.start, c.added.substring(0, MAX), c.removed) ::
+ split_changes(new Text.Change(c.id, id(), c.start + MAX, c.added.substring(MAX), ""))
}
val new_changes = split_changes(col)
changes = new_changes.reverse ::: changes
new_changes map (document_actor ! _)
+ doc_id = new_changes.last.id
}
col = null
if (col_timer.isRunning())
@@ -271,12 +271,12 @@
{
val text = buffer.getText(offset, length)
if (col == null)
- col = new Text.Change(id(), offset, text, "")
+ col = new Text.Change(doc_id, id(), offset, text, "")
else if (col.start <= offset && offset <= col.start + col.added.length)
- col = new Text.Change(col.id, col.start, col.added + text, col.removed)
+ col = new Text.Change(doc_id, col.id, col.start, col.added + text, col.removed)
else {
commit
- col = new Text.Change(id(), offset, text, "")
+ col = new Text.Change(doc_id, id(), offset, text, "")
}
delay_commit
}
@@ -286,10 +286,10 @@
{
val removed = buffer.getText(start, removed_length)
if (col == null)
- col = new Text.Change(id(), start, "", removed)
+ col = new Text.Change(doc_id, id(), start, "", removed)
else if (col.start > start + removed_length || start > col.start + col.added.length) {
commit
- col = new Text.Change(id(), start, "", removed)
+ col = new Text.Change(doc_id, id(), start, "", removed)
}
else {
/* val offset = start - col.start
@@ -301,7 +301,7 @@
(diff - (offset min 0), offset min 0)
col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
commit
- col = new Text.Change(id(), start, "", removed)
+ col = new Text.Change(doc_id, id(), start, "", removed)
}
delay_commit
}
--- a/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 13:29:44 2009 +0200
@@ -8,7 +8,12 @@
object Text {
- case class Change(id: String, start: Int, val added: String, val removed: String) {
+ case class Change(
+ base_id: String,
+ id: String,
+ start: Int,
+ added: String,
+ removed: String) {
override def toString = "start: " + start + " added: " + added + " removed: " + removed
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 13:29:44 2009 +0200
@@ -23,8 +23,6 @@
object ProverEvents {
case class Activate
- case class SetEventBus(bus: EventBus[StructureChange])
- case class SetIsCommandKeyword(is_command_keyword: String => Boolean)
}
class Prover(isabelle_system: Isabelle_System, logic: String) extends Actor
@@ -47,12 +45,13 @@
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.set_command_keyword(command_decls.contains))
- private val document_id0 = ProofDocument.empty.id
+ private val document_0 =
+ ProofDocument.empty.set_command_keyword(command_decls.contains)
+ private var document_versions = List(document_0)
def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
- def document = document_versions.head
+ def document(id: IsarDocument.Document_ID) =
+ document_versions.find(_.id == id).getOrElse(document_0)
private var initialized = false
@@ -91,7 +90,7 @@
private def handle_result(result: Isabelle_Process.Result)
{
- def command_change(c: Command) = this ! c
+ def command_change(c: Command) = change_receiver ! c
val (running, command) =
result.props.find(p => p._1 == Markup.ID) match {
case None => (false, null)
@@ -231,38 +230,34 @@
loop {
react {
case change: Text.Change => {
- val old = document
+ val old = document(change.base_id)
val (doc, structure_change) = old.text_changed(change)
document_versions ::= doc
- edit_document(old.id, doc.id, structure_change)
+ edit_document(old, doc, structure_change)
}
- case command: Command => {
- //state of command has changed
- change_receiver ! command
- }
+ case x => System.err.println("warning: ignored " + x)
}
}
}
def set_document(change_receiver: Actor, path: String) {
this.change_receiver = change_receiver
- process.begin_document(document_id0, path)
+ process.begin_document(document_0.id, path)
}
- private def edit_document(old_id: String, document_id: String, changes: StructureChange) =
- Swing_Thread.now {
- val removes =
- for (cmd <- changes.removed_commands) yield {
- commands -= cmd.id
- if (cmd.state_id != null) states -= cmd.state_id
- changes.before_change.map(_.id).getOrElse(document_id0) -> None
- }
- val inserts =
- for (cmd <- changes.added_commands) yield {
- commands += (cmd.id -> cmd)
- process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
- (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id)
- }
- process.edit_document(old_id, document_id, removes.reverse ++ inserts)
- }
+ private def edit_document(old: ProofDocument, doc: ProofDocument, changes: StructureChange) = {
+ val removes =
+ for (cmd <- changes.removed_commands) yield {
+ commands -= cmd.id
+ if (cmd.state_id != null) states -= cmd.state_id
+ changes.before_change.map(_.id).getOrElse(document_0.id) -> None
+ }
+ val inserts =
+ for (cmd <- changes.added_commands) yield {
+ commands += (cmd.id -> cmd)
+ process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
+ (doc.commands.prev(cmd).map(_.id).getOrElse(document_0.id)) -> Some(cmd.id)
+ }
+ process.edit_document(old.id, doc.id, removes.reverse ++ inserts)
+ }
}