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.
