--- 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;
--- 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"
--- 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"
-
;;
*)
;;
--- 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 =
--- 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
--- 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).
--- 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.
--- 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).
--- 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
--- 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 =
--- 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
--- 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);
--- 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)))
--- 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.