merged

--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Jan 05 15:45:29 2016 +0100
@@ -52,7 +52,7 @@
 lemma swap_apply2: "Fun.swap x y f y = f x"
   by (simp add: Fun.swap_def)
 
-lemma (in -) lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
+lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
   by auto
 
 lemma Zero_notin_Suc: "0 \<notin> Suc ` A"

--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Jan 05 15:45:29 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)

--- a/src/Tools/jEdit/src/plugin.scala	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jan 05 15:45:29 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 _ =>
     }