# HG changeset patch # User wenzelm # Date 1281024792 -7200 # Node ID 469555615ec70a914440c01dca487696e0b7f72b # Parent eab0d1c2e46ed19bc46272119a95e7c134b8aad2 renamed to_current to convert, and from_current to revert; diff -r eab0d1c2e46e -r 469555615ec7 src/Pure/PIDE/change.scala --- 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 diff -r eab0d1c2e46e -r 469555615ec7 src/Tools/jEdit/src/jedit/document_view.scala --- 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)) diff -r eab0d1c2e46e -r 469555615ec7 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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 diff -r eab0d1c2e46e -r 469555615ec7 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- 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