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. This history is simply a list together with a current pointer. TODO: Use a simple stack rather than a TreeSet to represent the collection; a browser region should simply be a position in a document.

Field Summary

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 just above _current and set _current to refer to r.
void	changeRegion(BrowserDocumentRegion region, Lambda<BrowserDocumentRegion,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()
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	setCurrentRegion(BrowserDocumentRegion r) Set the current region.
void	setMaximumSize(int size) Set the maximum number of regions that can be stored in this manager.

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, toString, wait, wait, wait

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 just above _current and set _current to refer to r. Only runs in event thread after initialization. Notifies regionAdded listeners if _currentIndex is changed. Assumes _regions.isEmpty() || _regions.contains(_current) and _regions.isEmpty() == (_current == null)

Parameters:

r - the DocumentRegion to be inserted into the manager

remove

public void remove(BrowserDocumentRegion r)

Remove the given DocumentRegion from the manager.

Parameters:

r - the DocumentRegion to be removed.

getRegions

public SortedSet<BrowserDocumentRegion> getRegions()

Returns:

an ArrayList 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

setCurrentRegion

public void setCurrentRegion(BrowserDocumentRegion r)

Set the current region.

nextCurrentRegion

public BrowserDocumentRegion nextCurrentRegion(GlobalEventNotifier notifier)

Make the region that is more recent the current region. If _current is null, set it to refer to first.

Returns:

new current region

prevCurrentRegion

public BrowserDocumentRegion prevCurrentRegion(GlobalEventNotifier notifier)

Make the region that is less recent the current region. If _current is null, set it to refer to last.

Returns:

new current region

setMaximumSize

public void setMaximumSize(int size)

Set the maximum number of regions that can be stored in this manager. If the maximum capacity has been reached and another region is added, the region at the end farther away from the insertion location will be discarded.

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,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.