src/Tools/jEdit/src/jedit/document_view.scala

     var visible_change = false
 
     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
         text_area.invalidateLineRange(line1, line2)
       }

       Swing_Thread.now {
         val snapshot = model.snapshot()
 
         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)] {
               def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
             }

           for (i <- 0 until physical_lines.length) {
             if (physical_lines(i) != -1) {
               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)
               }
             }

     }
 
     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 {
             case Some(text) => Isabelle.tooltip(text)
             case None => null

       val buffer = model.buffer
       val snapshot = model.snapshot()
       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))
           gfx.fillRect(0, y, getWidth - 1, height)
         }