KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > org > eclipse > jface > text > DocumentPartitioningChangedEvent


1 /*******************************************************************************
2  * Copyright (c) 2000, 2006 IBM Corporation and others.
3  * All rights reserved. This program and the accompanying materials
4  * are made available under the terms of the Eclipse Public License v1.0
5  * which accompanies this distribution, and is available at
6  * http://www.eclipse.org/legal/epl-v10.html
7  *
8  * Contributors:
9  * IBM Corporation - initial API and implementation
10  *******************************************************************************/
11 package org.eclipse.jface.text;
12
13 import java.util.HashMap JavaDoc;
14 import java.util.Iterator JavaDoc;
15 import java.util.Map JavaDoc;
16
17 import org.eclipse.core.runtime.Assert;
18
19 /**
20  * Event describing the change of document partitionings.
21  *
22  * @see org.eclipse.jface.text.IDocumentExtension3
23  * @since 3.0
24  */
25 public class DocumentPartitioningChangedEvent {
26
27     /** The document whose partitionings changed */
28     private final IDocument fDocument;
29     /** The map of partitionings to changed regions. */
30     private final Map JavaDoc fMap= new HashMap JavaDoc();
31
32
33     /**
34      * Creates a new document partitioning changed event for the given document.
35      * Initially this event is empty, i.e. does not describe any change.
36      *
37      * @param document the changed document
38      */
39     public DocumentPartitioningChangedEvent(IDocument document) {
40         fDocument= document;
41     }
42
43     /**
44      * Returns the changed document.
45      *
46      * @return the changed document
47      */
48     public IDocument getDocument() {
49         return fDocument;
50     }
51
52     /**
53      * Returns the changed region of the given partitioning or <code>null</code>
54      * if the given partitioning did not change.
55      *
56      * @param partitioning the partitioning
57      * @return the changed region of the given partitioning or <code>null</code>
58      */
59     public IRegion getChangedRegion(String JavaDoc partitioning) {
60         return (IRegion) fMap.get(partitioning);
61     }
62
63     /**
64      * Returns the set of changed partitionings.
65      *
66      * @return the set of changed partitionings
67      */
68     public String JavaDoc[] getChangedPartitionings() {
69         String JavaDoc[] partitionings= new String JavaDoc[fMap.size()];
70         fMap.keySet().toArray(partitionings);
71         return partitionings;
72     }
73
74     /**
75      * Sets the specified range as changed region for the given partitioning.
76      *
77      * @param partitioning the partitioning
78      * @param offset the region offset
79      * @param length the region length
80      */
81     public void setPartitionChange(String JavaDoc partitioning, int offset, int length) {
82         Assert.isNotNull(partitioning);
83         fMap.put(partitioning, new Region(offset, length));
84     }
85
86     /**
87      * Returns <code>true</code> if the set of changed partitionings is empty,
88      * <code>false</code> otherwise.
89      *
90      * @return <code>true</code> if the set of changed partitionings is empty
91      */
92     public boolean isEmpty() {
93         return fMap.isEmpty();
94     }
95
96     /**
97      * Returns the coverage of this event. This is the minimal region that
98      * contains all changed regions of all changed partitionings.
99      *
100      * @return the coverage of this event
101      */
102     public IRegion getCoverage() {
103         if (fMap.isEmpty())
104             return new Region(0, 0);
105
106         int offset= -1;
107         int endOffset= -1;
108         Iterator JavaDoc e= fMap.values().iterator();
109         while (e.hasNext()) {
110             IRegion r= (IRegion) e.next();
111
112             if (offset < 0 || r.getOffset() < offset)
113                 offset= r.getOffset();
114
115             int end= r.getOffset() + r.getLength();
116             if (end > endOffset)
117                 endOffset= end;
118         }
119
120         return new Region(offset, endOffset - offset);
121     }
122 }
123
Popular Tags