digama0 / mmj2

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

ClassCastException on New Proof #58

Closed brlarson closed 2 years ago

brlarson commented 2 years ago

Attempting File > New Proof and entering "bl.add2i" in the dialog box causes a cascade of ClassCastException below.

I created ccerror.mm (attached)ccerror.mm.zipto have the fewest number of constructs to cause the error.

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.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$WorksheetRequest.receive(ProofAsstGUI.java:2248) 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(AccessController.java:391) 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) 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) 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) 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) 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) 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)

brlarson commented 2 years ago

Closing and re-launching the Terminal window on MacOS cured the problem.

Sorry for the inconvenience.

digama0 commented 2 years ago

This is a known issue of using Java >9, but there should be a version check in there to prevent this from happening. My guess is that your installation lied about the version somehow due to a misconfiguration.

brlarson commented 2 years ago

Mario,

I figured something was amiss. I ran this (a.k.a MacMMJ2.command) when re-launching:

change java to 1.8

export JAVA_HOME=/usr/libexec/java_home -v 1.8

launch mmj2

java -Xms512M -Xmx1028M -jar /Applications/metamath-SEP2021/mmj2/mmj2jar/mmj2.jar "RunParms.txt" Y "/Users/brianlarson/git/LaTeX-metamath/mm/" "" ""

Others, of course, would have different folder locations.

I've had occasion where the export JAVA_HOME was ignored. Rebooting MacOS was the only thing top fix it.

--Brian

On Jan 23, 2022, at 3:59 PM, Mario Carneiro @.**@.>> wrote:

This email originated from outside of K-State.

This is a known issue of using Java >9, but there should be a version check in there to prevent this from happening. My guess is that your installation lied about the version somehow due to a misconfiguration.

— Reply to this email directly, view it on GitHubhttps://github.com/digama0/mmj2/issues/58#issuecomment-1019575662, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAJC32TDXFQJYQFO4BFXFWLUXR247ANCNFSM5MP5QY4Q. Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub. You are receiving this because you modified the open/close state.Message ID: @.***>

digama0 commented 2 years ago

Note that the script for running on macs is untested and largely unchanged since I started maintaining this project, as I don't have a mac to test with, so if you find an issue in the script please send a PR.