That bug occurs when you try to use mmj2 on newer versions of the JDK. It has been fixed on master, but I don't think there has been a release with the bugfix. (Unfortunately the fix doesn't completely restore the original chunked undo behavior so you have to undo one character at a time now, but it should be usable.)
I don't think there are any relevant features in java that are being exploited in mmj2, so if you aren't using java for anything else it seems reasonable to just stick with java 8 and avoid the upgrade breakage. Mario On Wed, Mar 18, 2020 at 6:19 AM 'Stanislas Polu' via Metamath < [email protected]> wrote: > Have you tried downgrading your JRE/JDK version ? > > Undo is very unstable for me as well but I was able to live without it > so far (I think mmj2 is ripe for a at least a re-build on recent > frameworks) > > -stan > > On Wed, Mar 18, 2020 at 1:40 PM Benoit <[email protected]> wrote: > > > > Thanks Stan. So you remove "-Xincgc" (incremental garbage colllector) > altogether ? I guess it then uses a default garbage collector ? I also > saw proposals to use -XX:+UseG1GC ("garbage first" garbage collector), > while -XX:+UseConcMarkSweepGC also triggers a deprecation warning. But I > do not know how they compare and what is best for performance and stability. > > > > Then, I have another deprecation warning: > > Warning: Nashorn engine is planned to be removed from a future JDK > release > > > > Then, running mmj2, hitting Ctrl-U or Ctrl-R often makes proofs > disappear, so unfortunately mmj2 is unusable for me. > > > > Terminal output when I click File > New Proof, enter an existing label, > and get an empty statement, i.e. > > $( <MM> <PROOF_ASST> THEOREM= > > > > $) > > > > 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) > > 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) > > Exception in thread "AWT-EventQueue-0" 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(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) > > > > > > > > -- > > You received this message because you are subscribed to the Google > Groups "Metamath" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to [email protected]. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/8f92f815-b70f-479f-9356-ddf0b438fa32%40googlegroups.com > . > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CACZd_0wy4tzkLmF%2By-sAzfhogjiTkSJ3ibUu608L0eEtLSzDpA%40mail.gmail.com > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSscihyMH3oo%2BOFp7JZzSmkWWD4DNa2hqgv9%3DUxYNMw-Pw%40mail.gmail.com.
