comparison dwtx/jface/text/AbstractLineTracker.d @ 134:51e6e63f930e

Regex fix for casts
author Frank Benoit <benoit@tionex.de>
date Sun, 24 Aug 2008 01:46:20 +0200
parents 7d818bd32d63
children 65801ad2b265
comparison
equal deleted inserted replaced
133:7d818bd32d63 134:51e6e63f930e
368 * @since 3.2 368 * @since 3.2
369 */ 369 */
370 private void checkImplementation() { 370 private void checkImplementation() {
371 if (fNeedsConversion) { 371 if (fNeedsConversion) {
372 fNeedsConversion= false; 372 fNeedsConversion= false;
373 fDelegate= new TreeLineTracker((ListLineTracker) fDelegate) { 373 fDelegate= new TreeLineTracker(cast(ListLineTracker) fDelegate) {
374 protected DelimiterInfo nextDelimiterInfo(String text, int offset) { 374 protected DelimiterInfo nextDelimiterInfo(String text, int offset) {
375 return AbstractLineTracker.this.nextDelimiterInfo(text, offset); 375 return AbstractLineTracker.this.nextDelimiterInfo(text, offset);
376 } 376 }
377 377
378 public String[] getLegalLineDelimiters() { 378 public String[] getLegalLineDelimiters() {
431 * 431 *
432 * @throws BadLocationException in case the recorded requests cannot be processed correctly 432 * @throws BadLocationException in case the recorded requests cannot be processed correctly
433 * @since 3.1 433 * @since 3.1
434 */ 434 */
435 protected final void flushRewriteSession() throws BadLocationException { 435 protected final void flushRewriteSession() throws BadLocationException {
436 if (DEBUG) 436 if cast(DEBUG)
437 System.out.println("AbstractLineTracker: Flushing rewrite session: " + fActiveRewriteSession); //$NON-NLS-1$ 437 System.out.println("AbstractLineTracker: Flushing rewrite session: " + fActiveRewriteSession); //$NON-NLS-1$
438 438
439 Iterator e= fPendingRequests.iterator(); 439 Iterator e= fPendingRequests.iterator();
440 440
441 fPendingRequests= null; 441 fPendingRequests= null;
442 fActiveRewriteSession= null; 442 fActiveRewriteSession= null;
443 443
444 while (e.hasNext()) { 444 while (e.hasNext()) {
445 Request request= (Request) e.next(); 445 Request request= cast(Request) e.next();
446 if (request.isReplaceRequest()) 446 if (request.isReplaceRequest())
447 replace(request.offset, request.length, request.text); 447 replace(request.offset, request.length, request.text);
448 else 448 else
449 set(request.text); 449 set(request.text);
450 } 450 }