comparison dwtx/jface/text/source/projection/ProjectionViewer.d @ 143:53b889547456

instanceof after &&
author Frank Benoit <benoit@tionex.de>
date Sun, 24 Aug 2008 21:32:37 +0200
parents b6bad70d540a
children 02cd5f1224d3
comparison
equal deleted inserted replaced
142:893c017bcdc5 143:53b889547456
1351 1351
1352 /* 1352 /*
1353 * @see dwtx.jface.text.TextViewer#handleVisibleDocumentAboutToBeChanged(dwtx.jface.text.DocumentEvent) 1353 * @see dwtx.jface.text.TextViewer#handleVisibleDocumentAboutToBeChanged(dwtx.jface.text.DocumentEvent)
1354 */ 1354 */
1355 protected void handleVisibleDocumentChanged(DocumentEvent event) { 1355 protected void handleVisibleDocumentChanged(DocumentEvent event) {
1356 if (fHandleProjectionChanges && event instanceof ProjectionDocumentEvent && isProjectionMode()) { 1356 if (fHandleProjectionChanges && cast(ProjectionDocumentEvent)event && isProjectionMode()) {
1357 ProjectionDocumentEvent e= cast(ProjectionDocumentEvent) event; 1357 ProjectionDocumentEvent e= cast(ProjectionDocumentEvent) event;
1358 1358
1359 DocumentEvent master= e.getMasterEvent(); 1359 DocumentEvent master= e.getMasterEvent();
1360 if (master !is null) 1360 if (master !is null)
1361 fReplaceVisibleDocumentExecutionTrigger= master.getDocument(); 1361 fReplaceVisibleDocumentExecutionTrigger= master.getDocument();
1385 /* 1385 /*
1386 * @see dwtx.jface.text.TextViewer#handleVisibleDocumentAboutToBeChanged(dwtx.jface.text.DocumentEvent) 1386 * @see dwtx.jface.text.TextViewer#handleVisibleDocumentAboutToBeChanged(dwtx.jface.text.DocumentEvent)
1387 * @since 3.1 1387 * @since 3.1
1388 */ 1388 */
1389 protected void handleVisibleDocumentAboutToBeChanged(DocumentEvent event) { 1389 protected void handleVisibleDocumentAboutToBeChanged(DocumentEvent event) {
1390 if (fHandleProjectionChanges && event instanceof ProjectionDocumentEvent && isProjectionMode()) { 1390 if (fHandleProjectionChanges && cast(ProjectionDocumentEvent)event && isProjectionMode()) {
1391 int deletedLines; 1391 int deletedLines;
1392 try { 1392 try {
1393 deletedLines= event.getDocument().getNumberOfLines(event.getOffset(), event.getLength()); 1393 deletedLines= event.getDocument().getNumberOfLines(event.getOffset(), event.getLength());
1394 } catch (BadLocationException e1) { 1394 } catch (BadLocationException e1) {
1395 deletedLines= 0; 1395 deletedLines= 0;