search

digama0 / mmj2

mmj2 GUI Proof Assistant for the Metamath project
GNU General Public License v2.0
72 stars 24 forks source link

mmj2 prints "cannot be cast to class" exception when unify (check proof) option is chosen #40

Closed Prosfilaes closed 4 years ago

Prosfilaes commented 4 years ago

When mmj2 is run from the jar in the git archive (as of May 4, 2020), clicking on unify (check proof) deletes the proof and emits the following error message on the console:

Exception in thread "AWT-EventQueue-0" Ignoring exception: java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap') at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110) at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293) at java.desktop/javax.swing.text.DefaultStyledDocument.setCharacterAttributes(DefaultStyledDocument.java:530) at mmj.pa.ColorThread.processEvent(ColorThread.java:266) at mmj.pa.ColorThread.run(ColorThread.java:170) java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap') at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110) at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293) at java.desktop/javax.swing.text.AbstractDocument.handleRemove(AbstractDocument.java:632) at java.desktop/javax.swing.text.AbstractDocument.remove(AbstractDocument.java:596) at mmj.pa.HighlightedDocument.remove(HighlightedDocument.java:101) at mmj.pa.HighlightedDocument.setTextProgrammatic(HighlightedDocument.java:178) at mmj.pa.ProofAsstGUI.setProofTextAreaText(ProofAsstGUI.java:618) at mmj.pa.ProofAsstGUI.displayProofWorksheet(ProofAsstGUI.java:2354) at mmj.pa.ProofAsstGUI.access$3(ProofAsstGUI.java:2345) at mmj.pa.ProofAsstGUI$44.receive(ProofAsstGUI.java:2150) at mmj.pa.ProofAsstGUI$RequestThreadStuff.lambda$0(ProofAsstGUI.java:2295) at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:313) at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:770) at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721) at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:715) at java.base/java.security.AccessController.doPrivileged(Native Method) at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85) at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:740) at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203) at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124) at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113) at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109) at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101) at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90) Ignoring exception: java.lang.ClassCastException: class javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper cannot be cast to class javax.swing.text.AbstractDocument$DefaultDocumentEvent (javax.swing.text.AbstractDocument$DefaultDocumentEventUndoableWrapper and javax.swing.text.AbstractDocument$DefaultDocumentEvent are in module java.desktop of loader 'bootstrap') at mmj.pa.CompoundUndoManager.undoableEditHappened(CompoundUndoManager.java:110) at java.desktop/javax.swing.text.AbstractDocument.fireUndoableEditUpdate(AbstractDocument.java:293) at java.desktop/javax.swing.text.DefaultStyledDocument.setCharacterAttributes(DefaultStyledDocument.java:530) at mmj.pa.ColorThread.processEvent(ColorThread.java:266) at mmj.pa.ColorThread.run(ColorThread.java:170)

This seems to be a change in Java 9; see https://github.com/nordfalk/jsyntaxpane/commit/5fc75594f8bc4df6e8f7096d4a440490b768fd46#diff-b3f8826824f551219879f1c798618c12R67 for one example of how it was fixed.

digama0 commented 4 years ago

This is already fixed in master.

Prosfilaes commented 4 years ago

It's not fixed in master; the jar file needs to be recompiled.

digama0 commented 4 years ago

The jar file in master should not be there. It is a build artifact and should not be part of version control, but a lot of the project structure is grandfathered in from the pre-git distribution. If #41 goes well, the releases will be there instead of in the source code.