Stream: Mirror: Isabelle Development Mailing List

Topic: recent.xml – java.lang.IllegalArgumentException: requirem...

view this post on Zulip Email Gateway (May 02 2025 at 16:37):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
This refers to 0af7fe946bfd9543697a6736ce244f1b2e004060

Quite often, jEdit refuses to start with the following traceback:

11:38:49 [main] [error] Plugin: java.lang.IllegalArgumentException: requirement failed: GUI thread expected
11:38:49 [main] [error] Plugin: at scala.Predef$.require(Predef.scala:337)
11:38:49 [main] [error] Plugin: at isabelle.GUI_Thread$.require(gui_thread.scala:24)
11:38:49 [main] [error] Plugin: at isabelle.jedit.Isabelle_Navigator.init(isabelle_navigator.scala:158)
11:38:49 [main] [error] Plugin: at isabelle.jedit.Main_Plugin.start(main_plugin.scala:445)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.PluginJAR.startPlugin(PluginJAR.java:1737)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:957)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.JARClassLoader._loadClass(JARClassLoader.java:393)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:112)
11:38:49 [main] [error] Plugin: at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:526)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.classpath.ClassManagerImpl.classForName(ClassManagerImpl.java:204)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.NameSpace.classForName(NameSpace.java:1320)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.NameSpace.getClassImpl(NameSpace.java:1220)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.NameSpace.getClass(NameSpace.java:1161)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.Name.consumeNextObjectField(Name.java:298)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.Name.toObject(Name.java:199)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.BSHAmbiguousName.toObject(BSHAmbiguousName.java:60)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.BSHAllocationExpression.objectAllocation(BSHAllocationExpression.java:86)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.BSHAllocationExpression.eval(BSHAllocationExpression.java:62)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.BSHPrimaryExpression.eval(BSHPrimaryExpression.java:102)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.BSHPrimaryExpression.eval(BSHPrimaryExpression.java:47)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:644)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:738)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:727)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.BeanShellFacade._eval(BeanShellFacade.java:153)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.BeanShellFacade.eval(BeanShellFacade.java:117)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.BeanShell.eval(BeanShell.java:382)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.ServiceManager$Descriptor.getInstance(ServiceManager.java:337)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.ServiceManager.getService(ServiceManager.java:262)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.io.VFSManager.getVFSForProtocol(VFSManager.java:156)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.MiscUtilities.isURL(MiscUtilities.java:583)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.io.VFSManager.getVFSForPath(VFSManager.java:174)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.MiscUtilities.pathsEqual(MiscUtilities.java:1198)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.BufferHistory.getEntry(BufferHistory.java:88)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.jEdit.composeBufferPropsFromHistory(jEdit.java:4409)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1860)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1826)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1779)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.BeanShell._runScript(BeanShell.java:328)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.BeanShell._runScript(BeanShell.java:291)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.BeanShell.runScript(BeanShell.java:217)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.Macros$BeanShellHandler.runMacro(Macros.java:1115)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.jEdit.runStartupScripts(jEdit.java:3992)
11:38:49 [main] [error] Plugin: at org.gjt.sp.jedit.jEdit.main(jEdit.java:553)
11:38:49 [main] [error] Plugin: at isabelle.jedit.JEdit_Main$.$anonfun$5(jedit_main.scala:126)
11:38:49 [main] [error] Plugin: at isabelle.jedit.JEdit_Main$.main(jedit_main.scala:135)
11:38:49 [main] [error] Plugin: at isabelle.jedit.JEdit_Main.main(jedit_main.scala)

Remove ~/.isabelle/jedit/recent.xml restores proper behaviour.

I have attached one problematic recent.xml

Florian

recent.xml
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

view this post on Zulip Email Gateway (May 09 2025 at 07:33):

From: Tobias Nipkow <nipkow@in.tum.de>
Thanks for the hint (and thanks to Fabian for reminding me), I have also
encountered it now.

Tobias

On 02/05/2025 18:37, Florian Haftmann wrote:

This refers to 0af7fe946bfd9543697a6736ce244f1b2e004060

Quite often, jEdit refuses to start with the following traceback:

11:38:49 [main] [error] Plugin: java.lang.IllegalArgumentException: requirement failed: GUI thread expected
11:38:49 [main] [error] Plugin:  at scala.Predef$.require(Predef.scala:337)
11:38:49 [main] [error] Plugin:  at isabelle.GUI_Thread$.require(gui_thread.scala:24)
11:38:49 [main] [error] Plugin:  at isabelle.jedit.Isabelle_Navigator.init(isabelle_navigator.scala:158)
11:38:49 [main] [error] Plugin:  at isabelle.jedit.Main_Plugin.start(main_plugin.scala:445)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.PluginJAR.startPlugin(PluginJAR.java:1737)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:957)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.JARClassLoader._loadClass(JARClassLoader.java:393)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:112)
11:38:49 [main] [error] Plugin:  at java.base/ java.lang.ClassLoader.loadClass(ClassLoader.java:526)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.classpath.ClassManagerImpl.classForName(ClassManagerImpl.java:204)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.NameSpace.classForName(NameSpace.java:1320)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.NameSpace.getClassImpl(NameSpace.java:1220)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.NameSpace.getClass(NameSpace.java:1161)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.Name.consumeNextObjectField(Name.java:298)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.Name.toObject(Name.java:199)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.BSHAmbiguousName.toObject(BSHAmbiguousName.java:60)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.BSHAllocationExpression.objectAllocation(BSHAllocationExpression.java:86)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.BSHAllocationExpression.eval(BSHAllocationExpression.java:62)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.BSHPrimaryExpression.eval(BSHPrimaryExpression.java:102)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.BSHPrimaryExpression.eval(BSHPrimaryExpression.java:47)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:644)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:738)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:727)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.BeanShellFacade._eval(BeanShellFacade.java:153)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.BeanShellFacade.eval(BeanShellFacade.java:117)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.BeanShell.eval(BeanShell.java:382)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.ServiceManager$Descriptor.getInstance(ServiceManager.java:337)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.ServiceManager.getService(ServiceManager.java:262)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.io.VFSManager.getVFSForProtocol(VFSManager.java:156)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.MiscUtilities.isURL(MiscUtilities.java:583)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.io.VFSManager.getVFSForPath(VFSManager.java:174)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.MiscUtilities.pathsEqual(MiscUtilities.java:1198)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.BufferHistory.getEntry(BufferHistory.java:88)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.jEdit.composeBufferPropsFromHistory(jEdit.java:4409)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1860)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1826)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1779)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.BeanShell._runScript(BeanShell.java:328)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.BeanShell._runScript(BeanShell.java:291)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.BeanShell.runScript(BeanShell.java:217)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.Macros$BeanShellHandler.runMacro(Macros.java:1115)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.jEdit.runStartupScripts(jEdit.java:3992)
11:38:49 [main] [error] Plugin:  at org.gjt.sp.jedit.jEdit.main(jEdit.java:553)
11:38:49 [main] [error] Plugin:  at isabelle.jedit.JEdit_Main$. $anonfun$5(jedit_main.scala:126)
11:38:49 [main] [error] Plugin:  at isabelle.jedit.JEdit_Main$.main(jedit_main.scala:135)
11:38:49 [main] [error] Plugin:  at isabelle.jedit.JEdit_Main.main(jedit_main.scala)

Remove ~/.isabelle/jedit/recent.xml restores proper behaviour.

I have attached one problematic recent.xml

Florian

smime.p7s

view this post on Zulip Email Gateway (May 11 2025 at 10:11):

From: Makarius <makarius@sketis.net>
On 02/05/2025 18:37, Florian Haftmann wrote:

This refers to 0af7fe946bfd9543697a6736ce244f1b2e004060

Quite often, jEdit refuses to start with the following traceback:

isabelle.jedit.Isabelle_Navigator.init(isabelle_navigator.scala:158) 11:38:49 [main] [error] Plugin:  at
isabelle.jedit.Main_Plugin.start(main_plugin.scala:445)``

Remove ~/.isabelle/jedit/recent.xml restores proper behaviour.

I have attached one problematic recent.xml

Thanks for the hint and the reproducible example. See now:

changeset: 82619:bfc920530ae6
tag: tip
user: wenzelm
date: Sun May 11 12:05:10 2025 +0200
files: src/Tools/jEdit/src/isabelle_navigator.scala
description:
more robust (amending 4ca84abb16ef): Main_Plugin.start() could happen on other
thread, e.g. when $JEDIT_SETTINGS/recent.xml refers to "isabelle-export:" URL;

Makarius

Last updated: May 31 2025 at 01:44 UTC