AbstractDocument fix concurrency (BadPositionCategoryException) #1067

By synchronized access to members used from different thread

eclipse-jdt/eclipse.jdt.ui#1067

Author: Jörg Kubitz

bundles/org.eclipse.text/src/org/eclipse/jface/text/AbstractDocument.java

@@ -102,11 +102,12 @@ static private class RegisteredReplace {
 	private final ListenerList<IDocumentListener> fPrenotifiedDocumentListeners= new ListenerList<>(ListenerList.IDENTITY);
 	/** The registered document partitioning listeners */
 	private final ListenerList<IDocumentPartitioningListener> fDocumentPartitioningListeners= new ListenerList<>(ListenerList.IDENTITY);
-	/** All positions managed by the document ordered by their start positions. */
+	/** All positions managed by the document ordered by their start positions.
+	 * synchronized access */
 	private final Map<String, List<Position>> fPositions= new HashMap<>();
 	/**
 	 * All positions managed by the document ordered by their end positions.
-	 * @since 3.4
+	 * synchronized access
 	 */
 	private final Map<String, List<Position>> fEndPositions= new HashMap<>();
 	/** All registered document position updaters */
@@ -242,15 +243,6 @@ protected List<IDocumentPartitioningListener> getDocumentPartitioningListeners()
 		return asList(fDocumentPartitioningListeners);
 	}
 
-	/**
-	 * Returns all positions managed by the document grouped by category.
-	 *
-	 * @return the document's positions
-	 */
-	protected Map<String, List<Position>> getDocumentManagedPositions() {
-		return fPositions;
-	}
-
 	@Override
 	public IDocumentPartitioner getDocumentPartitioner() {
 		return getDocumentPartitioner(DEFAULT_PARTITIONING);
@@ -335,7 +327,7 @@ public void removeDocumentPartitioningListener(IDocumentPartitioningListener lis
 	}
 
 	@Override
-	public void addPosition(String category, Position position) throws BadLocationException, BadPositionCategoryException  {
+	synchronized public void addPosition(String category, Position position) throws BadLocationException, BadPositionCategoryException  {
 
 		if ((0 > position.offset) || (0 > position.length) || (position.offset + position.length > getLength()))
 			throw new BadLocationException();
@@ -345,12 +337,12 @@ public void addPosition(String category, Position position) throws BadLocationEx
 
 		List<Position> list= fPositions.get(category);
 		if (list == null)
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 		list.add(computeIndexInPositionList(list, position.offset), position);
 
 		List<Position> endPositions= fEndPositions.get(category);
 		if (endPositions == null)
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 		endPositions.add(computeIndexInPositionList(endPositions, position.offset + position.length - 1, false), position);
 	}
 
@@ -363,7 +355,7 @@ public void addPosition(Position position) throws BadLocationException {
 	}
 
 	@Override
-	public void addPositionCategory(String category) {
+	synchronized public void addPositionCategory(String category) {
 
 		if (category == null)
 			return;
@@ -380,7 +372,7 @@ public void addPositionUpdater(IPositionUpdater updater) {
 	}
 
 	@Override
-	public boolean containsPosition(String category, int offset, int length) {
+	synchronized public boolean containsPosition(String category, int offset, int length) {
 
 		if (category == null)
 			return false;
@@ -408,7 +400,7 @@ public boolean containsPosition(String category, int offset, int length) {
 	}
 
 	@Override
-	public boolean containsPositionCategory(String category) {
+	synchronized public boolean containsPositionCategory(String category) {
 		if (category != null)
 			return fPositions.containsKey(category);
 		return false;
@@ -507,14 +499,14 @@ private int getOffset(boolean orderedByOffset, Position position) {
 	}
 
 	@Override
-	public int computeIndexInCategory(String category, int offset) throws BadLocationException, BadPositionCategoryException {
+	synchronized public int computeIndexInCategory(String category, int offset) throws BadLocationException, BadPositionCategoryException {
 
 		if (0 > offset || offset > getLength())
 			throw new BadLocationException();
 
 		List<Position> c= fPositions.get(category);
 		if (c == null)
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 
 		return computeIndexInPositionList(c, offset);
 	}
@@ -647,7 +639,7 @@ protected void fireDocumentAboutToBeChanged(DocumentEvent event) {
 	 *
 	 * @param event the document event describing the change to which structures must be adapted
 	 */
-	protected void updateDocumentStructures(DocumentEvent event) {
+	synchronized protected void updateDocumentStructures(DocumentEvent event) {
 
 		if (fDocumentPartitioners != null) {
 			fDocumentPartitioningChangedEvent= new DocumentPartitioningChangedEvent(this);
@@ -918,22 +910,22 @@ public ITypedRegion[] computePartitioning(int offset, int length) throws BadLoca
 	}
 
 	@Override
-	public Position[] getPositions(String category) throws BadPositionCategoryException {
+	synchronized public Position[] getPositions(String category) throws BadPositionCategoryException {
 
 		if (category == null)
 			throw new BadPositionCategoryException();
 
 		List<Position> c= fPositions.get(category);
 		if (c == null)
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 
 		Position[] positions= new Position[c.size()];
 		c.toArray(positions);
 		return positions;
 	}
 
 	@Override
-	public String[] getPositionCategories() {
+	synchronized public String[] getPositionCategories() {
 		String[] categories= new String[fPositions.size()];
 		Iterator<String> keys= fPositions.keySet().iterator();
 		for (int i= 0; i < categories.length; i++)
@@ -970,7 +962,7 @@ public void insertPositionUpdater(IPositionUpdater updater, int index) {
 	}
 
 	@Override
-	public void removePosition(String category, Position position) throws BadPositionCategoryException {
+	synchronized public void removePosition(String category, Position position) throws BadPositionCategoryException {
 
 		if (position == null)
 			return;
@@ -980,12 +972,12 @@ public void removePosition(String category, Position position) throws BadPositio
 
 		List<Position> c= fPositions.get(category);
 		if (c == null)
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 		removeFromPositionsList(c, position, true);
 
 		List<Position> endPositions= fEndPositions.get(category);
 		if (endPositions == null)
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 		removeFromPositionsList(endPositions, position, false);
 	}
 
@@ -1037,13 +1029,13 @@ public void removePosition(Position position) {
 	}
 
 	@Override
-	public void removePositionCategory(String category) throws BadPositionCategoryException {
+	synchronized public void removePositionCategory(String category) throws BadPositionCategoryException {
 
 		if (category == null)
 			return;
 
 		if ( !containsPositionCategory(category))
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 
 		fPositions.remove(category);
 		fEndPositions.remove(category);
@@ -1649,10 +1641,10 @@ private boolean isWithinRegion(Position region, Position position, boolean canSt
 	 * @throws BadPositionCategoryException if category is undefined in this document
 	 * @since 3.4
 	 */
-	private List<Position> getStartingPositions(String category, int offset, int length) throws BadPositionCategoryException {
+	synchronized private List<Position> getStartingPositions(String category, int offset, int length) throws BadPositionCategoryException {
 		List<Position> positions= fPositions.get(category);
 		if (positions == null)
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 
 		int indexStart= computeIndexInPositionList(positions, offset, true);
 		int indexEnd= computeIndexInPositionList(positions, offset + length, true);
@@ -1671,10 +1663,10 @@ private List<Position> getStartingPositions(String category, int offset, int len
 	 * @throws BadPositionCategoryException if category is undefined in this document
 	 * @since 3.4
 	 */
-	private List<Position> getEndingPositions(String category, int offset, int length) throws BadPositionCategoryException {
+	synchronized private List<Position> getEndingPositions(String category, int offset, int length) throws BadPositionCategoryException {
 		List<Position> positions= fEndPositions.get(category);
 		if (positions == null)
-			throw new BadPositionCategoryException();
+			throw new BadPositionCategoryException(category);
 
 		int indexStart= computeIndexInPositionList(positions, offset, false);
 		int indexEnd= computeIndexInPositionList(positions, offset + length, false);