# HG changeset patch
# User wenzelm
# Date 1452004825 -3600
# Node ID ee610059b0e9900c39f65eede93e1cbab11abc1c
# Parent  bd2ccef8209b2a77e0a0c41a0419ba2a694e369b
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;

diff -r bd2ccef8209b -r ee610059b0e9 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Jan 05 15:35:08 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Jan 05 15:40:25 2016 +0100
@@ -196,8 +196,10 @@
         try { Doc.view(path) }
         catch {
           case exn: Throwable =>
-            GUI.error_dialog(view,
-              "Documentation error", GUI.scrollable_text(Exn.message(exn)))
+            GUI_Thread.later {
+              GUI.error_dialog(view,
+                "Documentation error", GUI.scrollable_text(Exn.message(exn)))
+            }
         }
       }
     }
@@ -224,7 +226,9 @@
           try { Isabelle_System.open(name) }
           catch {
             case exn: Throwable =>
-              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
+              GUI_Thread.later {
+                GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
+              }
           }
         }
       override def toString: String = "URL " + quote(name)
diff -r bd2ccef8209b -r ee610059b0e9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Jan 05 15:35:08 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jan 05 15:40:25 2016 +0100
@@ -146,7 +146,7 @@
 
   /* current document content */
 
-  def snapshot(view: View): Document.Snapshot =
+  def snapshot(view: View): Document.Snapshot = GUI_Thread.now
   {
     val buffer = view.getBuffer
     document_model(buffer) match {
@@ -293,8 +293,10 @@
         delay_load.invoke()
 
       case Session.Shutdown =>
-        PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
-        delay_load.revoke()
+        GUI_Thread.later {
+          delay_load.revoke()
+          PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
+        }
 
       case _ =>
     }