--- a/src/Pure/PIDE/change.scala Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Pure/PIDE/change.scala Thu Aug 05 18:00:37 2010 +0200
@@ -14,11 +14,11 @@
abstract class Snapshot
{
- val latest_version: Change
- val stable_version: Change
val document: Document
val node: Document.Node
- def is_outdated: Boolean = stable_version != latest_version
+ val is_outdated: Boolean
+ def from_current(offset: Int): Int
+ def to_current(offset: Int): Int
}
}
@@ -62,14 +62,22 @@
/* snapshot */
- def snapshot(name: String): Change.Snapshot =
+ def snapshot(name: String, extra_edits: List[Text_Edit]): Change.Snapshot =
{
val latest = this
+ val stable = latest.ancestors.find(_.is_assigned).get
+ val changes =
+ (extra_edits /: latest.ancestors.takeWhile(_ != stable))((edits, change) =>
+ (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+
new Change.Snapshot {
- val latest_version = latest
- val stable_version: Change = latest.ancestors.find(_.is_assigned).get
- val document: Document = stable_version.join_document
- val node: Document.Node = document.nodes(name)
+ val document = stable.join_document
+ val node = document.nodes(name)
+ val is_outdated = !(extra_edits.isEmpty && latest == stable)
+ def from_current(offset: Int): Int =
+ (offset /: changes.reverse)((i, change) => change before i) // FIXME fold_rev (!?)
+ def to_current(offset: Int): Int =
+ (offset /: changes)((i, change) => change after i)
}
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/document_model.scala Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Thu Aug 05 18:00:37 2010 +0200
@@ -70,41 +70,26 @@
}
- /* history */
+ /* global state -- owned by Swing thread */
+
+ @volatile private var history = Change.init // owned by Swing thread
+ private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread
+
+
+ /* snapshot */
// FIXME proper error handling
val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
- @volatile private var history = Change.init // owned by Swing thread
-
- def current_change(): Change = history
- def snapshot(): Change.Snapshot = current_change().snapshot(thy_name)
-
-
- /* transforming offsets */
-
- private def changes_from(doc: Document): List[Text_Edit] =
- {
- Swing_Thread.assert()
- (edits_buffer.toList /:
- current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) =>
- (for ((name, eds) <- change.edits if name == thy_name) yield eds).flatten ::: edits)
- }
-
- def from_current(doc: Document, offset: Int): Int =
- (offset /: changes_from(doc).reverse) ((i, change) => change before i)
-
- def to_current(doc: Document, offset: Int): Int =
- (offset /: changes_from(doc)) ((i, change) => change after i)
+ def snapshot(): Change.Snapshot =
+ Swing_Thread.now { history.snapshot(thy_name, edits_buffer.toList) }
/* text edits */
- private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread
-
private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
if (!edits_buffer.isEmpty) {
- val new_change = current_change().edit(session, List((thy_name, edits_buffer.toList)))
+ val new_change = history.edit(session, List((thy_name, edits_buffer.toList)))
edits_buffer.clear
history = new_change
new_change.result.map(_ => session.input(new_change))
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 05 18:00:37 2010 +0200
@@ -120,16 +120,14 @@
{
Swing_Thread.assert()
- val document = snapshot.document
- val doc = snapshot.node
val buffer = model.buffer
var visible_change = false
- for ((command, start) <- doc.command_starts) {
+ for ((command, start) <- snapshot.node.command_starts) {
if (changed(command)) {
val stop = start + command.length
- val line1 = buffer.getLineOfOffset(model.to_current(document, start))
- val line2 = buffer.getLineOfOffset(model.to_current(document, stop))
+ val line1 = buffer.getLineOfOffset(snapshot.to_current(start))
+ val line2 = buffer.getLineOfOffset(snapshot.to_current(stop))
if (line2 >= text_area.getFirstLine &&
line1 <= text_area.getFirstLine + text_area.getVisibleLines)
visible_change = true
@@ -152,18 +150,14 @@
{
Swing_Thread.now {
val snapshot = model.snapshot()
- val document = snapshot.document
- val doc = snapshot.node
- def from_current(pos: Int) = model.from_current(document, pos)
- def to_current(pos: Int) = model.to_current(document, pos)
val command_range: Iterable[(Command, Int)] =
{
- val range = doc.command_range(from_current(start(0)))
+ val range = snapshot.node.command_range(snapshot.from_current(start(0)))
if (range.hasNext) {
val (cmd0, start0) = range.next
new Iterable[(Command, Int)] {
- def iterator = Document.command_starts(doc.commands.iterator(cmd0), start0)
+ def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
}
}
else Iterable.empty
@@ -177,15 +171,17 @@
val line_start = start(i)
val line_end = model.visible_line_end(line_start, end(i))
- val a = from_current(line_start)
- val b = from_current(line_end)
+ val a = snapshot.from_current(line_start)
+ val b = snapshot.from_current(line_end)
val cmds = command_range.iterator.
dropWhile { case (cmd, c) => c + cmd.length <= a } .
takeWhile { case (_, c) => c < b }
for ((command, command_start) <- cmds if !command.is_ignored) {
- val p = text_area.offsetToXY(line_start max to_current(command_start))
- val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
+ val p = text_area.offsetToXY(
+ line_start max snapshot.to_current(command_start))
+ val q = text_area.offsetToXY(
+ line_end min snapshot.to_current(command_start + command.length))
assert(p.y == q.y)
gfx.setColor(Document_View.choose_color(snapshot, command))
gfx.fillRect(p.x, y, q.x - p.x, line_height)
@@ -201,12 +197,10 @@
override def getToolTipText(x: Int, y: Int): String =
{
val snapshot = model.snapshot()
- val document = snapshot.document
- val doc = snapshot.node
- val offset = model.from_current(document, text_area.xyToOffset(x, y))
- doc.command_at(offset) match {
+ val offset = snapshot.from_current(text_area.xyToOffset(x, y))
+ snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- document.current_state(command).type_at(offset - command_start) match {
+ snapshot.document.current_state(command).type_at(offset - command_start) match {
case Some(text) => Isabelle.tooltip(text)
case None => null
}
@@ -270,12 +264,11 @@
super.paintComponent(gfx)
val buffer = model.buffer
val snapshot = model.snapshot()
- def to_current(pos: Int) = model.to_current(snapshot.document, pos)
val saved_color = gfx.getColor // FIXME needed!?
try {
for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
- val line1 = buffer.getLineOfOffset(to_current(start))
- val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
+ val line1 = buffer.getLineOfOffset(snapshot.to_current(start))
+ val line2 = buffer.getLineOfOffset(snapshot.to_current(start + command.length)) + 1
val y = line_to_y(line1)
val height = HEIGHT * (line2 - line1)
gfx.setColor(Document_View.choose_color(snapshot, command))
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 05 18:00:37 2010 +0200
@@ -43,26 +43,24 @@
Document_Model(buffer) match {
case Some(model) =>
val snapshot = model.snapshot()
- val document = snapshot.document
- val doc = snapshot.node
- val offset = model.from_current(document, original_offset)
- doc.command_at(offset) match {
+ val offset = snapshot.from_current(original_offset)
+ snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- document.current_state(command).ref_at(offset - command_start) match {
+ snapshot.document.current_state(command).ref_at(offset - command_start) match {
case Some(ref) =>
- val begin = model.to_current(document, command_start + ref.start)
+ val begin = snapshot.to_current(command_start + ref.start)
val line = buffer.getLineOfOffset(begin)
- val end = model.to_current(document, command_start + ref.stop)
+ val end = snapshot.to_current(command_start + ref.stop)
ref.info match {
case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
new External_Hyperlink(begin, end, line, ref_file, ref_line)
case Command.RefInfo(_, _, Some(id), Some(offset)) =>
Isabelle.session.lookup_entity(id) match {
case Some(ref_cmd: Command) =>
- doc.command_start(ref_cmd) match {
+ snapshot.node.command_start(ref_cmd) match {
case Some(ref_cmd_start) =>
new Internal_Hyperlink(begin, end, line,
- model.to_current(document, ref_cmd_start + offset - 1))
+ snapshot.to_current(ref_cmd_start + offset - 1))
case None => null // FIXME external ref
}
case _ => null
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 05 18:00:37 2010 +0200
@@ -128,11 +128,9 @@
import Isabelle_Sidekick.int_to_pos
val root = data.root
- val snapshot = model.snapshot()
- val document = snapshot.document
- val doc = snapshot.node // FIXME cover all nodes (!??)
- for ((command, command_start) <- doc.command_range(0) if !stopped) {
- root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
+ val snapshot = model.snapshot() // FIXME cover all nodes (!??)
+ for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
+ root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
{
val content = command.source(node.start, node.stop).replace('\n', ' ')
val id = command.id
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Aug 05 18:00:37 2010 +0200
@@ -152,10 +152,6 @@
val stop = start + line_segment.count
val snapshot = model.snapshot()
- val document = snapshot.document
- val doc = snapshot.node
- def to: Int => Int = model.to_current(document, _)
- def from: Int => Int = model.from_current(document, _)
/* FIXME
for (text_area <- Isabelle.jedit_text_areas(model.buffer)
@@ -168,10 +164,11 @@
var next_x = start
for {
- (command, command_start) <- doc.command_range(from(start), from(stop))
- markup <- document.current_state(command).highlight.flatten
- val abs_start = to(command_start + markup.start)
- val abs_stop = to(command_start + markup.stop)
+ (command, command_start) <-
+ snapshot.node.command_range(snapshot.from_current(start), snapshot.from_current(stop))
+ markup <- snapshot.document.current_state(command).highlight.flatten
+ val abs_start = snapshot.to_current(command_start + markup.start)
+ val abs_stop = snapshot.to_current(command_start + markup.stop)
if (abs_stop > start)
if (abs_start < stop)
val token_start = (abs_start - start) max 0
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Aug 05 18:00:37 2010 +0200
@@ -65,9 +65,9 @@
case Some(doc_view) =>
current_command match {
case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
- val document = doc_view.model.snapshot().document
+ val snapshot = doc_view.model.snapshot()
val filtered_results =
- document.current_state(cmd).results filter {
+ snapshot.document.current_state(cmd).results filter {
case XML.Elem(Markup.TRACING, _, _) => show_tracing
case XML.Elem(Markup.DEBUG, _, _) => show_debug
case _ => true