| author | wenzelm | 
| Sat, 19 Dec 2020 15:32:29 +0100 | |
| changeset 72958 | 0d8bc0252e2e | 
| parent 72247 | c06260b7152c | 
| child 73653 | d9823224fcfe | 
| permissions | -rw-r--r-- | 
| 72247 | 1 | diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java | 
| 2 | --- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 2020-09-03 05:31:03.000000000 +0200 | |
| 3 | +++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java 2020-09-08 20:13:35.656786460 +0200 | |
| 71932 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 4 | @@ -380,6 +380,18 @@ | 
| 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 | 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 |