# HG changeset patch
# User hoelzl
# Date 1428879557 -7200
# Node ID 7ff7fdfbb9a079134c21fbdff96d3b7824b554d4
# Parent  6c86d58ab0ca6324573d2e0d48f2b0fe8d4bf8c6# Parent  a8cb3971761545ce17052811c27aea38b43a7f0f
merged

diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Sun Apr 12 11:34:16 2015 +0200
+++ b/Admin/Release/CHECKLIST	Mon Apr 13 00:59:17 2015 +0200
@@ -47,8 +47,7 @@
 - test contrib components:
     x86_64-linux without 32bit C/C++ libraries
 
-- check "Handler catches all exceptions", using
-  PolyML.Compiler.reportExhaustiveHandlers := true;
+- check "Handler catches all exceptions"
 
 - Mac OS X: check app bundle with Retina display;
 
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 Admin/Windows/Cygwin/Cygwin-Setup.bat
--- a/Admin/Windows/Cygwin/Cygwin-Setup.bat	Sun Apr 12 11:34:16 2015 +0200
+++ b/Admin/Windows/Cygwin/Cygwin-Setup.bat	Mon Apr 13 00:59:17 2015 +0200
@@ -1,4 +1,3 @@
 @echo off
 
-"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2014 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin"
-
+"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2015 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin"
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Sun Apr 12 11:34:16 2015 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Mon Apr 13 00:59:17 2015 +0200
@@ -264,10 +264,6 @@
 
       touch "contrib/cygwin/isabelle/uninitialized"
     )
-
-    perl -pi -e "s,/bin/rebaseall.*,/isabelle/rebaseall,g;" \
-      "$ISABELLE_TARGET/contrib/cygwin/etc/postinstall/autorebase.bat.done"
-
     ;;
   *)
     ;;
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/HOL/Library/Countable.thy	Mon Apr 13 00:59:17 2015 +0200
@@ -202,9 +202,9 @@
 
 ML {*
 fun countable_datatype_tac ctxt st =
-  HEADGOAL (old_countable_datatype_tac ctxt) st
-  handle exn =>
-    if Exn.is_interrupt exn then reraise exn else BNF_LFP_Countable.countable_datatype_tac ctxt st;
+  (case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of
+    SOME res => res
+  | NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st);
 
 (* compatibility *)
 fun countable_tac ctxt =
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Apr 13 00:59:17 2015 +0200
@@ -405,7 +405,7 @@
 apply (rule of_real_inverse [symmetric])
 done
 
-lemma Reals_inverse_iff [simp]: 
+lemma Reals_inverse_iff [simp]:
   fixes x:: "'a :: {real_div_algebra, division_ring}"
   shows "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
 by (metis Reals_inverse inverse_inverse_eq)
@@ -454,7 +454,7 @@
     by (metis Reals_0 setsum.infinite)
 qed
 
-lemma setprod_in_Reals [intro,simp]: 
+lemma setprod_in_Reals [intro,simp]:
   assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
 proof (cases "finite s")
   case True then show ?thesis using assms
@@ -640,7 +640,7 @@
 
 lemma norm_ge_zero [simp]: "0 \<le> norm x"
 proof -
-  have "0 = norm (x + -1 *\<^sub>R x)" 
+  have "0 = norm (x + -1 *\<^sub>R x)"
     using scaleR_add_left[of 1 "-1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one)
   also have "\<dots> \<le> norm x + norm (-1 *\<^sub>R x)" by (rule norm_triangle_ineq)
   finally show ?thesis by simp
@@ -756,7 +756,7 @@
   finally show ?thesis .
 qed
 
-lemma norm_triangle_mono: 
+lemma norm_triangle_mono:
   fixes a b :: "'a::real_normed_vector"
   shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
 by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
@@ -876,7 +876,7 @@
   shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
   by (induct A rule: infinite_finite_induct) (auto simp: norm_mult)
 
-lemma norm_setprod_le: 
+lemma norm_setprod_le:
   "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a :: 'a :: {real_normed_algebra_1, comm_monoid_mult}))"
 proof (induction A rule: infinite_finite_induct)
   case (insert a A)
@@ -891,7 +891,7 @@
 lemma norm_setprod_diff:
   fixes z w :: "'i \<Rightarrow> 'a::{real_normed_algebra_1, comm_monoid_mult}"
   shows "(\<And>i. i \<in> I \<Longrightarrow> norm (z i) \<le> 1) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> norm (w i) \<le> 1) \<Longrightarrow>
-    norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))" 
+    norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
 proof (induction I rule: infinite_finite_induct)
   case (insert i I)
   note insert.hyps[simp]
@@ -918,7 +918,7 @@
     by (auto simp add: ac_simps mult_right_mono mult_left_mono)
 qed simp_all
 
-lemma norm_power_diff: 
+lemma norm_power_diff:
   fixes z w :: "'a::{real_normed_algebra_1, comm_monoid_mult}"
   assumes "norm z \<le> 1" "norm w \<le> 1"
   shows "norm (z^m - w^m) \<le> m * norm (z - w)"
@@ -1025,7 +1025,7 @@
 
 subclass first_countable_topology
 proof
-  fix x 
+  fix x
   show "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
   proof (safe intro!: exI[of _ "\<lambda>n. {y. dist x y < inverse (Suc n)}"])
     fix S assume "open S" "x \<in> S"
@@ -1202,13 +1202,13 @@
 
 lemma zero_le_sgn_iff [simp]: "0 \<le> sgn x \<longleftrightarrow> 0 \<le> (x::real)"
   by (cases "0::real" x rule: linorder_cases) simp_all
-  
+
 lemma zero_less_sgn_iff [simp]: "0 < sgn x \<longleftrightarrow> 0 < (x::real)"
   by (cases "0::real" x rule: linorder_cases) simp_all
 
 lemma sgn_le_0_iff [simp]: "sgn x \<le> 0 \<longleftrightarrow> (x::real) \<le> 0"
   by (cases "0::real" x rule: linorder_cases) simp_all
-  
+
 lemma sgn_less_0_iff [simp]: "sgn x < 0 \<longleftrightarrow> (x::real) < 0"
   by (cases "0::real" x rule: linorder_cases) simp_all
 
@@ -1547,6 +1547,8 @@
 lemma lim_sequentially: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
   unfolding tendsto_iff eventually_sequentially ..
 
+lemmas LIMSEQ_def = lim_sequentially  (*legacy binding*)
+
 lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
   unfolding lim_sequentially by (metis Suc_leD zero_less_Suc)
 
@@ -1729,7 +1731,7 @@
   also have "\<dots> < x" using N by simp
   finally have "y \<le> x"
     by (rule order_less_imp_le) }
-  note bound_isUb = this 
+  note bound_isUb = this
 
   obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1"
     using X[THEN metric_CauchyD, OF zero_less_one] by auto
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/GUI/gui.scala	Mon Apr 13 00:59:17 2015 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/GUI/gui.scala
-    Module:     PIDE-GUI
     Author:     Makarius
 
 Basic GUI tools (for AWT/Swing).
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/GUI/html5_panel.scala
--- a/src/Pure/GUI/html5_panel.scala	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/GUI/html5_panel.scala	Mon Apr 13 00:59:17 2015 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/GUI/html5_panel.scala
-    Module:     PIDE-JFX
     Author:     Makarius
 
 HTML5 panel based on Java FX WebView.
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/GUI/jfx_gui.scala
--- a/src/Pure/GUI/jfx_gui.scala	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/GUI/jfx_gui.scala	Mon Apr 13 00:59:17 2015 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/GUI/jfx_gui.scala
-    Module:     PIDE-JFX
     Author:     Makarius
 
 Basic GUI tools (for Java FX).
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/GUI/wrap_panel.scala
--- a/src/Pure/GUI/wrap_panel.scala	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/GUI/wrap_panel.scala	Mon Apr 13 00:59:17 2015 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/GUI/wrap_panel.scala
-    Module:     PIDE-GUI
     Author:     Makarius
 
 Panel with improved FlowLayout for wrapping of components over
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Apr 13 00:59:17 2015 +0200
@@ -92,7 +92,8 @@
                   Exn.interruptible_capture (fn () =>
                     read_file_node file_node master_dir pos src_path) ()
               | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
-                  Exn.Res (blob_file src_path lines digest file_node)
+                  (Position.report pos Markup.language_path;
+                    Exn.Res (blob_file src_path lines digest file_node))
               | make_file _ (Exn.Exn e) = Exn.Exn e;
             val src_paths = Keyword.command_files keywords cmd path;
             val files =
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 13 00:59:17 2015 +0200
@@ -388,10 +388,8 @@
                     map_filter Exn.get_exn blobs_digests
                     |> List.app (Output.error_message o Runtime.exn_message)
                   else (*auxiliary files*)
-                    let val pos = Token.pos_of (nth tokens blobs_index) in
-                      Position.reports
-                        ((pos, Markup.language_path) :: maps (blob_reports pos) blobs_digests)
-                    end;
+                    let val pos = Token.pos_of (nth tokens blobs_index)
+                    in Position.reports (maps (blob_reports pos) blobs_digests) end;
               in tokens end) ());
       val commands' =
         Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/System/isabelle_system.ML	Mon Apr 13 00:59:17 2015 +0200
@@ -59,9 +59,8 @@
 (* directory operations *)
 
 fun mkdirs path =
-  if #rc (Bash.process ("mkdir -p " ^ File.shell_path path)) <> 0 then
-    error ("Failed to create directory: " ^ Path.print path)
-  else ();
+  if File.is_dir path orelse #rc (Bash.process ("mkdir -p " ^ File.shell_path path)) = 0 then ()
+  else error ("Failed to create directory: " ^ Path.print path);
 
 fun mkdir path =
   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Apr 13 00:59:17 2015 +0200
@@ -257,8 +257,8 @@
   /* mkdirs */
 
   def mkdirs(path: Path): Unit =
-    if (bash("mkdir -p " + shell_path(path)).rc != 0)
-      error("Failed to create directory: " + quote(platform_path(path)))
+    if (path.is_dir || bash("mkdir -p " + shell_path(path)).rc == 0) ()
+    else error("Failed to create directory: " + quote(platform_path(path)))
 
 
 
diff -r 6c86d58ab0ca -r 7ff7fdfbb9a0 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Apr 12 11:34:16 2015 +0200
+++ b/src/Pure/Thy/html.scala	Mon Apr 13 00:59:17 2015 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/Thy/html.scala
-    Module:     PIDE
     Author:     Makarius
 
 HTML presentation elements.