--- a/src/Tools/jEdit/src/jedit/document_model.scala Fri Jul 02 21:48:54 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sat Jul 03 20:20:13 2010 +0200
@@ -95,14 +95,6 @@
def to_current(doc: Document, offset: Int): Int =
(offset /: changes_from(doc)) ((i, change) => change after i)
- def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
- {
- val start = doc.command_start(cmd).get // FIXME total?
- val stop = start + cmd.length
- (buffer.getLineOfOffset(to_current(doc, start)),
- buffer.getLineOfOffset(to_current(doc, stop)))
- }
-
/* text edits */