001: /*
002: * DisplayManager.java - Low-level text display
003: * :tabSize=8:indentSize=8:noTabs=false:
004: * :folding=explicit:collapseFolds=1:
005: *
006: * Copyright (C) 2001, 2005 Slava Pestov
007: *
008: * This program is free software; you can redistribute it and/or
009: * modify it under the terms of the GNU General Public License
010: * as published by the Free Software Foundation; either version 2
011: * of the License, or any later version.
012: *
013: * This program is distributed in the hope that it will be useful,
014: * but WITHOUT ANY WARRANTY; without even the implied warranty of
015: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
016: * GNU General Public License for more details.
017: *
018: * You should have received a copy of the GNU General Public License
019: * along with this program; if not, write to the Free Software
020: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
021: */
022:
023: package org.gjt.sp.jedit.textarea;
024:
025: //{{{ Imports
026: import java.awt.Toolkit;
027: import java.util.*;
028: import org.gjt.sp.jedit.buffer.*;
029: import org.gjt.sp.jedit.Debug;
030: import org.gjt.sp.util.Log;
031:
032: //}}}
033:
034: /**
035: * Manages low-level text display tasks, such as folding.
036: *
037: * @since jEdit 4.2pre1
038: * @author Slava Pestov
039: * @version $Id: DisplayManager.java 10273 2007-08-01 21:20:45Z kpouer $
040: */
041: public class DisplayManager {
042: //{{{ Static part
043:
044: //{{{ getDisplayManager() method
045: static DisplayManager getDisplayManager(JEditBuffer buffer,
046: TextArea textArea) {
047: List<DisplayManager> l = bufferMap.get(buffer);
048: if (l == null) {
049: l = new LinkedList<DisplayManager>();
050: bufferMap.put(buffer, l);
051: }
052:
053: /* An existing display manager's fold visibility map
054: that a new display manager will inherit */
055: DisplayManager copy = null;
056: Iterator<DisplayManager> liter = l.iterator();
057: DisplayManager dmgr;
058: while (liter.hasNext()) {
059: dmgr = liter.next();
060: copy = dmgr;
061: if (!dmgr.inUse && dmgr.textArea == textArea) {
062: dmgr.inUse = true;
063: return dmgr;
064: }
065: }
066:
067: // if we got here, no unused display manager in list
068: dmgr = new DisplayManager(buffer, textArea, copy);
069: dmgr.inUse = true;
070: l.add(dmgr);
071:
072: return dmgr;
073: } //}}}
074:
075: //{{{ releaseDisplayManager() method
076: static void releaseDisplayManager(DisplayManager dmgr) {
077: dmgr.inUse = false;
078: } //}}}
079:
080: //{{{ bufferClosed() method
081: public static void bufferClosed(JEditBuffer buffer) {
082: bufferMap.remove(buffer);
083: } //}}}
084:
085: //{{{ textAreaDisposed() method
086: static void textAreaDisposed(TextArea textArea) {
087: for (List<DisplayManager> l : bufferMap.values()) {
088: Iterator<DisplayManager> liter = l.iterator();
089: while (liter.hasNext()) {
090: DisplayManager dmgr = liter.next();
091: if (dmgr.textArea == textArea) {
092: dmgr.dispose();
093: liter.remove();
094: }
095: }
096: }
097: } //}}}
098:
099: private static final Map<JEditBuffer, List<DisplayManager>> bufferMap = new HashMap<JEditBuffer, List<DisplayManager>>();
100:
101: //}}}
102:
103: //{{{ getBuffer() method
104: /**
105: * @since jEdit 4.3pre3
106: */
107: public JEditBuffer getBuffer() {
108: return buffer;
109: } //}}}
110:
111: //{{{ isLineVisible() method
112: /**
113: * Returns if the specified line is visible.
114: * @param line A physical line index
115: * @since jEdit 4.2pre1
116: */
117: public final boolean isLineVisible(int line) {
118: return folds.search(line) % 2 == 0;
119: } //}}}
120:
121: //{{{ getFirstVisibleLine() method
122: /**
123: * Returns the physical line number of the first visible line.
124: * @since jEdit 4.2pre1
125: */
126: public int getFirstVisibleLine() {
127: return folds.first();
128: } //}}}
129:
130: //{{{ getLastVisibleLine() method
131: /**
132: * Returns the physical line number of the last visible line.
133: * @since jEdit 4.2pre1
134: */
135: public int getLastVisibleLine() {
136: return folds.last();
137: } //}}}
138:
139: //{{{ getNextVisibleLine() method
140: /**
141: * Returns the next visible line after the specified line index.
142: * @param line A physical line index
143: * @since jEdit 4.0pre1
144: */
145: public int getNextVisibleLine(int line) {
146: if (line < 0 || line >= buffer.getLineCount())
147: throw new ArrayIndexOutOfBoundsException(line);
148:
149: return folds.next(line);
150: } //}}}
151:
152: //{{{ getPrevVisibleLine() method
153: /**
154: * Returns the previous visible line before the specified line index.
155: * @param line a physical line index
156: * @return the previous visible physical line or -1 if there is no visible line
157: * @since jEdit 4.0pre1
158: */
159: public int getPrevVisibleLine(int line) {
160: if (line < 0 || line >= buffer.getLineCount())
161: throw new ArrayIndexOutOfBoundsException(line);
162:
163: return folds.prev(line);
164: } //}}}
165:
166: //{{{ getScreenLineCount() method
167: /**
168: * Returns how many screen lines contains the given physical line.
169: * It can be greater than 1 when using soft wrap
170: *
171: * @param line the physical line
172: * @return the screen line count
173: */
174: public final int getScreenLineCount(int line) {
175: if (!screenLineMgr.isScreenLineCountValid(line))
176: throw new RuntimeException("Invalid screen line count: "
177: + line);
178:
179: return screenLineMgr.getScreenLineCount(line);
180: } //}}}
181:
182: //{{{ getScrollLineCount() method
183: public final int getScrollLineCount() {
184: return scrollLineCount.scrollLine;
185: } //}}}
186:
187: //{{{ collapseFold() method
188: /**
189: * Collapses the fold at the specified physical line index.
190: * @param line A physical line index
191: * @since jEdit 4.2pre1
192: */
193: public void collapseFold(int line) {
194: int lineCount = buffer.getLineCount();
195: int start = 0;
196: int end = lineCount - 1;
197:
198: // if the caret is on a collapsed fold, collapse the
199: // parent fold
200: if (line != 0 && line != buffer.getLineCount() - 1
201: && buffer.isFoldStart(line) && !isLineVisible(line + 1)) {
202: line--;
203: }
204:
205: int initialFoldLevel = buffer.getFoldLevel(line);
206:
207: //{{{ Find fold start and end...
208: if (line != lineCount - 1
209: && buffer.getFoldLevel(line + 1) > initialFoldLevel) {
210: // this line is the start of a fold
211: start = line + 1;
212:
213: for (int i = line + 1; i < lineCount; i++) {
214: if (buffer.getFoldLevel(i) <= initialFoldLevel) {
215: end = i - 1;
216: break;
217: }
218: }
219: } else {
220: boolean ok = false;
221:
222: // scan backwards looking for the start
223: for (int i = line - 1; i >= 0; i--) {
224: if (buffer.getFoldLevel(i) < initialFoldLevel) {
225: start = i + 1;
226: ok = true;
227: break;
228: }
229: }
230:
231: if (!ok) {
232: // no folds in buffer
233: return;
234: }
235:
236: for (int i = line + 1; i < lineCount; i++) {
237: if (buffer.getFoldLevel(i) < initialFoldLevel) {
238: end = i - 1;
239: break;
240: }
241: }
242: } //}}}
243:
244: // Collapse the fold...
245: hideLineRange(start, end);
246:
247: notifyScreenLineChanges();
248: textArea.foldStructureChanged();
249: } //}}}
250:
251: //{{{ expandFold() method
252: /**
253: * Expands the fold at the specified physical line index.
254: * @param line A physical line index
255: * @param fully If true, all subfolds will also be expanded
256: * @since jEdit 4.2pre1
257: */
258: public int expandFold(int line, boolean fully) {
259: // the first sub-fold. used by JEditTextArea.expandFold().
260: int returnValue = -1;
261:
262: int lineCount = buffer.getLineCount();
263: int start = 0;
264: int end = lineCount - 1;
265:
266: int initialFoldLevel = buffer.getFoldLevel(line);
267:
268: //{{{ Find fold start and fold end...
269: if (line != lineCount - 1 && isLineVisible(line)
270: && !isLineVisible(line + 1)
271: && buffer.getFoldLevel(line + 1) > initialFoldLevel) {
272: // this line is the start of a fold
273:
274: int index = folds.search(line + 1);
275: if (index == -1) {
276: expandAllFolds();
277: return -1;
278: }
279:
280: start = folds.lookup(index);
281: if (index != folds.count() - 1)
282: end = folds.lookup(index + 1) - 1;
283: else {
284: start = line + 1;
285:
286: for (int i = line + 1; i < lineCount; i++) {
287: if (/* isLineVisible(i) && */
288: buffer.getFoldLevel(i) <= initialFoldLevel) {
289: end = i - 1;
290: break;
291: }
292: }
293: }
294: } else {
295: int index = folds.search(line);
296: if (index == -1) {
297: expandAllFolds();
298: return -1;
299: }
300:
301: start = folds.lookup(index);
302: if (index != folds.count() - 1)
303: end = folds.lookup(index + 1) - 1;
304: else {
305: for (int i = line + 1; i < lineCount; i++) {
306: //XXX
307: if ((isLineVisible(i) && buffer.getFoldLevel(i) < initialFoldLevel)
308: || i == getLastVisibleLine()) {
309: end = i - 1;
310: break;
311: }
312: }
313: }
314: } //}}}
315:
316: //{{{ Expand the fold...
317: if (fully) {
318: showLineRange(start, end);
319: } else {
320: // we need a different value of initialFoldLevel here!
321: initialFoldLevel = buffer.getFoldLevel(start);
322:
323: int firstVisible = start;
324:
325: for (int i = start; i <= end; i++) {
326: if (buffer.getFoldLevel(i) > initialFoldLevel) {
327: if (returnValue == -1 && i != 0
328: && buffer.isFoldStart(i - 1)) {
329: returnValue = i - 1;
330: }
331:
332: if (firstVisible != i) {
333: showLineRange(firstVisible, i - 1);
334: }
335: firstVisible = i + 1;
336: }
337: }
338:
339: if (firstVisible == end + 1)
340: returnValue = -1;
341: else
342: showLineRange(firstVisible, end);
343:
344: if (!isLineVisible(line)) {
345: // this is a hack, and really needs to be done better.
346: expandFold(line, false);
347: return returnValue;
348: }
349: } //}}}
350:
351: notifyScreenLineChanges();
352: textArea.foldStructureChanged();
353:
354: return returnValue;
355: } //}}}
356:
357: //{{{ expandAllFolds() method
358: /**
359: * Expands all folds.
360: * @since jEdit 4.2pre1
361: */
362: public void expandAllFolds() {
363: showLineRange(0, buffer.getLineCount() - 1);
364: notifyScreenLineChanges();
365: textArea.foldStructureChanged();
366: } //}}}
367:
368: //{{{ expandFolds() method
369: /**
370: * This method should only be called from <code>actions.xml</code>.
371: * @since jEdit 4.2pre1
372: */
373: public void expandFolds(char digit) {
374: if (digit < '1' || digit > '9') {
375: Toolkit.getDefaultToolkit().beep();
376: } else
377: expandFolds((digit - '1') + 1);
378: } //}}}
379:
380: //{{{ expandFolds() method
381: /**
382: * Expands all folds with the specified fold level.
383: * @param foldLevel The fold level
384: * @since jEdit 4.2pre1
385: */
386: public void expandFolds(int foldLevel) {
387: if (buffer.getFoldHandler() instanceof IndentFoldHandler)
388: foldLevel = (foldLevel - 1) * buffer.getIndentSize() + 1;
389:
390: showLineRange(0, buffer.getLineCount() - 1);
391:
392: /* this ensures that the first line is always visible */
393: boolean seenVisibleLine = false;
394:
395: int firstInvisible = 0;
396:
397: for (int i = 0; i < buffer.getLineCount(); i++) {
398: if (!seenVisibleLine || buffer.getFoldLevel(i) < foldLevel) {
399: if (firstInvisible != i) {
400: hideLineRange(firstInvisible, i - 1);
401: }
402: firstInvisible = i + 1;
403: seenVisibleLine = true;
404: }
405: }
406:
407: if (firstInvisible != buffer.getLineCount())
408: hideLineRange(firstInvisible, buffer.getLineCount() - 1);
409:
410: notifyScreenLineChanges();
411: textArea.foldStructureChanged();
412: } //}}}
413:
414: //{{{ narrow() method
415: /**
416: * Narrows the visible portion of the buffer to the specified
417: * line range.
418: * @param start The first line
419: * @param end The last line
420: * @since jEdit 4.2pre1
421: */
422: public void narrow(int start, int end) {
423: if (start > end || start < 0 || end >= buffer.getLineCount())
424: throw new ArrayIndexOutOfBoundsException(start + ", " + end);
425:
426: if (start < getFirstVisibleLine() || end > getLastVisibleLine())
427: expandAllFolds();
428:
429: if (start != 0)
430: hideLineRange(0, start - 1);
431: if (end != buffer.getLineCount() - 1)
432: hideLineRange(end + 1, buffer.getLineCount() - 1);
433:
434: // if we narrowed to a single collapsed fold
435: if (start != buffer.getLineCount() - 1
436: && !isLineVisible(start + 1))
437: expandFold(start, false);
438:
439: textArea.fireNarrowActive();
440:
441: notifyScreenLineChanges();
442: textArea.foldStructureChanged();
443: } //}}}
444:
445: //{{{ Package-private members
446: final FirstLine firstLine;
447: final ScrollLineCount scrollLineCount;
448: final ScreenLineManager screenLineMgr;
449: RangeMap folds;
450:
451: //{{{ init() method
452: void init() {
453: if (initialized) {
454: if (!buffer.isLoading())
455: resetAnchors();
456: } else {
457: initialized = true;
458: folds = new RangeMap();
459: if (buffer.isLoading())
460: folds.reset(buffer.getLineCount());
461: else
462: bufferHandler.foldHandlerChanged(buffer);
463: notifyScreenLineChanges();
464: }
465: } //}}}
466:
467: //{{{ notifyScreenLineChanges() method
468: void notifyScreenLineChanges() {
469: if (Debug.SCROLL_DEBUG)
470: Log.log(Log.DEBUG, this , "notifyScreenLineChanges()");
471:
472: // when the text area switches to us, it will do
473: // a reset anyway
474: if (textArea.getDisplayManager() != this )
475: return;
476:
477: try {
478: if (firstLine.callReset)
479: firstLine.reset();
480: else if (firstLine.callChanged)
481: firstLine.changed();
482:
483: if (scrollLineCount.callReset) {
484: scrollLineCount.reset();
485: firstLine.ensurePhysicalLineIsVisible();
486: } else if (scrollLineCount.callChanged)
487: scrollLineCount.changed();
488:
489: if (firstLine.callChanged || scrollLineCount.callReset
490: || scrollLineCount.callChanged) {
491: textArea.updateScrollBar();
492: textArea.recalculateLastPhysicalLine();
493: }
494: } finally {
495: firstLine.callReset = firstLine.callChanged = false;
496: scrollLineCount.callReset = scrollLineCount.callChanged = false;
497: }
498: } //}}}
499:
500: //{{{ setFirstLine() method
501: void setFirstLine(int oldFirstLine, int firstLine) {
502: int visibleLines = textArea.getVisibleLines();
503:
504: if (firstLine >= oldFirstLine + visibleLines) {
505: this .firstLine.scrollDown(firstLine - oldFirstLine);
506: textArea.chunkCache.invalidateAll();
507: } else if (firstLine <= oldFirstLine - visibleLines) {
508: this .firstLine.scrollUp(oldFirstLine - firstLine);
509: textArea.chunkCache.invalidateAll();
510: } else if (firstLine > oldFirstLine) {
511: this .firstLine.scrollDown(firstLine - oldFirstLine);
512: textArea.chunkCache.scrollDown(firstLine - oldFirstLine);
513: } else if (firstLine < oldFirstLine) {
514: this .firstLine.scrollUp(oldFirstLine - firstLine);
515: textArea.chunkCache.scrollUp(oldFirstLine - firstLine);
516: }
517:
518: notifyScreenLineChanges();
519: } //}}}
520:
521: //{{{ setFirstPhysicalLine() method
522: void setFirstPhysicalLine(int amount, int skew) {
523: int oldFirstLine = textArea.getFirstLine();
524:
525: if (amount == 0) {
526: skew -= this .firstLine.skew;
527:
528: // JEditTextArea.scrollTo() needs this to simplify
529: // its code
530: if (skew < 0)
531: this .firstLine.scrollUp(-skew);
532: else if (skew > 0)
533: this .firstLine.scrollDown(skew);
534: else {
535: // nothing to do
536: return;
537: }
538: } else if (amount > 0)
539: this .firstLine.physDown(amount, skew);
540: else if (amount < 0)
541: this .firstLine.physUp(-amount, skew);
542:
543: int firstLine = textArea.getFirstLine();
544: int visibleLines = textArea.getVisibleLines();
545:
546: if (firstLine == oldFirstLine)
547: /* do nothing */;
548: else if (firstLine >= oldFirstLine + visibleLines
549: || firstLine <= oldFirstLine - visibleLines) {
550: textArea.chunkCache.invalidateAll();
551: } else if (firstLine > oldFirstLine) {
552: textArea.chunkCache.scrollDown(firstLine - oldFirstLine);
553: } else if (firstLine < oldFirstLine) {
554: textArea.chunkCache.scrollUp(oldFirstLine - firstLine);
555: }
556:
557: // we have to be careful
558: notifyScreenLineChanges();
559: } //}}}
560:
561: //{{{ invalidateScreenLineCounts() method
562: void invalidateScreenLineCounts() {
563: screenLineMgr.invalidateScreenLineCounts();
564: firstLine.callReset = true;
565: scrollLineCount.callReset = true;
566: } //}}}
567:
568: //{{{ updateScreenLineCount() method
569: void updateScreenLineCount(int line) {
570: if (!screenLineMgr.isScreenLineCountValid(line)) {
571: int newCount = textArea.chunkCache
572: .getLineSubregionCount(line);
573:
574: setScreenLineCount(line, newCount);
575: }
576: } //}}}
577:
578: //{{{ bufferLoaded() method
579: void bufferLoaded() {
580: folds.reset(buffer.getLineCount());
581: screenLineMgr.reset();
582:
583: if (textArea.getDisplayManager() == this ) {
584: textArea.propertiesChanged();
585: init();
586: }
587:
588: int collapseFolds = buffer.getIntegerProperty("collapseFolds",
589: 0);
590: if (collapseFolds != 0)
591: expandFolds(collapseFolds);
592: } //}}}
593:
594: //{{{ foldHandlerChanged() method
595: void foldHandlerChanged() {
596: if (buffer.isLoading())
597: return;
598:
599: folds.reset(buffer.getLineCount());
600: resetAnchors();
601:
602: int collapseFolds = buffer.getIntegerProperty("collapseFolds",
603: 0);
604: if (collapseFolds != 0)
605: expandFolds(collapseFolds);
606: } //}}}
607:
608: //}}}
609:
610: //{{{ Private members
611: private boolean initialized;
612: private boolean inUse;
613: private JEditBuffer buffer;
614: private TextArea textArea;
615: private BufferHandler bufferHandler;
616:
617: //{{{ DisplayManager constructor
618: private DisplayManager(JEditBuffer buffer, TextArea textArea,
619: DisplayManager copy) {
620: this .buffer = buffer;
621: this .screenLineMgr = new ScreenLineManager(buffer);
622: this .textArea = textArea;
623:
624: scrollLineCount = new ScrollLineCount(this , textArea);
625: firstLine = new FirstLine(this , textArea);
626:
627: bufferHandler = new BufferHandler(this , textArea, buffer);
628: // this listener priority thing is a bad hack...
629: buffer.addBufferListener(bufferHandler,
630: JEditBuffer.HIGH_PRIORITY);
631:
632: if (copy != null) {
633: folds = new RangeMap(copy.folds);
634: initialized = true;
635: }
636: } //}}}
637:
638: //{{{ resetAnchors() method
639: private void resetAnchors() {
640: firstLine.callReset = true;
641: scrollLineCount.callReset = true;
642: notifyScreenLineChanges();
643: } //}}}
644:
645: //{{{ dispose() method
646: private void dispose() {
647: buffer.removeBufferListener(bufferHandler);
648: } //}}}
649:
650: //{{{ showLineRange() method
651: private void showLineRange(int start, int end) {
652: if (Debug.FOLD_VIS_DEBUG) {
653: Log.log(Log.DEBUG, this , "showLineRange(" + start + ','
654: + end + ')');
655: }
656:
657: for (int i = start; i <= end; i++) {
658: //XXX
659: if (!isLineVisible(i)) {
660: // important: not screenLineMgr.getScreenLineCount()
661: updateScreenLineCount(i);
662: int screenLines = getScreenLineCount(i);
663: if (firstLine.physicalLine >= i) {
664: firstLine.scrollLine += screenLines;
665: firstLine.callChanged = true;
666: }
667: scrollLineCount.scrollLine += screenLines;
668: scrollLineCount.callChanged = true;
669: }
670: }
671:
672: /* update fold visibility map. */
673: folds.show(start, end);
674: } //}}}
675:
676: //{{{ hideLineRange() method
677: private void hideLineRange(int start, int end) {
678: if (Debug.FOLD_VIS_DEBUG) {
679: Log.log(Log.DEBUG, this , "hideLineRange(" + start + ','
680: + end + ')');
681: }
682:
683: int i = start;
684: if (!isLineVisible(i))
685: i = getNextVisibleLine(i);
686: while (i != -1 && i <= end) {
687: int screenLines = screenLineMgr.getScreenLineCount(i);
688: if (i < firstLine.physicalLine) {
689: firstLine.scrollLine -= screenLines;
690: firstLine.skew = 0;
691: firstLine.callChanged = true;
692: }
693:
694: scrollLineCount.scrollLine -= screenLines;
695: scrollLineCount.callChanged = true;
696:
697: i = getNextVisibleLine(i);
698: }
699:
700: /* update fold visibility map. */
701: folds.hide(start, end);
702:
703: if (!isLineVisible(firstLine.physicalLine)) {
704: int firstVisible = getFirstVisibleLine();
705: if (firstLine.physicalLine < firstVisible) {
706: firstLine.physicalLine = firstVisible;
707: firstLine.scrollLine = 0;
708: } else {
709: firstLine.physicalLine = getPrevVisibleLine(firstLine.physicalLine);
710: firstLine.scrollLine -= screenLineMgr
711: .getScreenLineCount(firstLine.physicalLine);
712: }
713: firstLine.callChanged = true;
714: }
715: } //}}}
716:
717: //{{{ setScreenLineCount() method
718: /**
719: * Sets the number of screen lines that the specified physical line
720: * is split into.
721: * @param line the line number
722: * @param count the line count (1 if no wrap)
723: * @since jEdit 4.2pre1
724: */
725: private void setScreenLineCount(int line, int count) {
726: int oldCount = screenLineMgr.getScreenLineCount(line);
727:
728: // old one so that the screen line manager sets the
729: // validity flag!
730:
731: screenLineMgr.setScreenLineCount(line, count);
732:
733: if (count == oldCount)
734: return;
735:
736: if (!isLineVisible(line))
737: return;
738:
739: if (firstLine.physicalLine >= line) {
740: if (firstLine.physicalLine == line)
741: firstLine.callChanged = true;
742: else {
743: firstLine.scrollLine += count - oldCount;
744: firstLine.callChanged = true;
745: }
746: }
747:
748: scrollLineCount.scrollLine += count - oldCount;
749: scrollLineCount.callChanged = true;
750: } //}}}
751:
752: //}}}
753: }
|