org.gjt.sp.jedit.buffer
Class PositionManager

java.lang.Object
  org.gjt.sp.jedit.buffer.PositionManager

public class PositionManager

extends java.lang.Object

A class internal to jEdit's document model. You should not use it directly.

Since:

jEdit 4.2pre3

Version:

$Id: PositionManager.java,v 1.35 2003/11/18 20:51:57 spestov Exp $

Author:

Slava Pestov

Constructor Summary

PositionManager()

Method Summary

void	contentInserted(int offset, int length)
void	contentRemoved(int offset, int length)
javax.swing.text.Position	createPosition(int offset)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

PositionManager

public PositionManager()

Method Detail

createPosition

public javax.swing.text.Position createPosition(int offset)

contentInserted

public void contentInserted(int offset,
                            int length)

contentRemoved

public void contentRemoved(int offset,
                           int length)