# HG changeset patch
# User eberlm
# Date 1452012861 -3600
# Node ID 4db2d39aa76c0f11ac41521b45f8cdc9e4e44a6b
# Parent  1546a042e87b391e9802f492734ba6f745b6035b# Parent  d9874039786e167abe87d23942a899380bbcdff8
Merged

diff -r 1546a042e87b -r 4db2d39aa76c ANNOUNCE
--- a/ANNOUNCE	Tue Jan 05 17:54:10 2016 +0100
+++ b/ANNOUNCE	Tue Jan 05 17:54:21 2016 +0100
@@ -20,8 +20,7 @@
 
 * HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.
 
-* Many HOL library improvements, including advanced topological concepts and
-integration theory ported from HOL Light.
+* Many HOL library improvements, notably HOL-Multivariate_Analysis.
 
 * Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard
 ML), per-thread profiling, native Windows version (32bit and 64bit).
diff -r 1546a042e87b -r 4db2d39aa76c CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Jan 05 17:54:10 2016 +0100
+++ b/CONTRIBUTORS	Tue Jan 05 17:54:21 2016 +0100
@@ -8,40 +8,37 @@
 
 * Winter 2015: Manuel Eberl, TUM
   The radius of convergence of power series and various summability tests.
-  Harmonic numbers and the Euler–Mascheroni constant.
+  Harmonic numbers and the Euler-Mascheroni constant.
   The Generalised Binomial Theorem.
-  The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and 
-  their most important properties.
+  The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
+  most important properties.
 
 * Autumn 2015: Florian Haftmann, TUM
-  Rewrite definitions for global interpretations and sublocale
-  declarations.
+  Rewrite definitions for global interpretations and sublocale declarations.
 
 * Autumn 2015: Andreas Lochbihler
-  Bourbaki-Witt fixpoint theorem for increasing functions on
-  chain-complete partial orders.
+  Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete
+  partial orders.
 
 * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
   A large number of additional binomial identities.
 
 * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
-  Isar subgoal command for proof structure within unstructured proof
-  scripts.
+  Isar subgoal command for proof structure within unstructured proof scripts.
 
 * Summer 2015: Florian Haftmann, TUM
   Generic partial division in rings as inverse operation of multiplication.
 
 * Summer 2015: Manuel Eberl and Florian Haftmann, TUM
-  Type class hierarchy with common algebraic notions of integral
-  (semi)domains like units, associated elements and normalization
-  wrt. units.
+  Type class hierarchy with common algebraic notions of integral (semi)domains
+  like units, associated elements and normalization wrt. units.
 
 * Summer 2015: Florian Haftmann, TUM
   Fundamentals of abstract type class for factorial rings.
 
 * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich
-  Command to lift a BNF structure on the raw type to the abstract type
-  for typedefs.
+  Command to lift a BNF structure on the raw type to the abstract type for
+  typedefs.
 
 
 Contributions to Isabelle2015
diff -r 1546a042e87b -r 4db2d39aa76c NEWS
--- a/NEWS	Tue Jan 05 17:54:10 2016 +0100
+++ b/NEWS	Tue Jan 05 17:54:21 2016 +0100
@@ -642,7 +642,8 @@
 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
 Minor INCOMPATIBILITY, use 'function' instead.
 
-* Library/Periodic_Fun: a locale that provides convenient lemmas for periodic functions
+* Library/Periodic_Fun: a locale that provides convenient lemmas for
+periodic functions.
 
 * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (=
 complex path integrals), Cauchy's integral theorem, winding numbers and
@@ -653,9 +654,10 @@
 components, homotopic paths and the inside or outside of a set.
 
 * Multivariate_Analysis: radius of convergence of power series and 
-  various summability tests; Harmonic numbers and the Euler–Mascheroni constant;
-  the Generalised Binomial Theorem; the complex and real Gamma/log-Gamma/Digamma/
-  Polygamma functions and their most important properties;
+various summability tests; Harmonic numbers and the Euler–Mascheroni
+constant; the Generalised Binomial Theorem; the complex and real
+Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
+properties.
 
 * Data_Structures: new and growing session of standard data structures.
 
diff -r 1546a042e87b -r 4db2d39aa76c src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Jan 05 17:54:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Jan 05 17:54:21 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"
diff -r 1546a042e87b -r 4db2d39aa76c src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Jan 05 17:54:10 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Jan 05 17:54:21 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 1546a042e87b -r 4db2d39aa76c src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Jan 05 17:54:10 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jan 05 17:54:21 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 _ =>
     }