Flawed GUI initialization

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

• Mantis: MT-117

• Submitted on: 2003-01-20 by (at)klebanov

• Updated: 2003-01-26

• Assigned to: (at)aroth

Description

When the prover initializes the stage after "reading sort rules" is messed up. The representation is wriggling and shaking; Swing components disappear and reappear. An exception is thrown (attached in the bt) before everything calms down. I think this should be repaired. As far as I remember this behavior has appeared after the new prover init scheme came in place. Would be glad to assist in any way in tracking this down.

Additional Information

Exception occurred during event dispatching:
java.lang.InternalError: incorrect component
        at javax.swing.plaf.basic.BasicTreeUI.paint(BasicTreeUI.java:1008)
        at javax.swing.plaf.metal.MetalTreeUI.paint(MetalTreeUI.java:139)
        at javax.swing.plaf.ComponentUI.update(ComponentUI.java:39)
        at javax.swing.JComponent.paintComponent(JComponent.java:395)
        at javax.swing.JComponent.paint(JComponent.java:687)
        at javax.swing.JComponent.paintChildren(JComponent.java:498)
        at javax.swing.JComponent.paint(JComponent.java:696)
        at javax.swing.JComponent.paintChildren(JComponent.java:498)
        at javax.swing.JComponent.paint(JComponent.java:696)
        at javax.swing.JViewport.paint(JViewport.java:668)
        at javax.swing.JComponent.paintChildren(JComponent.java:498)
        at javax.swing.JComponent.paint(JComponent.java:696)
        at javax.swing.JComponent.paintChildren(JComponent.java:498)
        at javax.swing.JComponent.paint(JComponent.java:696)
        at javax.swing.JComponent.paintChildren(JComponent.java:498)
        at javax.swing.JSplitPane.paintChildren(JSplitPane.java:1006)
        at javax.swing.JComponent.paint(JComponent.java:696)
        at javax.swing.JComponent.paintWithBuffer(JComponent.java:3878)
        at javax.swing.JComponent._paintImmediately(JComponent.java:3821)
        at javax.swing.JComponent.paintImmediately(JComponent.java:3672)
        at javax.swing.RepaintManager.paintDirtyRegions(RepaintManager.java:370)
        at javax.swing.SystemEventQueueUtilities$ComponentWorkRequest.run(SystemEventQueueUtilities.java:124)
        at java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:154)
        at java.awt.EventQueue.dispatchEvent(EventQueue.java:337)
        at java.awt.EventDispatchThread.pumpOneEventForHierarchy(EventDispatchThread.java:131)
        at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:98)
        at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
        at java.awt.EventDispatchThread.run(EventDispatchThread.java:85)

Files

Notes

(at)aroth at 2003-01-20

Is it better / good enough in 0.480 ?

(at)klebanov at 2003-01-20

Nope. Not better yet. Btw I found the exact regression. 0.452 is OK, 0.453 (or more exactly 0.454, which fixes a typo preventing 0.453 from compiling) has the problem.

(at)pruemmer at 2003-01-20

The flicker disappears if you comment out the "updateComponentTreeUI" in line 678 of Main.java. As there is another call in main(), I'm not sure whether the second call is necessary (when not using KeY standalone).

(at)aroth at 2003-01-21

So why do we need "updateComponentTreeUI" at all? Everything seems to work fine without, even bug #87 does not occur.

(at)klebanov at 2003-01-21

Yep, works BEAUTIFULLY now. I'm stunned. What did the call do there in the first place?

QUOTE:
public static void updateComponentTreeUI(Component c)
A simple minded look and feel change: ask each node in the tree to updateUI() -- that is, to initialize its UI property with the current look and feel.

Check it in! (and reverse the latest "workaround")

(at)aroth at 2003-01-22

Done in 0.481. I don't know what the call was good for (we'll need some historians to find out). It moved somewhat around (0.453, 0.414) but not substantially.

Attributes

• Category: GUI
• Status: CLOSED
• Severity: MINOR
• OS:
• Target Version:
• Resolution: FIXED
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build: 0.479
• Tags []
• Labels: ~GUI ~Bug ~NORMAL

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:42:32.068Z
• updated_at: 2017-05-29T02:42:32.841Z
• closed_at: 2017-05-29T02:42:32.803Z (closed_by: )
• milestone:
• user_notes_count: 0