--- a/src/Pure/PIDE/change.scala Thu Aug 05 18:00:37 2010 +0200
+++ b/src/Pure/PIDE/change.scala Thu Aug 05 18:13:12 2010 +0200
@@ -17,8 +17,8 @@
val document: Document
val node: Document.Node
val is_outdated: Boolean
- def from_current(offset: Int): Int
- def to_current(offset: Int): Int
+ def convert(offset: Int): Int
+ def revert(offset: Int): Int
}
}
@@ -74,10 +74,8 @@
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)
+ def convert(offset: Int): Int = (offset /: changes)((i, change) => change after i)
+ def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change before i) // FIXME fold_rev (!?)
}
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 05 18:00:37 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 05 18:13:12 2010 +0200
@@ -126,8 +126,8 @@
for ((command, start) <- snapshot.node.command_starts) {
if (changed(command)) {
val stop = start + command.length
- val line1 = buffer.getLineOfOffset(snapshot.to_current(start))
- val line2 = buffer.getLineOfOffset(snapshot.to_current(stop))
+ val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+ val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
if (line2 >= text_area.getFirstLine &&
line1 <= text_area.getFirstLine + text_area.getVisibleLines)
visible_change = true
@@ -153,7 +153,7 @@
val command_range: Iterable[(Command, Int)] =
{
- val range = snapshot.node.command_range(snapshot.from_current(start(0)))
+ val range = snapshot.node.command_range(snapshot.revert(start(0)))
if (range.hasNext) {
val (cmd0, start0) = range.next
new Iterable[(Command, Int)] {
@@ -171,17 +171,17 @@
val line_start = start(i)
val line_end = model.visible_line_end(line_start, end(i))
- val a = snapshot.from_current(line_start)
- val b = snapshot.from_current(line_end)
+ val a = snapshot.revert(line_start)
+ val b = snapshot.revert(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 snapshot.to_current(command_start))
- val q = text_area.offsetToXY(
- line_end min snapshot.to_current(command_start + command.length))
+ val p =
+ text_area.offsetToXY(line_start max snapshot.convert(command_start))
+ val q =
+ text_area.offsetToXY(line_end min snapshot.convert(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)
@@ -197,7 +197,7 @@
override def getToolTipText(x: Int, y: Int): String =
{
val snapshot = model.snapshot()
- val offset = snapshot.from_current(text_area.xyToOffset(x, y))
+ val offset = snapshot.revert(text_area.xyToOffset(x, y))
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
snapshot.document.current_state(command).type_at(offset - command_start) match {
@@ -267,8 +267,8 @@
val saved_color = gfx.getColor // FIXME needed!?
try {
for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
- val line1 = buffer.getLineOfOffset(snapshot.to_current(start))
- val line2 = buffer.getLineOfOffset(snapshot.to_current(start + command.length)) + 1
+ val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+ val line2 = buffer.getLineOfOffset(snapshot.convert(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 18:00:37 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 05 18:13:12 2010 +0200
@@ -43,14 +43,14 @@
Document_Model(buffer) match {
case Some(model) =>
val snapshot = model.snapshot()
- val offset = snapshot.from_current(original_offset)
+ val offset = snapshot.revert(original_offset)
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
snapshot.document.current_state(command).ref_at(offset - command_start) match {
case Some(ref) =>
- val begin = snapshot.to_current(command_start + ref.start)
+ val begin = snapshot.convert(command_start + ref.start)
val line = buffer.getLineOfOffset(begin)
- val end = snapshot.to_current(command_start + ref.stop)
+ val end = snapshot.convert(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)
@@ -60,7 +60,7 @@
snapshot.node.command_start(ref_cmd) match {
case Some(ref_cmd_start) =>
new Internal_Hyperlink(begin, end, line,
- snapshot.to_current(ref_cmd_start + offset - 1))
+ snapshot.convert(ref_cmd_start + offset - 1))
case None => null // FIXME external ref
}
case _ => null
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Aug 05 18:00:37 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Aug 05 18:13:12 2010 +0200
@@ -165,10 +165,10 @@
var next_x = start
for {
(command, command_start) <-
- snapshot.node.command_range(snapshot.from_current(start), snapshot.from_current(stop))
+ snapshot.node.command_range(snapshot.revert(start), snapshot.revert(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)
+ val abs_start = snapshot.convert(command_start + markup.start)
+ val abs_stop = snapshot.convert(command_start + markup.stop)
if (abs_stop > start)
if (abs_start < stop)
val token_start = (abs_start - start) max 0