<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">2014-04-02 10:47 GMT+02:00 Makarius <span dir="ltr"><<a href="mailto:makarius@sketis.net" target="_blank">makarius@sketis.net</a>></span>:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="">On Wed, 2 Apr 2014, stvienna wiener wrote:<br>
<br></div>
What is your OS and hardware platform (memory, number of cores)?<br><div class=""></div></blockquote><div><br><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt" id="docs-internal-guid-86911dab-4e1e-982a-e27e-0628a6799d15">
<span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">I am running a 64-bit arch linux distribution, but without any 32-bit compatibility libraries. I have a labtop with a quad core i7 cpu (i7-3720QM CPU @ 2.60GHz; Isabelle “sees” 8 workers), 16GB of memory and a fast SSD.</span></p>
<br><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"></span><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">What is the right way to allocate more memory to Isabelle/JEdit from the start on? I mean I have 16GB and it seems with the default settings JEdit uses only 1 GB.</span><br>
<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
If you have an exception trace, the obvious thing is to show that here.<span class=""><font color="#888888"><br></font></span></blockquote><div><br><br><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt" id="docs-internal-guid-86911dab-4e20-4135-433c-8d91fd4121b6">
<span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">*I am running Isabelle development version*</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">$ hg id -i</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">907f04603177</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">$ hg identify --num</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">56527</span></p>
<br><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"></span><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt">
<span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">How are issues supposed to be reported? Should I give a snipped in the E-Mail and post the rest to pastebin or so? If you have suggestions tell me (I posted the full stacktrace here in the e-mail).</span></p>
<br><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"></span><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt">
<span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">*POSSIBLE ISSUE 1*</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Syslog Panel:</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Unofficial version of Isabelle/HOL (unidentified repository version)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Warning - Unable to increase stack - interrupting thread</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Warning - Unable to increase stack - interrupting thread </span></p>
<br><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"></span><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt">
<span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">*POSSIBLE ISSUE 2*</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">[isabelle3@st-pc787 isabelle]$ ./bin/isabelle jedit -l HOL</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0: Exception in thread "AWT-EventQueue-0"</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0: java.lang.NullPointerException</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3414)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3405)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at org.gjt.sp.jedit.EditAction$Wrapper.actionPerformed(EditAction.java:212)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:2018)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2341)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:402)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:259)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at javax.swing.AbstractButton.doClick(AbstractButton.java:376)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at javax.swing.plaf.basic.BasicMenuItemUI.doClick(BasicMenuItemUI.java:833)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at javax.swing.plaf.basic.BasicMenuItemUI$Handler.mouseReleased(BasicMenuItemUI.java:877)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.AWTEventMulticaster.mouseReleased(AWTEventMulticaster.java:289)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Component.processMouseEvent(Component.java:6505)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at javax.swing.JComponent.processMouseEvent(JComponent.java:3320)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Component.processEvent(Component.java:6270)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Container.processEvent(Container.java:2229)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Component.dispatchEventImpl(Component.java:4861)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Container.dispatchEventImpl(Container.java:2287)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Component.dispatchEvent(Component.java:4687)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4832)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.LightweightDispatcher.processMouseEvent(Container.java:4492)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.LightweightDispatcher.dispatchEvent(Container.java:4422)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Container.dispatchEventImpl(Container.java:2273)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Window.dispatchEventImpl(Window.java:2719)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.Component.dispatchEvent(Component.java:4687)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventQueue.dispatchEventImpl(EventQueue.java:735)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventQueue.access$200(EventQueue.java:103)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventQueue$3.run(EventQueue.java:694)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventQueue$3.run(EventQueue.java:692)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.security.AccessController.doPrivileged(Native Method)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:87)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventQueue$4.run(EventQueue.java:708)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventQueue$4.run(EventQueue.java:706)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.security.AccessController.doPrivileged(Native Method)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventQueue.dispatchEvent(EventQueue.java:705)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:242)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:161)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:150)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:146)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:138)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:13:33 AM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at java.awt.EventDispatchThread.run(EventDispatchThread.java:91)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:27:48 AM [jEdit Worker #4] [error] ErrorListDialog$ErrorEntry: /home/stephan/Isabelle/repo2/NotepadIssue.thy:</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:27:48 AM [jEdit Worker #4] [error] ErrorListDialog$ErrorEntry: Cannot list directory.</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:28:40 AM [jEdit Worker #2] [error] BufferSaveRequest: Unable to save buffer java.io.FileNotFoundException: /home/stephan/Isabelle/repo2/NotepadIssue.thy/Untitled-1 (Not a directory)</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:28:40 AM [jEdit Worker #2] [error] ErrorListDialog$ErrorEntry: /home/stephan/Isabelle/repo2/NotepadIssue.thy/Untitled-1:</span></p>
<p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt"><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">1:28:40 AM [jEdit Worker #2] [error] ErrorListDialog$ErrorEntry: Cannot save: /home/stephan/Isabelle/repo2/NotepadIssue.thy/Untitled-1 (Not a directory)</span></p>
<br><span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"></span><p dir="ltr" style="line-height:1.15;margin-top:0pt;margin-bottom:0pt">
<span style="font-size:15px;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:normal;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">(the problem above is perhaps due to unreadable files because the files belong to a different user)</span></p>
<br><br><br></div><div>Stephan A. (from Vienna)<br></div></div></div></div>