if (textEditor != null) {
// If a line number was given, go to it
if (offset >= 0) {
- IDocument document = textEditor.getDocumentProvider()
- .getDocument(textEditor.getEditorInput());
+// IDocument document = textEditor.getDocumentProvider()
+// .getDocument(textEditor.getEditorInput());
textEditor.selectAndReveal(offset, length);
}
}