avoid crash of jEdit.closeBuffer() via TaskManager.instance.waitForIoTasks() due to race condition of save() vs. automatic load() of already open buffer, e.g. relevant for save-as on "isabelle-export:" artifacts;
authorwenzelm
Sun, 20 Jan 2019 21:26:15 +0100
changeset 69696 9fd395ff57bc
parent 69695 753ae9e9773d
child 69697 4d95261fab5a
avoid crash of jEdit.closeBuffer() via TaskManager.instance.waitForIoTasks() due to race condition of save() vs. automatic load() of already open buffer, e.g. relevant for save-as on "isabelle-export:" artifacts;
Admin/components/components.sha1
Admin/components/main
src/Tools/jEdit/patches/vfs_manager
--- a/Admin/components/components.sha1	Sat Jan 19 20:40:17 2019 +0000
+++ b/Admin/components/components.sha1	Sun Jan 20 21:26:15 2019 +0100
@@ -144,6 +144,7 @@
 9c64ee0705e5284b507ca527196081979d689519  jedit_build-20181025.tar.gz
 cfa65bf8720b9b798ffa0986bafbc8437f44f758  jedit_build-20181026.tar.gz
 847492b75b38468268f9ea424d27d53f2d95cef4  jedit_build-20181203.tar.gz
+536a38ed527115b4bf2545a2137ec57b6ffad718  jedit_build-20190120.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
--- a/Admin/components/main	Sat Jan 19 20:40:17 2019 +0000
+++ b/Admin/components/main	Sun Jan 20 21:26:15 2019 +0100
@@ -6,7 +6,7 @@
 e-2.0-2
 isabelle_fonts-20181129
 jdk-11+28
-jedit_build-20181203
+jedit_build-20190120
 jfreechart-1.5.0
 jortho-1.0-2
 kodkodi-1.5.2-1
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/vfs_manager	Sun Jan 20 21:26:15 2019 +0100
@@ -0,0 +1,22 @@
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
+--- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2018-04-09 01:57:13.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java	2019-01-20 20:55:19.968888999 +0100
+@@ -345,6 +345,18 @@
+ 
+ 				if(vfsUpdates.size() == 1)
+ 				{
++					// slowdown race concerning Buffer.isLoading() status
++					// of Buffer.save() + Buffer.finishSaving()
++					// versus Buffer.load() + "runnable"
++					try
++					{
++						Thread.sleep(100);
++					}
++					catch(InterruptedException ie)
++					{
++						Thread.currentThread().interrupt();
++					}
++
+ 					// we were the first to add an update;
+ 					// add update sending runnable to AWT
+ 					// thread