edu.rice.cs.drjava.model
Class BrowserHistoryManager

java.lang.Object
  edu.rice.cs.drjava.model.EventNotifier<RegionManagerListener<BrowserDocumentRegion>>
      edu.rice.cs.drjava.model.BrowserHistoryManager

public class BrowserHistoryManager
extends EventNotifier<RegionManagerListener<BrowserDocumentRegion>>

Browser history manager for the entire model. Follows readers/writers locking protocol of EventNotifier.

Field Summary

private java.util.Stack<BrowserDocumentRegion>	_futureRegions
private int	_maxSize
private java.util.Stack<BrowserDocumentRegion>	_pastRegions List of regions.
static int	DIFF_THRESHOLD Two regions are similar if they are in the same document and not more than DIFF_THRESHOLD lines apart.

Fields inherited from class edu.rice.cs.drjava.model.EventNotifier

_listeners, _lock

Constructor Summary

BrowserHistoryManager()
Create a new ConcreteRegionManager without maximum size.

BrowserHistoryManager(int size)
Create a new ConcreteRegionManager with the specified maximum size.

Method Summary

void	addBrowserRegion(BrowserDocumentRegion r, GlobalEventNotifier notifier) Add the supplied DocumentRegion r to the manager as current region.
void	addBrowserRegionBefore(BrowserDocumentRegion r, GlobalEventNotifier notifier) Add the supplied DocumentRegion r to the manager before the current region.
void	changeRegion(BrowserDocumentRegion region, Lambda<BrowserDocumentRegion,java.lang.Object> cmd) Apply the given command to the specified region to change it.
void	clearBrowserRegions() Tells the manager to remove all regions.
BrowserDocumentRegion	getCurrentRegion()
int	getMaximumSize()
java.util.SortedSet<BrowserDocumentRegion>	getRegions()
boolean	isCurrentRegionFirst()
boolean	isCurrentRegionLast()
BrowserDocumentRegion	nextCurrentRegion(GlobalEventNotifier notifier) Make the region that is more recent the current region.
BrowserDocumentRegion	prevCurrentRegion(GlobalEventNotifier notifier) Make the region that is less recent the current region.
void	remove(BrowserDocumentRegion r) Remove the given DocumentRegion from the manager.
void	setMaximumSize(int size) Set the maximum number of regions that can be stored in this manager.
private void	shrinkManager() Remove regions if there are more than the maximum number allowed.
static boolean	similarRegions(BrowserDocumentRegion r1, BrowserDocumentRegion r2) Return true if the two regions are similar.
java.lang.String	toString()

Methods inherited from class edu.rice.cs.drjava.model.EventNotifier

addListener, removeAllListeners, removeListener

Methods inherited from class java.lang.Object

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

Field Detail

DIFF_THRESHOLD

public static final int DIFF_THRESHOLD

Two regions are similar if they are in the same document and not more than DIFF_THRESHOLD lines apart.

See Also:

Constant Field Values

_pastRegions

private volatile java.util.Stack<BrowserDocumentRegion> _pastRegions

List of regions. In Java 6, ArrayDeque is a better choice than Stack; should be changed once compatibility with Java 5 is abandoned.

_futureRegions

private volatile java.util.Stack<BrowserDocumentRegion> _futureRegions

_maxSize

private volatile int _maxSize

Constructor Detail

BrowserHistoryManager

public BrowserHistoryManager(int size)

Create a new ConcreteRegionManager with the specified maximum size.

Parameters:

size - maximum number of regions that can be stored in this manager.

BrowserHistoryManager

public BrowserHistoryManager()

Create a new ConcreteRegionManager without maximum size.

Method Detail

addBrowserRegion

public void addBrowserRegion(BrowserDocumentRegion r,
                             GlobalEventNotifier notifier)

Add the supplied DocumentRegion r to the manager as current region.

Parameters:

r - the DocumentRegion to be inserted into the manager

addBrowserRegionBefore

public void addBrowserRegionBefore(BrowserDocumentRegion r,
                                   GlobalEventNotifier notifier)

Add the supplied DocumentRegion r to the manager before the current region.

Parameters:

r - the DocumentRegion to be inserted into the manager

shrinkManager

private void shrinkManager()

Remove regions if there are more than the maximum number allowed. Typically used to remove one region.

remove

public void remove(BrowserDocumentRegion r)

Remove the given DocumentRegion from the manager.

Parameters:

r - the DocumentRegion to be removed.

getRegions

public java.util.SortedSet<BrowserDocumentRegion> getRegions()

Returns:

a SortedSet containing the DocumentRegion objects in this mangager.

clearBrowserRegions

public void clearBrowserRegions()

Tells the manager to remove all regions.

getCurrentRegion

public BrowserDocumentRegion getCurrentRegion()

Returns:

the current region or null if none selected

isCurrentRegionFirst

public boolean isCurrentRegionFirst()

Returns:

true if the current region is the first in the list, i.e. prevCurrentRegion is without effect

isCurrentRegionLast

public boolean isCurrentRegionLast()

Returns:

true if the current region is the last in the list, i.e. nextCurrentRegion is without effect

nextCurrentRegion

public BrowserDocumentRegion nextCurrentRegion(GlobalEventNotifier notifier)

Make the region that is more recent the current region.

Returns:

new current region

prevCurrentRegion

public BrowserDocumentRegion prevCurrentRegion(GlobalEventNotifier notifier)

Make the region that is less recent the current region.

Returns:

new current region

setMaximumSize

public void setMaximumSize(int size)

Set the maximum number of regions that can be stored in this manager.

Parameters:

size - maximum number of regions, or 0 if no maximum

getMaximumSize

public int getMaximumSize()

Returns:

the maximum number of regions that can be stored in this manager.

changeRegion

public void changeRegion(BrowserDocumentRegion region,
                         Lambda<BrowserDocumentRegion,java.lang.Object> cmd)

Apply the given command to the specified region to change it.

Parameters:

region - the region to find and change

cmd - command that mutates the region.

similarRegions

public static boolean similarRegions(BrowserDocumentRegion r1,
                                     BrowserDocumentRegion r2)

Return true if the two regions are similar.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object