--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:55:20 2009 +0200
@@ -87,24 +87,26 @@
def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(document.id, _)
var next_x = start
- for {
- command <- document.commands.
- dropWhile(_.stop(document) <= from(start)).
- takeWhile(_.start(document) < from(stop))
- markup <- command.highlight_node.flatten
- if (to(markup.abs_stop(document)) > start)
- if (to(markup.abs_start(document)) < stop)
- byte = DynamicTokenMarker.choose_byte(markup.info.toString)
- token_start = to(markup.abs_start(document)) - start max 0
- token_length =
- to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
- (start - to(markup.abs_start(document)) max 0) -
- (to(markup.abs_stop(document)) - stop max 0)
- } {
- if (start + token_start > next_x)
- handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
- handler.handleToken(line_segment, byte, token_start, token_length, context)
- next_x = start + token_start + token_length
+
+ var command = document.find_command_at(from(start))
+ while (command != null && command.start(document) < from(stop)) {
+ for {
+ markup <- command.highlight_node.flatten
+ if (to(markup.abs_stop(document)) > start)
+ if (to(markup.abs_start(document)) < stop)
+ byte = DynamicTokenMarker.choose_byte(markup.info.toString)
+ token_start = to(markup.abs_start(document)) - start max 0
+ token_length =
+ to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
+ (start - to(markup.abs_start(document)) max 0) -
+ (to(markup.abs_stop(document)) - stop max 0)
+ } {
+ if (start + token_start > next_x)
+ handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
+ handler.handleToken(line_segment, byte, token_start, token_length, context)
+ next_x = start + token_start + token_length
+ }
+ command = document.commands.next(command).getOrElse(null)
}
if (next_x < stop)
handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jun 02 22:55:20 2009 +0200
@@ -43,8 +43,11 @@
if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length)
else path)
theory_view.activate
- prover ! new isabelle.proofdocument.Text.Change(
- Isabelle.plugin.id(), 0, buffer.getText(0, buffer.getLength), 0)
+ val MCL = TheoryView.MAX_CHANGE_LENGTH
+ for (i <- 0 to buffer.getLength / MCL)
+ prover ! new isabelle.proofdocument.Text.Change(
+ Isabelle.plugin.id(), i * MCL,
+ buffer.getText(i * MCL, MCL min buffer.getLength - i * MCL),0)
//register output-view
prover.output_info += (text =>
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:55:20 2009 +0200
@@ -197,14 +197,14 @@
val saved_color = gfx.getColor
val metrics = text_area.getPainter.getFontMetrics
+
+ // encolor phase
var e = document.find_command_at(from_current(start))
- val commands = document.commands.dropWhile(_.stop(document) <= from_current(start)).
- takeWhile(c => to_current(c.start(document)) < end)
- // encolor phase
- for (e <- commands) {
+ while (e != null && e.start(document) < end) {
val begin = start max to_current(e.start(document))
val finish = end - 1 min to_current(e.stop(document))
encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
+ e = document.commands.next(e).getOrElse(null)
}
gfx.setColor(saved_color)
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 22:55:20 2009 +0200
@@ -61,7 +61,7 @@
return (doc.mark_active, change)
}
def set_command_keyword(f: String => Boolean): ProofDocument =
- new ProofDocument(id, tokens, token_start, commands, active, f)
+ new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), tokens, token_start, commands, active, f)
def content = Token.string_from_tokens(Nil ++ tokens, token_start)
/** token view **/
@@ -126,7 +126,8 @@
case t :: ts =>
if (start(t) == start(new_token) &&
start(t) > change.start + change.added.length) {
- old_suffix = ts
+ old_suffix = t :: ts
+ new_tokens = new_tokens.tail
invalid_tokens = Nil
}
case _ =>
@@ -134,42 +135,45 @@
}
val insert = new_tokens.reverse
val new_token_list = begin ::: insert ::: old_suffix
- val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
token_changed(change.id, begin.lastOption, insert,
- old_suffix.firstOption, new_tokenset, start)
+ old_suffix.firstOption, new_token_list, start)
}
/** command view **/
- def find_command_at(pos: Int): Command = {
- for (cmd <- commands) { if (pos < cmd.stop(this)) return cmd }
- return null
- }
-
private def token_changed(
new_id: String,
before_change: Option[Token],
inserted_tokens: List[Token],
after_change: Option[Token],
- new_tokenset: LinearSet[Token],
+ new_tokens: List[Token],
new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
{
- val cmd_first_changed =
- if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get))
- else None
- val cmd_last_changed =
- if (after_change.isDefined) commands.find(_.tokens.contains(after_change.get))
- else None
+ val new_tokenset = (LinearSet() ++ new_tokens).asInstanceOf[LinearSet[Token]]
+ val cmd_before_change = before_change match {
+ case None => None
+ case Some(bc) =>
+ val cmd_with_bc = commands.find(_.contains(bc)).get
+ if (cmd_with_bc.tokens.last == bc) {
+ if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
+ Some(cmd_with_bc)
+ else commands.prev(cmd_with_bc)
+ }
+ else commands.prev(cmd_with_bc)
+ }
- val cmd_before_change =
- if (cmd_first_changed.isDefined) commands.prev(cmd_first_changed.get)
- else None
- val cmd_after_change =
- if (cmd_last_changed.isDefined) commands.next(cmd_last_changed.get)
- else None
+ val cmd_after_change = after_change match {
+ case None => None
+ case Some(ac) =>
+ val cmd_with_ac = commands.find(_.contains(ac)).get
+ if (ac.is_start)
+ Some(cmd_with_ac)
+ else
+ commands.next(cmd_with_ac)
+ }
- val removed_commands = commands.dropWhile(Some(_) != cmd_first_changed).
+ val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
takeWhile(Some(_) != cmd_after_change)
// calculate inserted commands
@@ -183,21 +187,33 @@
}
}
- val split_begin_tokens =
- if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil
- else {
- cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) :::
- List(before_change.get)
- }
- val split_end_tokens =
- if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil
- else {
- cmd_last_changed.get.tokens.dropWhile(_ != after_change.get)
- }
+ val split_begin =
+ if (before_change.isDefined) {
+ val changed =
+ if (cmd_before_change.isDefined)
+ new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
+ else new_tokenset
+ if (changed.exists(_ == before_change.get))
+ changed.takeWhile(_ != before_change.get).toList :::
+ List(before_change.get)
+ else Nil
+ } else Nil
+ val split_end =
+ if (after_change.isDefined && cmd_after_change.isDefined) {
+ val unchanged = new_tokens.dropWhile(_ != after_change.get)
+ if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
+ unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
+ else Nil
+ } else Nil
+
+ val rescan_begin =
+ split_begin :::
+ before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
val rescanning_tokens =
- split_begin_tokens ::: inserted_tokens ::: split_end_tokens
- val inserted_commands = tokens_to_commands(rescanning_tokens)
+ after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
+ split_end
+ val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList)
// build new document
@@ -209,4 +225,30 @@
new_commandset, active, is_command_keyword)
return (doc, change)
}
+
+ val commands_offsets = {
+ var last_stop = 0
+ (for (c <- commands) yield {
+ val r = c -> (last_stop,c.stop(this))
+ last_stop = c.stop(this)
+ r
+ }).toArray
+ }
+
+ // use a binary search to find commands for a given offset
+ def find_command_at(pos: Int): Command = find_command_at(pos, 0, commands_offsets.length)
+ private def find_command_at(pos: Int, array_start: Int, array_stop: Int): Command = {
+ val middle_index = (array_start + array_stop) / 2
+ if (middle_index >= commands_offsets.length) return null
+ val (middle, (start, stop)) = commands_offsets(middle_index)
+ // does middle contain pos?
+ if (start <= pos && stop > pos)
+ middle
+ else if (start > pos)
+ find_command_at(pos, array_start, middle_index)
+ else if (stop <= pos)
+ find_command_at(pos, middle_index + 1, array_stop)
+ else error("can't be")
+ }
+
}
--- a/src/Tools/jEdit/src/proofdocument/Token.scala Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Tue Jun 02 22:55:20 2009 +0200
@@ -32,6 +32,8 @@
}
class Token(val content: String, val kind: Token.Kind.Value) {
+ import Token.Kind._
val length = content.length
override def toString = content
+ val is_start = kind == COMMAND_START || kind == COMMENT
}
--- a/src/Tools/jEdit/src/prover/Command.scala Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Tue Jun 02 22:55:20 2009 +0200
@@ -43,6 +43,8 @@
def start(doc: ProofDocument) = doc.token_start(tokens.first)
def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
+ def contains(p: Token) = tokens.contains(p)
+
/* command status */
var state_id: IsarDocument.State_ID = null
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 22:55:20 2009 +0200
@@ -125,8 +125,8 @@
}
else this set_children new_children
} else {
- error("ignored nonfitting markup " + new_child.id + new_child.content +
- new_child.info.toString + "(" +new_child.start + ", "+ new_child.stop + ")")
+ System.err.println("ignored nonfitting markup: " + new_child)
+ this
}
}