author | wenzelm |
Mon, 25 Mar 2019 17:21:26 +0100 | |
changeset 69981 | 3dced198b9ec |
parent 69838 | 4419d4d675c3 |
child 71932 | 65fd0f032a75 |
permissions | -rw-r--r-- |
69696
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
1 |
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 |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
2 |
--- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2018-04-09 01:57:13.000000000 +0200 |
69838
4419d4d675c3
formal update of patches -- no change of content;
wenzelm
parents:
69696
diff
changeset
|
3 |
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java 2019-02-24 12:21:25.986736893 +0100 |
69696
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
4 |
@@ -345,6 +345,18 @@ |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
5 |
|
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
6 |
if(vfsUpdates.size() == 1) |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
7 |
{ |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
8 |
+ // slowdown race concerning Buffer.isLoading() status |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
9 |
+ // of Buffer.save() + Buffer.finishSaving() |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
10 |
+ // versus Buffer.load() + "runnable" |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
11 |
+ try |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
12 |
+ { |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
13 |
+ Thread.sleep(100); |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
14 |
+ } |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
15 |
+ catch(InterruptedException ie) |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
16 |
+ { |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
17 |
+ Thread.currentThread().interrupt(); |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
18 |
+ } |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
19 |
+ |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
20 |
// we were the first to add an update; |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
21 |
// add update sending runnable to AWT |
9fd395ff57bc
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;
wenzelm
parents:
diff
changeset
|
22 |
// thread |