Thanks for the tip. Here is a bug report. Let me know if you need other information.
I installed mmj2-master from https://github.com/digama0/mmj2. I'm using Debian Bullseye and here is my java version: benoit@ordi:~$ java -version openjdk version "11.0.6" 2020-01-14 OpenJDK Runtime Environment (build 11.0.6+10-post-Debian-2) OpenJDK 64-Bit Server VM (build 11.0.6+10-post-Debian-2, mixed mode) I launched mmj2 with: benoit@ordi:~$ java -Xms256M -Xmx512M -jar /home/benoit/Documents/_metamath/mmj2/mmj2jar/mmj2.jar /home/benoit/Documents/_metamath/mmj2/mmj2jar/RunParms.txt Y /home/benoit/Documents/_metamath/mmj2/mmj2jar/ /home/benoit/Documents/_metamath/mm181 "" It works (even though I get the warning "Warning: Nashorn engine is planned to be removed from a future JDK release"). Then I click on File > New Proof and type "a1i", and the moment I type "Enter", mmj2 displays an almost empty window: $( <MM> <PROOF_ASST> THEOREM= $) and the terminal displays what is copied below. When I redo this operation (File > New Proof, "a1i", "Enter"), it correctly displays a1i. Then I type "ax-mp" on the qed line, as usual, and I type Ctrl-U to unify, but it deletes the qed line, displaying "! |- ( ps -> ph )", and the terminal displays more "Ignoring exception:" messages. 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$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) 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) -- 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/048011e9-83be-45a9-aa8d-f0c99b5627fd%40googlegroups.com.
