49 |
import javax.swing.event.DocumentEvent; |
import javax.swing.event.DocumentEvent; |
50 |
import javax.swing.event.DocumentEvent.ElementChange; |
import javax.swing.event.DocumentEvent.ElementChange; |
51 |
|
|
52 |
public class PlainView extends View |
public class PlainView extends View implements TabExpander |
|
implements TabExpander |
|
53 |
{ |
{ |
54 |
Color selectedColor; |
Color selectedColor; |
55 |
Color unselectedColor; |
Color unselectedColor; |
255 |
} |
} |
256 |
catch (BadLocationException ex) |
catch (BadLocationException ex) |
257 |
{ |
{ |
258 |
|
assert false : "BadLocationException should not be thrown here."; |
259 |
} |
} |
260 |
|
|
261 |
if (seg == null || seg.array == null || seg.count == 0) |
if (seg == null || seg.array == null || seg.count == 0) |
416 |
} |
} |
417 |
catch (BadLocationException ex) |
catch (BadLocationException ex) |
418 |
{ |
{ |
419 |
|
assert false : "BadLocationException should not be thrown here."; |
420 |
} |
} |
421 |
|
|
422 |
if (seg == null || seg.array == null || seg.count == 0) |
if (seg == null || seg.array == null || seg.count == 0) |
504 |
else |
else |
505 |
{ |
{ |
506 |
Rectangle repaintRec = rec0.union(rec1); |
Rectangle repaintRec = rec0.union(rec1); |
507 |
host.repaint(0, repaintRec.y, host.getWidth(), |
host.repaint(); |
|
repaintRec.height); |
|
508 |
} |
} |
509 |
} |
} |
510 |
|
|