--- a/Admin/PLATFORMS Wed Jun 06 11:12:37 2018 +0200
+++ b/Admin/PLATFORMS Wed Jun 06 13:04:52 2018 +0200
@@ -39,7 +39,7 @@
macOS 10.13 High Sierra
x86_64-windows Windows 7
- x86_64-cygwin Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86_64/release)
+ x86_64-cygwin Cygwin 2.10 https://isabelle.sketis.net/cygwin_2018 (x86_64/release)
All of the above platforms are 100% supported by Isabelle -- end-users
should not have to care about the differences (at least in theory).
--- a/Admin/Windows/Cygwin/Cygwin-Setup.bat Wed Jun 06 11:12:37 2018 +0200
+++ b/Admin/Windows/Cygwin/Cygwin-Setup.bat Wed Jun 06 13:04:52 2018 +0200
@@ -1,3 +1,3 @@
@echo off
-"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2017 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin"
+"%CD%\contrib\cygwin\isabelle\cygwin" --site "{MIRROR}" --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin"
--- a/Admin/Windows/Cygwin/README Wed Jun 06 11:12:37 2018 +0200
+++ b/Admin/Windows/Cygwin/README Wed Jun 06 13:04:52 2018 +0200
@@ -1,10 +1,10 @@
Cygwin
======
-* http://www.cygwin.com/
+* https://www.cygwin.com/
* Mirror with many old versions (not setup.ini)
- http://ftp.eq.uc.pt/software/pc/prog/cygwin
+ https://ftp.eq.uc.pt/software/pc/prog/cygwin
* Local snapshots:
http://isabelle.in.tum.de/cygwin (Isabelle2012)
@@ -15,6 +15,7 @@
http://isabelle.in.tum.de/cygwin_2016 (Isabelle2016)
http://isabelle.in.tum.de/cygwin_2016-1 (Isabelle2016-1)
http://isabelle.in.tum.de/cygwin_2017 (Isabelle2017)
+ https://isabelle.sketis.net/cygwin_2018 (Isabelle2018)
* Apache2 redirects for virtual host isabelle.conf:
Redirect /cygwin/release http://ftp.eq.uc.pt/software/pc/prog/cygwin/release
@@ -31,6 +32,9 @@
Redirect /cygwin_2017/x86/release http://ftp.eq.uc.pt/software/pc/prog/cygwin/x86/release
Redirect /cygwin_2017/x86_64/release http://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
Redirect /cygwin_2017/noarch/release http://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
+ Redirect /cygwin_2018/x86/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86/release
+ Redirect /cygwin_2018/x86_64/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
+ Redirect /cygwin_2018/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
* Quasi-component: "isabelle build_cygwin" (as Administrator)
--- a/Admin/components/bundled-windows Wed Jun 06 11:12:37 2018 +0200
+++ b/Admin/components/bundled-windows Wed Jun 06 13:04:52 2018 +0200
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20170930
+cygwin-20180604
windows_app-20180417
--- a/Admin/components/components.sha1 Wed Jun 06 11:12:37 2018 +0200
+++ b/Admin/components/components.sha1 Wed Jun 06 13:04:52 2018 +0200
@@ -37,6 +37,7 @@
d9ad7aae99d54e3b9813151712eb88a441613f04 cygwin-20161024.tar.gz
f8eb6a0f722e3cfe3775d1204c5c7063ee1f008e cygwin-20170828.tar.gz
c22048912b010a5a0b4f2a3eb4d318d6953761e4 cygwin-20170930.tar.gz
+5a3919e665947b820fd7f57787280c7512be3782 cygwin-20180604.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
--- a/Admin/lib/Tools/makedist_bundle Wed Jun 06 11:12:37 2018 +0200
+++ b/Admin/lib/Tools/makedist_bundle Wed Jun 06 13:04:52 2018 +0200
@@ -284,8 +284,12 @@
(
cd "$ISABELLE_TARGET"
- cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
- "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" .
+ cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" .
+
+ CYGWIN_MIRROR="$(cat contrib/cygwin/isabelle/cygwin_mirror)"
+ cat "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" | \
+ perl -p > "Cygwin-Setup.bat" -e "s,{MIRROR},$CYGWIN_MIRROR,;"
+ chmod +x "Cygwin-Setup.bat"
for NAME in postinstall rebaseall
do
--- a/NEWS Wed Jun 06 11:12:37 2018 +0200
+++ b/NEWS Wed Jun 06 13:04:52 2018 +0200
@@ -71,6 +71,9 @@
*** Isabelle/jEdit Prover IDE ***
+* Slightly more parallel checking, notably for high priority print
+functions (e.g. State output).
+
* The view title is set dynamically, according to the Isabelle
distribution and the logic session name. The user can override this via
set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
@@ -86,16 +89,16 @@
E.g. "Prob" may be completed to "HOL-Probability.Probability".
* The command-line tool "isabelle jedit" provides more flexible options
-for session selection:
- - options -P opens the parent session image of -l
- - options -A and -B modify the meaning of -l to produce a base
- image on the spot, based on the specified ancestor (or parent)
- - option -F focuses on the specified logic session
- - option -R has changed: it only opens the session ROOT entry
- - option -S sets up the development environment to edit the
- specified session: it abbreviates -B -F -R -l
+for session management:
+ - option -R builds an auxiliary logic image with all required theories
+ from other sessions, relative to an ancestor session given by option
+ -A (default: parent)
+ - option -S is like -R, with a focus on the selected session and its
+ descendants (this reduces startup time for big projects like AFP)
Examples:
+ isabelle jedit -R HOL-Number_Theory
+ isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
@@ -236,14 +239,14 @@
* Abstract bit operations as part of Main: push_bit, take_bit,
drop_bit.
-* New, more general, axiomatization of complete_distrib_lattice.
+* New, more general, axiomatization of complete_distrib_lattice.
The former axioms:
"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
-are replaced by
+are replaced by
"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
-The instantiations of sets and functions as complete_distrib_lattice
+The instantiations of sets and functions as complete_distrib_lattice
are moved to Hilbert_Choice.thy because their proofs need the Hilbert
-choice operator. The dual of this property is also proved in
+choice operator. The dual of this property is also proved in
Hilbert_Choice.thy.
* New syntax for the minimum/maximum of a function over a finite set:
@@ -292,7 +295,7 @@
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
INCOMPATIBILITY.
-* The relator rel_filter on filters has been strengthened to its
+* The relator rel_filter on filters has been strengthened to its
canonical categorical definition with better properties. INCOMPATIBILITY.
* Generalized linear algebra involving linear, span, dependent, dim
@@ -305,7 +308,7 @@
* HOL-Algebra: renamed (^) to [^]
-* Session HOL-Analysis: Moebius functions, the Riemann mapping
+* Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping
theorem, the Vitali covering theorem, change-of-variables results for
integration and measures.
--- a/README_REPOSITORY Wed Jun 06 11:12:37 2018 +0200
+++ b/README_REPOSITORY Wed Jun 06 13:04:52 2018 +0200
@@ -5,10 +5,10 @@
--------------------
1a. Linux and Mac OS X: ensure that Mercurial is installed
- (see also http://www.selenic.com/mercurial)
+ (see also https://www.mercurial-scm.org)
1b. Windows: ensure that Cygwin64 with curl and Mercurial is installed
- (see also http://www.cygwin.com)
+ (see also https://www.cygwin.com)
2. Clone repository (bash shell commands):
@@ -46,7 +46,7 @@
Introduction
------------
-Mercurial http://www.selenic.com/mercurial belongs to source code
+Mercurial https://www.mercurial-scm.org belongs to source code
management systems that follow the so-called paradigm of "distributed
version control". This means plain revision control without the
legacy of CVS or SVN (and without the extra complexity introduced by
--- a/etc/options Wed Jun 06 11:12:37 2018 +0200
+++ b/etc/options Wed Jun 06 13:04:52 2018 +0200
@@ -156,7 +156,7 @@
public option editor_output_delay : real = 0.1
-- "delay for prover output (markup, common messages etc.)"
-public option editor_consolidate_delay : real = 2.5
+public option editor_consolidate_delay : real = 2.0
-- "delay to consolidate status of command evaluation (execution forks)"
public option editor_prune_delay : real = 15
--- a/etc/settings Wed Jun 06 11:12:37 2018 +0200
+++ b/etc/settings Wed Jun 06 13:04:52 2018 +0200
@@ -134,5 +134,8 @@
ISABELLE_GNUPLOT="gnuplot"
#ISABELLE_GHC="/usr/bin/ghc"
+#ISABELLE_MLTON="/usr/bin/mlton"
#ISABELLE_OCAML="/usr/bin/ocaml"
+#ISABELLE_OCAMLC="/usr/bin/ocamlc"
+#ISABELLE_SMLNJ="/usr/bin/sml"
#ISABELLE_SWIPL="/usr/bin/swipl"
--- a/src/Doc/JEdit/JEdit.thy Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy Wed Jun 06 13:04:52 2018 +0200
@@ -228,15 +228,12 @@
\<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
Options are:
- -A specify ancestor for base session image (default: parent)
- -B use base session image, with theories from other sessions
- -F focus on selected logic session: ignore unrelated theories
+ -A NAME ancestor session for options -R and -S (default: parent)
-D NAME=X set JVM system property
-J OPTION add JVM runtime option
(default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
- -P use parent session image
- -R open ROOT entry of logic session
- -S NAME edit specified logic session, abbreviates -B -F -R -l NAME
+ -R NAME build image with requirements from other sessions
+ -S NAME like option -R, with focus on selected session
-b build only
-d DIR include session directory
-f fresh build
@@ -261,18 +258,15 @@
The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
session image.
- Option \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-B\<close> and are mutually exclusive and modify the meaning of
- option \<^verbatim>\<open>-l\<close> as follows. Option \<^verbatim>\<open>-P\<close> opens the parent session image. Option
- \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on the required theory
- imports from other sessions, relative to an ancestor session given by option
- \<^verbatim>\<open>-A\<close> (default: parent session).
+ Option \<^verbatim>\<open>-R\<close> builds an auxiliary logic image with all required theories from
+ \<^emph>\<open>other\<close> sessions, relative to an ancestor session given by option \<^verbatim>\<open>-A\<close>
+ (default: parent session). Option \<^verbatim>\<open>-R\<close> also opens the session \<^verbatim>\<open>ROOT\<close> entry
+ in the editor, to facilitate editing of the main session.
- Option \<^verbatim>\<open>-F\<close> focuses on the effective logic session: the accessible
- namespace of theories is restricted to sessions that are connected to it.
-
- Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
- editor. Option \<^verbatim>\<open>-S\<close> sets up the development environment to edit the
- specified session: it abbreviates \<^verbatim>\<open>-B\<close> \<^verbatim>\<open>-F\<close> \<^verbatim>\<open>-R\<close> \<^verbatim>\<open>-l\<close>.
+ Option \<^verbatim>\<open>-S\<close> is like \<^verbatim>\<open>-R\<close>, with a focus on the selected session and its
+ descendants: the namespace of accessible theories is restricted accordingly.
+ This reduces startup time for big projects, notably the ``Archive of Formal
+ Proofs''.
The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
Note that the system option @{system_option_ref jedit_print_mode} allows to
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Jun 06 11:12:37 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Jun 06 13:04:52 2018 +0200
@@ -6005,7 +6005,7 @@
shows "f holomorphic_on S"
proof -
{ fix z
- assume "z \<in> S" and cdf: "\<And>x. x\<in>S - K \<Longrightarrow> f field_differentiable at x"
+ assume "z \<in> S" and cdf: "\<And>x. x \<in> S - K \<Longrightarrow> f field_differentiable at x"
have "f field_differentiable at z"
proof (cases "z \<in> K")
case False then show ?thesis by (blast intro: cdf \<open>z \<in> S\<close>)
@@ -6018,14 +6018,15 @@
using S \<open>z \<in> S\<close> by (force simp: open_contains_ball)
have fde: "continuous_on (ball z (min d e)) f"
by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
+ have cont: "{a,b,c} \<subseteq> ball z (min d e) \<Longrightarrow> continuous_on (convex hull {a, b, c}) f" for a b c
+ by (simp add: hull_minimal continuous_on_subset [OF fde])
+ have fd: "\<lbrakk>{a,b,c} \<subseteq> ball z (min d e); x \<in> interior (convex hull {a, b, c}) - K\<rbrakk>
+ \<Longrightarrow> f field_differentiable at x" for a b c x
+ by (metis cdf Diff_iff Int_iff ball_min_Int subsetD convex_ball e interior_mono interior_subset subset_hull)
obtain g where "\<And>w. w \<in> ball z (min d e) \<Longrightarrow> (g has_field_derivative f w) (at w within ball z (min d e))"
- apply (rule contour_integral_convex_primitive [OF convex_ball fde])
- apply (rule Cauchy_theorem_triangle_cofinite [OF _ K])
- apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset)
- apply (rule cdf)
- apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset
- interior_mono interior_subset subset_hull)
- by auto
+ apply (rule contour_integral_convex_primitive
+ [OF convex_ball fde Cauchy_theorem_triangle_cofinite [OF _ K]])
+ using cont fd by auto
then have "f holomorphic_on ball z (min d e)"
by (metis open_ball at_within_open derivative_is_holomorphic)
then show ?thesis
@@ -6061,20 +6062,21 @@
qed
proposition Cauchy_integral_formula_convex:
- assumes S: "convex S" and K: "finite K" and contf: "continuous_on S f"
- and fcd: "(\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x)"
- and z: "z \<in> interior S" and vpg: "valid_path \<gamma>"
- and pasz: "path_image \<gamma> \<subseteq> S - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
- shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
- apply (rule Cauchy_integral_formula_weak [OF S finite.emptyI contf])
- apply (simp add: holomorphic_on_open [symmetric] field_differentiable_def)
- using no_isolated_singularity [where S = "interior S"]
- apply (metis K contf fcd holomorphic_on_open field_differentiable_def continuous_on_subset
- has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
- using assms
- apply auto
- done
-
+ assumes S: "convex S" and K: "finite K" and contf: "continuous_on S f"
+ and fcd: "(\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x)"
+ and z: "z \<in> interior S" and vpg: "valid_path \<gamma>"
+ and pasz: "path_image \<gamma> \<subseteq> S - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+ shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
+proof -
+ have *: "\<And>x. x \<in> interior S \<Longrightarrow> f field_differentiable at x"
+ unfolding holomorphic_on_open [symmetric] field_differentiable_def
+ using no_isolated_singularity [where S = "interior S"]
+ by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd
+ field_differentiable_at_within field_differentiable_def holomorphic_onI
+ holomorphic_on_imp_differentiable_at open_interior)
+ show ?thesis
+ by (rule Cauchy_integral_formula_weak [OF S finite.emptyI contf]) (use * assms in auto)
+qed
text\<open> Formula for higher derivatives.\<close>
@@ -6155,33 +6157,32 @@
and w: "w \<in> ball z r"
shows "((\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n) sums f w)"
proof -
- have fh': "f holomorphic_on cball z ((r + dist w z) / 2)"
- apply (rule holomorphic_on_subset [OF holf])
- apply (clarsimp simp del: divide_const_simps)
- apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w)
- done
- \<comment> \<open>Replacing @{term r} and the original (weak) premises\<close>
- obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
- apply (rule that [of "(r + dist w z) / 2"])
- apply (simp_all add: fh')
- apply (metis add_0_iff ball_eq_empty dist_nz dist_self empty_iff not_less pos_add_strict w)
- apply (metis add_less_cancel_right dist_commute mem_ball mult_2_right w)
- done
- then have holf: "f holomorphic_on ball z r" and contf: "continuous_on (cball z r) f"
- using ball_subset_cball holomorphic_on_subset apply blast
+ \<comment> \<open>Replacing @{term r} and the original (weak) premises with stronger ones\<close>
+ obtain r where "r > 0" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
+ proof
+ have "cball z ((r + dist w z) / 2) \<subseteq> ball z r"
+ using w by (simp add: dist_commute real_sum_of_halves subset_eq)
+ then show "f holomorphic_on cball z ((r + dist w z) / 2)"
+ by (rule holomorphic_on_subset [OF holf])
+ have "r > 0"
+ using w by clarsimp (metis dist_norm le_less_trans norm_ge_zero)
+ then show "0 < (r + dist w z) / 2"
+ by simp (use zero_le_dist [of w z] in linarith)
+ qed (use w in \<open>auto simp: dist_commute\<close>)
+ then have holf: "f holomorphic_on ball z r"
+ using ball_subset_cball holomorphic_on_subset by blast
+ have contf: "continuous_on (cball z r) f"
by (simp add: holfc holomorphic_on_imp_continuous_on)
have cint: "\<And>k. (\<lambda>u. f u / (u - z) ^ Suc k) contour_integrable_on circlepath z r"
- apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf])
- apply (simp add: \<open>0 < r\<close>)
- done
+ by (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf]) (simp add: \<open>0 < r\<close>)
obtain B where "0 < B" and B: "\<And>u. u \<in> cball z r \<Longrightarrow> norm(f u) \<le> B"
by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> norm(u - w)"
- apply (rule_tac k = "r - dist z w" in that)
- using w
- apply (auto simp: dist_norm norm_minus_commute)
- by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
+ proof
+ show "\<And>u. cmod (u - z) = r \<Longrightarrow> r - dist z w \<le> cmod (u - w)"
+ by (metis add_diff_eq diff_add_cancel dist_norm norm_diff_ineq)
+ qed (use w in \<open>auto simp: dist_norm norm_minus_commute\<close>)
have ul: "uniform_limit (sphere z r) (\<lambda>n x. (\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k))) (\<lambda>x. f x / (x - w)) sequentially"
unfolding uniform_limit_iff dist_norm
proof clarify
@@ -6239,16 +6240,14 @@
using contour_integrable_lmul [OF cint, of "(w - z) ^ a" for a] apply (simp add: field_simps)
apply (simp only: contour_integral_lmul cint algebra_simps)
done
+ have cic: "\<And>u. (\<lambda>y. \<Sum>k<u. (w - z) ^ k * (f y / (y - z) ^ Suc k)) contour_integrable_on circlepath z r"
+ apply (intro contour_integrable_sum contour_integrable_lmul, simp)
+ using \<open>0 < r\<close> by (force intro!: Cauchy_higher_derivative_integral_circlepath [OF contf holf])
have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
sums contour_integral (circlepath z r) (\<lambda>u. f u/(u - w))"
unfolding sums_def
- apply (rule Lim_transform_eventually [OF eq])
- apply (rule contour_integral_uniform_limit_circlepath [OF eventuallyI ul])
- apply (rule contour_integrable_sum, simp)
- apply (rule contour_integrable_lmul)
- apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf])
- using \<open>0 < r\<close>
- apply auto
+ apply (intro Lim_transform_eventually [OF eq] contour_integral_uniform_limit_circlepath [OF eventuallyI ul] cic)
+ using \<open>0 < r\<close> apply auto
done
then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
sums (2 * of_real pi * \<i> * f w)"
@@ -6288,16 +6287,12 @@
apply (rule Cauchy_integral_circlepath)
using \<open>R > 0\<close> apply (auto intro: holomorphic_on_subset [OF holf] holomorphic_on_imp_continuous_on)+
done
- have "cmod (x - z) = R \<Longrightarrow> cmod (f x) * 2 \<le> cmod (f z)" for x
- apply (simp add: R_def)
- apply (rule less_imp_le)
- apply (rule B)
- using norm_triangle_ineq4 [of x z]
- apply auto
- done
- with \<open>R > 0\<close> fz show False
+ have "cmod (x - z) = R \<Longrightarrow> cmod (f x) * 2 < cmod (f z)" for x
+ unfolding R_def
+ by (rule B) (use norm_triangle_ineq4 [of x z] in auto)
+ with \<open>R > 0\<close> fz show False
using has_contour_integral_bound_circlepath [OF *, of "norm(f z)/2/R"]
- by (auto simp: norm_mult norm_divide divide_simps)
+ by (auto simp: less_imp_le norm_mult norm_divide divide_simps)
qed
proposition Liouville_weak:
@@ -6342,7 +6337,7 @@
assume i: "i \<in> {1..n}" and nz: "a i \<noteq> 0"
have 1: "(\<lambda>z. \<Sum>i\<le>n. a i * z^i) holomorphic_on UNIV"
by (rule holomorphic_intros)+
- show ?thesis
+ show thesis
apply (rule Liouville_weak_inverse [OF 1])
apply (rule polyfun_extremal)
apply (rule nz)
--- a/src/HOL/HOLCF/Bifinite.thy Wed Jun 06 11:12:37 2018 +0200
+++ b/src/HOL/HOLCF/Bifinite.thy Wed Jun 06 13:04:52 2018 +0200
@@ -112,18 +112,21 @@
by (rule chainI, simp add: monofun_cfun monofun_LAM)
lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
-apply (rule cfun_eqI)
-apply (simp add: contlub_cfun_fun)
-apply (simp add: discr_approx_def)
-apply (case_tac x, simp)
-apply (rule lub_eqI)
-apply (rule is_lubI)
-apply (rule ub_rangeI, simp)
-apply (drule ub_rangeD)
-apply (erule rev_below_trans)
-apply simp
-apply (rule lessI)
-done
+ apply (rule cfun_eqI)
+ apply (simp add: contlub_cfun_fun)
+ apply (simp add: discr_approx_def)
+ subgoal for x
+ apply (cases x)
+ apply simp
+ apply (rule lub_eqI)
+ apply (rule is_lubI)
+ apply (rule ub_rangeI, simp)
+ apply (drule ub_rangeD)
+ apply (erule rev_below_trans)
+ apply simp
+ apply (rule lessI)
+ done
+ done
lemma inj_on_undiscr [simp]: "inj_on undiscr A"
using Discr_undiscr by (rule inj_on_inverseI)
@@ -203,14 +206,21 @@
definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
-unfolding encode_prod_u_def decode_prod_u_def
-by (case_tac x, simp, rename_tac y, case_tac y, simp)
+ unfolding encode_prod_u_def decode_prod_u_def
+ apply (cases x)
+ apply simp
+ subgoal for y by (cases y) simp
+ done
lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
-unfolding encode_prod_u_def decode_prod_u_def
-apply (case_tac y, simp, rename_tac a b)
-apply (case_tac a, simp, case_tac b, simp, simp)
-done
+ unfolding encode_prod_u_def decode_prod_u_def
+ apply (cases y)
+ apply simp
+ subgoal for a b
+ apply (cases a, simp)
+ apply (cases b, simp, simp)
+ done
+ done
instance prod :: (profinite, profinite) profinite
proof
--- a/src/HOL/HOLCF/Cfun.thy Wed Jun 06 11:12:37 2018 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Wed Jun 06 13:04:52 2018 +0200
@@ -394,7 +394,7 @@
lemma flat_codom: "f\<cdot>x = c \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
for c :: "'b::flat"
- apply (case_tac "f\<cdot>x = \<bottom>")
+ apply (cases "f\<cdot>x = \<bottom>")
apply (rule disjI1)
apply (rule bottomI)
apply (erule_tac t="\<bottom>" in subst)
--- a/src/HOL/HOLCF/Completion.thy Wed Jun 06 11:12:37 2018 +0200
+++ b/src/HOL/HOLCF/Completion.thy Wed Jun 06 13:04:52 2018 +0200
@@ -41,13 +41,13 @@
unfolding ideal_def by fast
lemma ideal_principal: "ideal {x. x \<preceq> z}"
-apply (rule idealI)
-apply (rule_tac x=z in exI)
-apply (fast intro: r_refl)
-apply (rule_tac x=z in bexI, fast)
-apply (fast intro: r_refl)
-apply (fast intro: r_trans)
-done
+ apply (rule idealI)
+ apply (rule exI [where x = z])
+ apply (fast intro: r_refl)
+ apply (rule bexI [where x = z], fast)
+ apply (fast intro: r_refl)
+ apply (fast intro: r_trans)
+ done
lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}"
by (fast intro: ideal_principal)
@@ -59,17 +59,19 @@
assumes ideal_A: "\<And>i. ideal (A i)"
assumes chain_A: "\<And>i j. i \<le> j \<Longrightarrow> A i \<subseteq> A j"
shows "ideal (\<Union>i. A i)"
- apply (rule idealI)
- apply (cut_tac idealD1 [OF ideal_A], fast)
- apply (clarify, rename_tac i j)
- apply (drule subsetD [OF chain_A [OF max.cobounded1]])
- apply (drule subsetD [OF chain_A [OF max.cobounded2]])
- apply (drule (1) idealD2 [OF ideal_A])
- apply blast
- apply clarify
- apply (drule (1) idealD3 [OF ideal_A])
- apply fast
-done
+ apply (rule idealI)
+ using idealD1 [OF ideal_A] apply fast
+ apply (clarify)
+ subgoal for i j
+ apply (drule subsetD [OF chain_A [OF max.cobounded1]])
+ apply (drule subsetD [OF chain_A [OF max.cobounded2]])
+ apply (drule (1) idealD2 [OF ideal_A])
+ apply blast
+ done
+ apply clarify
+ apply (drule (1) idealD3 [OF ideal_A])
+ apply fast
+ done
lemma typedef_ideal_po:
fixes Abs :: "'a set \<Rightarrow> 'b::below"
@@ -208,10 +210,10 @@
have a_mem: "enum a \<in> rep x"
unfolding a_def
apply (rule LeastI_ex)
- apply (cut_tac ideal_rep [of x])
+ apply (insert ideal_rep [of x])
apply (drule idealD1)
- apply (clarify, rename_tac a)
- apply (rule_tac x="count a" in exI, simp)
+ apply (clarify)
+ subgoal for a by (rule exI [where x="count a"]) simp
done
have b: "\<And>i. P i \<Longrightarrow> enum i \<in> rep x
\<Longrightarrow> enum (b i) \<in> rep x \<and> \<not> enum (b i) \<preceq> enum i"
@@ -220,50 +222,63 @@
\<Longrightarrow> enum (c i j) \<in> rep x \<and> enum i \<preceq> enum (c i j) \<and> enum j \<preceq> enum (c i j)"
unfolding c_def
apply (drule (1) idealD2 [OF ideal_rep], clarify)
- apply (rule_tac a="count z" in LeastI2, simp, simp)
+ subgoal for \<dots> z by (rule LeastI2 [where a="count z"], simp, simp)
done
- have X_mem: "\<And>n. enum (X n) \<in> rep x"
- apply (induct_tac n)
- apply (simp add: X_0 a_mem)
- apply (clarsimp simp add: X_Suc, rename_tac n)
- apply (simp add: b c)
- done
+ have X_mem: "enum (X n) \<in> rep x" for n
+ proof (induct n)
+ case 0
+ then show ?case by (simp add: X_0 a_mem)
+ next
+ case (Suc n)
+ with b c show ?case by (auto simp: X_Suc)
+ qed
have X_chain: "\<And>n. enum (X n) \<preceq> enum (X (Suc n))"
apply (clarsimp simp add: X_Suc r_refl)
apply (simp add: b c X_mem)
done
have less_b: "\<And>n i. n < b i \<Longrightarrow> enum n \<in> rep x \<Longrightarrow> enum n \<preceq> enum i"
unfolding b_def by (drule not_less_Least, simp)
- have X_covers: "\<And>n. \<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)"
- apply (induct_tac n)
- apply (clarsimp simp add: X_0 a_def)
- apply (drule_tac k=0 in Least_le, simp add: r_refl)
- apply (clarsimp, rename_tac n k)
- apply (erule le_SucE)
- apply (rule r_trans [OF _ X_chain], simp)
- apply (case_tac "P (X n)", simp add: X_Suc)
- apply (rule_tac x="b (X n)" and y="Suc n" in linorder_cases)
- apply (simp only: less_Suc_eq_le)
- apply (drule spec, drule (1) mp, simp add: b X_mem)
- apply (simp add: c X_mem)
- apply (drule (1) less_b)
- apply (erule r_trans)
- apply (simp add: b c X_mem)
- apply (simp add: X_Suc)
- apply (simp add: P_def)
- done
+ have X_covers: "\<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)" for n
+ proof (induct n)
+ case 0
+ then show ?case
+ apply (clarsimp simp add: X_0 a_def)
+ apply (drule Least_le [where k=0], simp add: r_refl)
+ done
+ next
+ case (Suc n)
+ then show ?case
+ apply clarsimp
+ apply (erule le_SucE)
+ apply (rule r_trans [OF _ X_chain], simp)
+ apply (cases "P (X n)", simp add: X_Suc)
+ apply (rule linorder_cases [where x="b (X n)" and y="Suc n"])
+ apply (simp only: less_Suc_eq_le)
+ apply (drule spec, drule (1) mp, simp add: b X_mem)
+ apply (simp add: c X_mem)
+ apply (drule (1) less_b)
+ apply (erule r_trans)
+ apply (simp add: b c X_mem)
+ apply (simp add: X_Suc)
+ apply (simp add: P_def)
+ done
+ qed
have 1: "\<forall>i. enum (X i) \<preceq> enum (X (Suc i))"
by (simp add: X_chain)
- have 2: "x = (\<Squnion>n. principal (enum (X n)))"
+ have "x = (\<Squnion>n. principal (enum (X n)))"
apply (simp add: eq_iff rep_lub 1 rep_principal)
- apply (auto, rename_tac a)
- apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
- apply (rule_tac x=i in exI, simp add: X_covers)
- apply (rule_tac x="count a" in exI, simp)
- apply (erule idealD3 [OF ideal_rep])
- apply (rule X_mem)
+ apply auto
+ subgoal for a
+ apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
+ apply (rule_tac x=i in exI, simp add: X_covers)
+ apply (rule_tac x="count a" in exI, simp)
+ done
+ subgoal
+ apply (erule idealD3 [OF ideal_rep])
+ apply (rule X_mem)
+ done
done
- from 1 2 show ?thesis ..
+ with 1 show ?thesis ..
qed
lemma principal_induct:
@@ -301,16 +316,20 @@
by (simp add: x rep_lub Y rep_principal)
have "f ` rep x <<| (\<Squnion>n. f (Y n))"
apply (rule is_lubI)
- apply (rule ub_imageI, rename_tac a)
- apply (clarsimp simp add: rep_x)
- apply (drule f_mono)
- apply (erule below_lub [OF chain])
+ apply (rule ub_imageI)
+ subgoal for a
+ apply (clarsimp simp add: rep_x)
+ apply (drule f_mono)
+ apply (erule below_lub [OF chain])
+ done
apply (rule lub_below [OF chain])
- apply (drule_tac x="Y n" in ub_imageD)
- apply (simp add: rep_x, fast intro: r_refl)
- apply assumption
+ subgoal for \<dots> n
+ apply (drule ub_imageD [where x="Y n"])
+ apply (simp add: rep_x, fast intro: r_refl)
+ apply assumption
+ done
done
- thus ?thesis ..
+ then show ?thesis ..
qed
lemma extension_beta:
@@ -353,16 +372,18 @@
assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
assumes below: "\<And>a. f a \<sqsubseteq> g a"
shows "extension f \<sqsubseteq> extension g"
- apply (rule cfun_belowI)
- apply (simp only: extension_beta f_mono g_mono)
- apply (rule is_lub_thelub_ex)
- apply (rule extension_lemma, erule f_mono)
- apply (rule ub_imageI, rename_tac a)
- apply (rule below_trans [OF below])
- apply (rule is_ub_thelub_ex)
- apply (rule extension_lemma, erule g_mono)
- apply (erule imageI)
-done
+ apply (rule cfun_belowI)
+ apply (simp only: extension_beta f_mono g_mono)
+ apply (rule is_lub_thelub_ex)
+ apply (rule extension_lemma, erule f_mono)
+ apply (rule ub_imageI)
+ subgoal for x a
+ apply (rule below_trans [OF below])
+ apply (rule is_ub_thelub_ex)
+ apply (rule extension_lemma, erule g_mono)
+ apply (erule imageI)
+ done
+ done
lemma cont_extension:
assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b"
--- a/src/HOL/HOLCF/Domain_Aux.thy Wed Jun 06 11:12:37 2018 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy Wed Jun 06 13:04:52 2018 +0200
@@ -199,32 +199,40 @@
assumes f: "decisive f"
assumes g: "decisive g"
shows "decisive (ssum_map\<cdot>f\<cdot>g)"
-apply (rule decisiveI, rename_tac s)
-apply (case_tac s, simp_all)
-apply (rule_tac x=x in decisive_cases [OF f], simp_all)
-apply (rule_tac x=y in decisive_cases [OF g], simp_all)
-done
+ apply (rule decisiveI)
+ subgoal for s
+ apply (cases s, simp_all)
+ apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+ apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+ done
+ done
lemma decisive_sprod_map:
assumes f: "decisive f"
assumes g: "decisive g"
shows "decisive (sprod_map\<cdot>f\<cdot>g)"
-apply (rule decisiveI, rename_tac s)
-apply (case_tac s, simp_all)
-apply (rule_tac x=x in decisive_cases [OF f], simp_all)
-apply (rule_tac x=y in decisive_cases [OF g], simp_all)
-done
+ apply (rule decisiveI)
+ subgoal for s
+ apply (cases s, simp)
+ subgoal for x y
+ apply (rule decisive_cases [OF f, where x = x], simp_all)
+ apply (rule decisive_cases [OF g, where x = y], simp_all)
+ done
+ done
+ done
lemma decisive_abs_rep:
fixes abs rep
assumes iso: "iso abs rep"
assumes d: "decisive d"
shows "decisive (abs oo d oo rep)"
-apply (rule decisiveI)
-apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
-apply (simp add: iso.rep_iso [OF iso])
-apply (simp add: iso.abs_strict [OF iso])
-done
+ apply (rule decisiveI)
+ subgoal for s
+ apply (rule decisive_cases [OF d, where x="rep\<cdot>s"])
+ apply (simp add: iso.rep_iso [OF iso])
+ apply (simp add: iso.abs_strict [OF iso])
+ done
+ done
lemma lub_ID_finite:
assumes chain: "chain d"
--- a/src/HOL/HOLCF/Pcpo.thy Wed Jun 06 11:12:37 2018 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy Wed Jun 06 13:04:52 2018 +0200
@@ -198,16 +198,20 @@
begin
subclass chfin
- apply standard
- apply (unfold max_in_chain_def)
- apply (case_tac "\<forall>i. Y i = \<bottom>")
- apply simp
- apply simp
- apply (erule exE)
- apply (rule_tac x="i" in exI)
- apply clarify
- apply (blast dest: chain_mono ax_flat)
- done
+proof
+ fix Y
+ assume *: "chain Y"
+ show "\<exists>n. max_in_chain n Y"
+ apply (unfold max_in_chain_def)
+ apply (cases "\<forall>i. Y i = \<bottom>")
+ apply simp
+ apply simp
+ apply (erule exE)
+ apply (rule_tac x="i" in exI)
+ apply clarify
+ using * apply (blast dest: chain_mono ax_flat)
+ done
+qed
lemma flat_below_iff: "x \<sqsubseteq> y \<longleftrightarrow> x = \<bottom> \<or> x = y"
by (safe dest!: ax_flat)
--- a/src/Pure/Admin/build_cygwin.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/Admin/build_cygwin.scala Wed Jun 06 13:04:52 2018 +0200
@@ -9,7 +9,7 @@
object Build_Cygwin
{
- val default_mirror: String = "http://isabelle.in.tum.de/cygwin_2017"
+ val default_mirror: String = "https://isabelle.sketis.net/cygwin_2018"
val packages: List[String] =
List("curl", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip")
@@ -33,6 +33,8 @@
try { Bytes.read(Url(cygwin_exe_name)) }
catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) })
+ File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror)
+
Isabelle_System.bash(
"chmod +x " + File.bash_path(cygwin_exe) + " && " +
File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Jun 06 13:04:52 2018 +0200
@@ -252,7 +252,6 @@
Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
-
val remote_builds1: List[List[Remote_Build]] =
{
List(
@@ -260,6 +259,12 @@
options = "-m32 -B -M1x2,2", args = "-N -g timing")),
List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
+ List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
+ options = "-m32 -B -M1x2,2 -t Benchmarks" +
+ " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
+ " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=sml -e ISABELLE_SWIPL=swipl",
+ args = "-N -a -d '~~/src/Benchmarks'",
+ detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))),
List(
Remote_Build("Mac OS X", "macbroy2",
options = "-m32 -M8" +
--- a/src/Pure/Concurrent/future.ML Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Jun 06 13:04:52 2018 +0200
@@ -692,9 +692,10 @@
(* snapshot: current tasks of groups *)
-fun snapshot groups =
- SYNCHRONIZED "snapshot" (fn () =>
- Task_Queue.group_tasks (! queue) groups);
+fun snapshot [] = []
+ | snapshot groups =
+ SYNCHRONIZED "snapshot" (fn () =>
+ Task_Queue.group_tasks (! queue) groups);
(* shutdown *)
--- a/src/Pure/PIDE/command.ML Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/command.ML Wed Jun 06 13:04:52 2018 +0200
@@ -26,6 +26,7 @@
val print0: {pri: int, print_fn: print_fn} -> eval -> print
val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
eval -> print list -> print list option
+ val parallel_print: print -> bool
type print_function =
{keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
{delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
@@ -36,6 +37,7 @@
val no_exec: exec
val exec_ids: exec option -> Document_ID.exec list
val exec: Document_ID.execution -> exec -> unit
+ val exec_parallel_prints: Document_ID.execution -> Future.task list -> exec -> exec option
end;
structure Command: COMMAND =
@@ -386,6 +388,9 @@
if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
end;
+fun parallel_print (Print {pri, ...}) =
+ pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print");
+
fun print_function name f =
Synchronized.change print_functions (fn funs =>
(if name = "" then error "Unnamed print function" else ();
@@ -448,23 +453,24 @@
if Lazy.is_finished eval_process then ()
else run_process execution_id exec_id eval_process;
-fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) =
+fun fork_print execution_id deps (Print {name, delay, pri, exec_id, print_process, ...}) =
+ let
+ val group = Future.worker_subgroup ();
+ fun fork () =
+ ignore ((singleton o Future.forks)
+ {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true}
+ (fn () =>
+ if ignore_process print_process then ()
+ else run_process execution_id exec_id print_process));
+ in
+ (case delay of
+ NONE => fork ()
+ | SOME d => ignore (Event_Timer.request (Time.now () + d) fork))
+ end;
+
+fun run_print execution_id (print as Print {exec_id, print_process, ...}) =
if ignore_process print_process then ()
- else if pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print")
- then
- let
- val group = Future.worker_subgroup ();
- fun fork () =
- ignore ((singleton o Future.forks)
- {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
- (fn () =>
- if ignore_process print_process then ()
- else run_process execution_id exec_id print_process));
- in
- (case delay of
- NONE => fork ()
- | SOME d => ignore (Event_Timer.request (Time.now () + d) fork))
- end
+ else if parallel_print print then fork_print execution_id [] print
else run_process execution_id exec_id print_process;
in
@@ -472,7 +478,11 @@
fun exec execution_id (eval, prints) =
(run_eval execution_id eval; List.app (run_print execution_id) prints);
+fun exec_parallel_prints execution_id deps (exec as (Eval {eval_process, ...}, prints)) =
+ if Lazy.is_finished eval_process
+ then (List.app (fork_print execution_id deps) prints; NONE)
+ else SOME exec;
+
end;
end;
-
--- a/src/Pure/PIDE/command.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/command.scala Wed Jun 06 13:04:52 2018 +0200
@@ -263,6 +263,8 @@
def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
+ lazy val maybe_consolidated: Boolean = Protocol.maybe_consolidated(status)
+
lazy val protocol_status: Protocol.Status =
{
val warnings =
--- a/src/Pure/PIDE/document.ML Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/document.ML Wed Jun 06 13:04:52 2018 +0200
@@ -24,7 +24,7 @@
val command_exec: state -> string -> Document_ID.command -> Command.exec option
val remove_versions: Document_ID.version list -> state -> state
val start_execution: state -> state
- val update: Document_ID.version -> Document_ID.version -> edit list -> bool -> state ->
+ val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
val state: unit -> state
val change_state: (state -> state) -> unit
@@ -314,17 +314,20 @@
type execution =
{version_id: Document_ID.version, (*static version id*)
execution_id: Document_ID.execution, (*dynamic execution id*)
- delay_request: unit future}; (*pending event timer request*)
+ delay_request: unit future, (*pending event timer request*)
+ parallel_prints: Command.exec list}; (*parallel prints for early execution*)
val no_execution: execution =
{version_id = Document_ID.none,
execution_id = Document_ID.none,
- delay_request = Future.value ()};
+ delay_request = Future.value (),
+ parallel_prints = []};
-fun new_execution version_id delay_request : execution =
+fun new_execution version_id delay_request parallel_prints : execution =
{version_id = version_id,
execution_id = Execution.start (),
- delay_request = delay_request};
+ delay_request = delay_request,
+ parallel_prints = parallel_prints};
abstype state = State of
{versions: version Inttab.table, (*version id -> document content*)
@@ -347,12 +350,23 @@
(* document versions *)
-fun define_version version_id version =
+fun parallel_prints_node node =
+ iterate_entries (fn (_, opt_exec) => fn rev_result =>
+ (case opt_exec of
+ SOME (eval, prints) =>
+ (case filter Command.parallel_print prints of
+ [] => SOME rev_result
+ | prints' => SOME ((eval, prints') :: rev_result))
+ | NONE => NONE)) node [] |> rev;
+
+fun define_version version_id version assigned_nodes =
map_state (fn (versions, blobs, commands, {delay_request, ...}) =>
let
- val versions' = Inttab.update_new (version_id, version) versions
+ val version' = fold put_node assigned_nodes version;
+ val versions' = Inttab.update_new (version_id, version') versions
handle Inttab.DUP dup => err_dup "document version" dup;
- val execution' = new_execution version_id delay_request;
+ val parallel_prints = maps (parallel_prints_node o #2) assigned_nodes;
+ val execution' = new_execution version_id delay_request parallel_prints;
in (versions', blobs, commands, execution') end);
fun the_version (State {versions, ...}) version_id =
@@ -479,12 +493,16 @@
fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
timeit "Document.start_execution" (fn () =>
let
- val {version_id, execution_id, delay_request} = execution;
+ val {version_id, execution_id, delay_request, parallel_prints} = execution;
val delay = seconds (Options.default_real "editor_execution_delay");
val _ = Future.cancel delay_request;
val delay_request' = Event_Timer.future (Time.now () + delay);
+ val delay = Future.task_of delay_request';
+
+ val parallel_prints' = parallel_prints
+ |> map_filter (Command.exec_parallel_prints execution_id [delay]);
fun finished_import (name, (node, _)) =
finished_result node orelse is_some (Thy_Info.lookup_theory name);
@@ -497,7 +515,7 @@
if Symtab.defined required name orelse visible_node node orelse pending_result node then
let
fun body () =
- (Execution.worker_task_active true;
+ (Execution.worker_task_active true name;
if forall finished_import deps then
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
@@ -507,23 +525,22 @@
else NONE
| NONE => NONE)) node ()
else ();
- Execution.worker_task_active false)
+ Execution.worker_task_active false name)
handle exn =>
(Output.system_message (Runtime.exn_message exn);
- Execution.worker_task_active false;
+ Execution.worker_task_active false name;
Exn.reraise exn);
val future =
(singleton o Future.forks)
{name = "theory:" ^ name,
group = SOME (Future.new_group NONE),
- deps =
- Future.task_of delay_request' :: Execution.active_tasks name @
- maps (the_list o #2 o #2) deps,
+ deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
pri = 0, interrupts = false} body;
in (node, SOME (Future.task_of future)) end
else (node, NONE));
val execution' =
- {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
+ {version_id = version_id, execution_id = execution_id,
+ delay_request = delay_request', parallel_prints = parallel_prints'};
in (versions, blobs, commands, execution') end));
@@ -672,13 +689,16 @@
(case finished_result_theory node of
SOME (result_id, thy) =>
let
- val eval_ids =
- iterate_entries (fn (_, opt_exec) => fn eval_ids =>
- (case opt_exec of
- SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
- | NONE => NONE)) node [];
+ val active_tasks =
+ (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active =>
+ if active then NONE
+ else
+ (case opt_exec of
+ NONE => NONE
+ | SOME (eval, _) =>
+ SOME (not (null (Execution.snapshot [Command.eval_exec_id eval])))));
in
- if null (Execution.snapshot eval_ids) then
+ if not active_tasks then
let
val consolidation =
if Options.bool options "editor_presentation" then
@@ -748,6 +768,7 @@
timeit "Document.edit_nodes"
(fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
+ val consolidate = Symtab.defined (Symtab.make_set consolidate);
val nodes = nodes_of new_version;
val required = make_required nodes;
val required0 = make_required (nodes_of old_version);
@@ -766,7 +787,7 @@
val root_theory = check_root_theory node;
val keywords = the_default (Session.get_keywords ()) (get_keywords node);
- val maybe_consolidate = consolidate andalso could_consolidate node;
+ val maybe_consolidate = consolidate name andalso could_consolidate node;
val imports = map (apsnd Future.join) deps;
val imports_result_changed = exists (#4 o #1 o #2) imports;
val node_required = Symtab.defined required name;
@@ -838,7 +859,7 @@
val assigned_nodes = map_filter #3 updated;
val state' = state
- |> define_version new_version_id (fold put_node assigned_nodes new_version);
+ |> define_version new_version_id new_version assigned_nodes;
in (removed, assign_result, state') end);
--- a/src/Pure/PIDE/document.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/document.scala Wed Jun 06 13:04:52 2018 +0200
@@ -537,6 +537,8 @@
def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
+ def messages: List[(XML.Tree, Position.T)]
+ def exports: List[Export.Entry]
def find_command(id: Document_ID.Generic): Option[(Node, Command)]
def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
@@ -847,6 +849,18 @@
removing_versions = false)
}
+ def command_state_eval(version: Version, command: Command): Option[Command.State] =
+ {
+ require(is_assigned(version))
+ try {
+ the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
+ case eval_id :: _ => Some(the_dynamic_state(eval_id))
+ case Nil => None
+ }
+ }
+ catch { case _: State.Fail => None }
+ }
+
private def command_states_self(version: Version, command: Command)
: List[(Document_ID.Generic, Command.State)] =
{
@@ -928,6 +942,16 @@
case Some(command) => command_states(version, command).headOption.exists(_.initialized)
})
+ def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
+ name.is_theory &&
+ {
+ version.nodes(name).commands.reverse.iterator.forall(command =>
+ command_state_eval(version, command) match {
+ case None => false
+ case Some(st) => st.maybe_consolidated
+ })
+ }
+
def node_consolidated(version: Version, name: Node.Name): Boolean =
!name.is_theory ||
{
@@ -1006,6 +1030,22 @@
def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
state.markup_to_XML(version, node_name, range, elements)
+ def messages: List[(XML.Tree, Position.T)] =
+ (for {
+ (command, start) <-
+ Document.Node.Commands.starts_pos(
+ node.commands.iterator, Token.Pos.file(node_name.node))
+ pos = command.span.keyword_pos(start).position(command.span.name)
+ (_, tree) <- state.command_results(version, command).iterator
+ } yield (tree, pos)).toList
+
+ def exports: List[Export.Entry] =
+ Command.Exports.merge(
+ for {
+ command <- node.commands.iterator
+ st <- state.command_states(version, command).iterator
+ } yield st.exports).iterator.map(_._2).toList
+
/* find command */
--- a/src/Pure/PIDE/execution.ML Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/execution.ML Wed Jun 06 13:04:52 2018 +0200
@@ -115,8 +115,10 @@
SOME (groups, _) => groups
| NONE => []);
-fun snapshot exec_ids =
- change_state_result (`(fn (_, _, execs) => Future.snapshot (maps (exec_groups execs) exec_ids)));
+fun snapshot [] = []
+ | snapshot exec_ids =
+ change_state_result
+ (`(fn (_, _, execs) => Future.snapshot (maps (exec_groups execs) exec_ids)));
fun join exec_ids =
(case snapshot exec_ids of
--- a/src/Pure/PIDE/protocol.ML Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/protocol.ML Wed Jun 06 13:04:52 2018 +0200
@@ -74,7 +74,7 @@
val _ =
Isabelle_Process.protocol_command "Document.update"
(Future.task_context "Document.update" (Future.new_group NONE)
- (fn [old_id_string, new_id_string, edits_yxml, consolidate_string] =>
+ (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] =>
Document.change_state (fn state =>
let
val old_id = Document_ID.parse old_id_string;
@@ -100,7 +100,9 @@
Document.Perspective (bool_atom a, map int_atom b,
list (pair int (pair string (list string))) c)]))
end;
- val consolidate = Value.parse_bool consolidate_string;
+ val consolidate =
+ YXML.parse_body consolidate_yxml |>
+ let open XML.Decode in list string end;
val _ = Execution.discontinue ();
--- a/src/Pure/PIDE/protocol.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Jun 06 13:04:52 2018 +0200
@@ -38,6 +38,26 @@
}
+ /* consolidation status */
+
+ def maybe_consolidated(markups: List[Markup]): Boolean =
+ {
+ var touched = false
+ var forks = 0
+ var runs = 0
+ for (markup <- markups) {
+ markup.name match {
+ case Markup.FORKED => touched = true; forks += 1
+ case Markup.JOINED => forks -= 1
+ case Markup.RUNNING => touched = true; runs += 1
+ case Markup.FINISHED => runs -= 1
+ case _ =>
+ }
+ }
+ touched && forks == 0 && runs == 0
+ }
+
+
/* command status */
object Status
@@ -419,7 +439,7 @@
/* document versions */
def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
- edits: List[Document.Edit_Command], consolidate: Boolean)
+ edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
{
val edits_yxml =
{
@@ -446,9 +466,17 @@
val (name, edit) = node_edit
pair(string, encode_edit(name))(name.node, edit)
})
- Symbol.encode_yxml(encode_edits(edits)) }
+ Symbol.encode_yxml(encode_edits(edits))
+ }
+
+ val consolidate_yxml =
+ {
+ import XML.Encode._
+ Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
+ }
+
protocol_command(
- "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate.toString)
+ "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate_yxml)
}
def remove_versions(versions: List[Document.Version])
--- a/src/Pure/PIDE/resources.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/resources.scala Wed Jun 06 13:04:52 2018 +0200
@@ -216,7 +216,7 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text],
- consolidate: Boolean): Session.Change =
+ consolidate: List[Document.Node.Name]): Session.Change =
Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
def commit(change: Session.Change) { }
--- a/src/Pure/PIDE/session.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/PIDE/session.scala Wed Jun 06 13:04:52 2018 +0200
@@ -50,7 +50,7 @@
syntax_changed: List[Document.Node.Name],
deps_changed: Boolean,
doc_edits: List[Document.Edit_Command],
- consolidate: Boolean,
+ consolidate: List[Document.Node.Name],
version: Document.Version)
case object Change_Flush
@@ -231,7 +231,7 @@
previous: Future[Document.Version],
doc_blobs: Document.Blobs,
text_edits: List[Document.Edit_Text],
- consolidate: Boolean,
+ consolidate: List[Document.Node.Name],
version_result: Promise[Document.Version])
private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
@@ -259,6 +259,7 @@
def flush(): Unit = synchronized {
if (assignment || nodes.nonEmpty || commands.nonEmpty)
commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
+ if (nodes.nonEmpty) consolidation.update(nodes)
assignment = false
nodes = Set.empty
commands = Set.empty
@@ -299,6 +300,28 @@
}
+ /* node consolidation */
+
+ private object consolidation
+ {
+ private val delay =
+ Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
+
+ private val changed_nodes = Synchronized(Set.empty[Document.Node.Name])
+
+ def update(new_nodes: Set[Document.Node.Name] = Set.empty)
+ {
+ changed_nodes.change(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)
+ delay.invoke()
+ }
+
+ def flush(): Set[Document.Node.Name] =
+ changed_nodes.change_result(nodes => (nodes, Set.empty))
+
+ def revoke() { delay.revoke() }
+ }
+
+
/* prover process */
private object prover
@@ -347,7 +370,7 @@
def handle_raw_edits(
doc_blobs: Document.Blobs = Document.Blobs.empty,
edits: List[Document.Edit_Text] = Nil,
- consolidate: Boolean = false)
+ consolidate: List[Document.Node.Name] = Nil)
//{{{
{
require(prover.defined)
@@ -526,6 +549,7 @@
prover.set(start_prover(manager.send(_)))
case Stop =>
+ consolidation.revoke()
delay_prune.revoke()
if (prover.defined) {
protocol_handlers.exit()
@@ -534,7 +558,19 @@
}
case Consolidate_Execution =>
- if (prover.defined) handle_raw_edits(consolidate = true)
+ if (prover.defined) {
+ val state = global_state.value
+ state.stable_tip_version match {
+ case None => consolidation.update()
+ case Some(version) =>
+ val consolidate =
+ consolidation.flush().iterator.filter(name =>
+ !resources.session_base.loaded_theory(name) &&
+ !state.node_consolidated(version, name) &&
+ state.node_maybe_consolidated(version, name)).toList
+ if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate)
+ }
+ }
case Prune_History =>
if (prover.defined) {
@@ -581,28 +617,6 @@
}
}
- private val consolidator: Thread =
- Standard_Thread.fork("Session.consolidator", daemon = true) {
- try {
- while (true) {
- Thread.sleep(consolidate_delay.ms)
-
- val state = global_state.value
- state.stable_tip_version match {
- case None =>
- case Some(version) =>
- val consolidated =
- version.nodes.iterator.forall(
- { case (name, _) =>
- resources.session_base.loaded_theory(name) ||
- state.node_consolidated(version, name) })
- if (!consolidated) manager.send(Consolidate_Execution)
- }
- }
- }
- catch { case Exn.Interrupt() => }
- }
-
/* main operations */
@@ -641,8 +655,6 @@
change_parser.shutdown()
change_buffer.shutdown()
- consolidator.interrupt
- consolidator.join
manager.shutdown()
dispatcher.shutdown()
--- a/src/Pure/Thy/sessions.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Wed Jun 06 13:04:52 2018 +0200
@@ -394,21 +394,21 @@
progress: Progress = No_Progress,
dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
- ancestor_session: Option[String] = None,
- all_known: Boolean = false,
- focus_session: Boolean = false,
- required_session: Boolean = false): Base_Info =
+ session_ancestor: Option[String] = None,
+ session_requirements: Boolean = false,
+ session_focus: Boolean = false,
+ all_known: Boolean = false): Base_Info =
{
val full_sessions = load_structure(options, dirs = dirs)
val global_theories = full_sessions.global_theories
val selected_sessions =
- full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))
+ full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
val info = selected_sessions(session)
- val ancestor = ancestor_session orElse info.parent
+ val ancestor = session_ancestor orElse info.parent
val (session1, infos1) =
- if (required_session && ancestor.isDefined) {
+ if (session_requirements && ancestor.isDefined) {
val deps = Sessions.deps(selected_sessions, global_theories, progress = progress)
val base = deps(session)
@@ -430,7 +430,7 @@
if (required_theories.isEmpty) (ancestor.get, Nil)
else {
- val other_name = info.name + "_base(" + ancestor.get + ")"
+ val other_name = info.name + "_requirements(" + ancestor.get + ")"
(other_name,
List(
make_info(info.options,
@@ -461,7 +461,7 @@
{
val sel_sessions1 = session1 :: include_sessions
val select_sessions1 =
- if (focus_session) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
+ if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
full_sessions1.selection(Selection(sessions = select_sessions1))
}
--- a/src/Pure/Thy/thy_resources.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Wed Jun 06 13:04:52 2018 +0200
@@ -55,7 +55,7 @@
}
}
- sealed case class Theories_Result(
+ class Theories_Result private[Thy_Resources](
val state: Document.State,
val version: Document.Version,
val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
@@ -63,32 +63,11 @@
def node_names: List[Document.Node.Name] = nodes.map(_._1)
def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
- def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] =
+ def snapshot(node_name: Document.Node.Name): Document.Snapshot =
{
- val node = version.nodes(node_name)
- (for {
- (command, start) <-
- Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
- pos = command.span.keyword_pos(start).position(command.span.name)
- (_, tree) <- state.command_results(version, command).iterator
- } yield (tree, pos)).toList
- }
-
- def markup_to_XML(node_name: Document.Node.Name,
- range: Text.Range = Text.Range.full,
- elements: Markup.Elements = Markup.Elements.full): XML.Body =
- {
- state.markup_to_XML(version, node_name, range, elements)
- }
-
- def exports(node_name: Document.Node.Name): List[Export.Entry] =
- {
- val node = version.nodes(node_name)
- Command.Exports.merge(
- for {
- command <- node.commands.iterator
- st <- state.command_states(version, command).iterator
- } yield st.exports).iterator.map(_._2).toList
+ val snapshot = state.snapshot(node_name)
+ assert(version.id == snapshot.version.id)
+ snapshot
}
}
@@ -134,7 +113,7 @@
val nodes =
for (name <- dep_theories)
yield (name -> Protocol.node_status(state, version, name))
- try { result.fulfill(Theories_Result(state, version, nodes)) }
+ try { result.fulfill(new Theories_Result(state, version, nodes)) }
catch { case _: IllegalStateException => }
case _ =>
}
--- a/src/Pure/Thy/thy_syntax.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Jun 06 13:04:52 2018 +0200
@@ -297,7 +297,7 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text],
- consolidate: Boolean): Session.Change =
+ consolidate: List[Document.Node.Name]): Session.Change =
{
val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
--- a/src/Pure/Tools/dump.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/Tools/dump.scala Wed Jun 06 13:04:52 2018 +0200
@@ -14,22 +14,24 @@
sealed case class Aspect_Args(
options: Options,
progress: Progress,
+ deps: Sessions.Deps,
output_dir: Path,
- deps: Sessions.Deps,
- result: Thy_Resources.Theories_Result)
+ node_name: Document.Node.Name,
+ node_status: Protocol.Node_Status,
+ snapshot: Document.Snapshot)
{
- def write(node_name: Document.Node.Name, file_name: Path, bytes: Bytes)
+ def write(file_name: Path, bytes: Bytes)
{
val path = output_dir + Path.basic(node_name.theory) + file_name
Isabelle_System.mkdirs(path.dir)
Bytes.write(path, bytes)
}
- def write(node_name: Document.Node.Name, file_name: Path, text: String): Unit =
- write(node_name, file_name, Bytes(text))
+ def write(file_name: Path, text: String): Unit =
+ write(file_name, Bytes(text))
- def write(node_name: Document.Node.Name, file_name: Path, body: XML.Body): Unit =
- write(node_name, file_name, Symbol.encode(YXML.string_of_body(body)))
+ def write(file_name: Path, body: XML.Body): Unit =
+ write(file_name, Symbol.encode(YXML.string_of_body(body)))
}
sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
@@ -40,35 +42,27 @@
val known_aspects =
List(
+ Aspect("markup", "PIDE markup (YXML format)",
+ { case args =>
+ args.write(Path.explode("markup.yxml"),
+ args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
+ }),
Aspect("messages", "output messages (YXML format)",
{ case args =>
- for (node_name <- args.result.node_names) {
- args.write(node_name, Path.explode("messages.yxml"),
- args.result.messages(node_name).iterator.map(_._1).toList)
- }
- }),
- Aspect("markup", "PIDE markup (YXML format)",
- { case args =>
- for (node_name <- args.result.node_names) {
- args.write(node_name, Path.explode("markup.yxml"),
- args.result.markup_to_XML(node_name))
- }
+ args.write(Path.explode("messages.yxml"),
+ args.snapshot.messages.iterator.map(_._1).toList)
}),
Aspect("latex", "generated LaTeX source",
{ case args =>
- for {
- node_name <- args.result.node_names
- entry <- args.result.exports(node_name)
- if entry.name == "document.tex"
- } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
+ for (entry <- args.snapshot.exports if entry.name == "document.tex")
+ args.write(Path.explode(entry.name), entry.uncompressed())
}, options = List("editor_presentation")),
Aspect("theory", "foundational theory content",
{ case args =>
for {
- node_name <- args.result.node_names
- entry <- args.result.exports(node_name)
+ entry <- args.snapshot.exports
if entry.name.startsWith(Export_Theory.export_prefix)
- } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
+ } args.write(Path.explode(entry.name), entry.uncompressed())
}, options = List("editor_presentation", "export_theory"))
).sortBy(_.name)
@@ -129,8 +123,12 @@
/* dump aspects */
- val aspect_args = Aspect_Args(dump_options, progress, output_dir, deps, theories_result)
- aspects.foreach(_.operation(aspect_args))
+ for ((node_name, node_status) <- theories_result.nodes) {
+ val snapshot = theories_result.snapshot(node_name)
+ val aspect_args =
+ Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot)
+ aspects.foreach(_.operation(aspect_args))
+ }
session_result
}
--- a/src/Pure/Tools/server_commands.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala Wed Jun 06 13:04:52 2018 +0200
@@ -205,25 +205,27 @@
"errors" ->
(for {
(name, status) <- result.nodes if !status.ok
- (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
+ (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree)
} yield output_message(tree, pos)),
"nodes" ->
- (for ((name, status) <- result.nodes) yield
+ (for ((name, status) <- result.nodes) yield {
+ val snapshot = result.snapshot(name)
name.json +
("status" -> status.json) +
("messages" ->
(for {
- (tree, pos) <- result.messages(name) if Protocol.is_exported(tree)
+ (tree, pos) <- snapshot.messages if Protocol.is_exported(tree)
} yield output_message(tree, pos))) +
("exports" ->
(if (args.export_pattern == "") Nil else {
val matcher = Export.make_matcher(args.export_pattern)
- for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
+ for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
yield {
val (base64, body) = entry.uncompressed().maybe_base64
JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
}
- }))))
+ }))
+ }))
(result_json, result)
}
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Jun 06 13:04:52 2018 +0200
@@ -97,15 +97,12 @@
echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
echo
echo " Options are:"
- echo " -A specify ancestor for base session image (default: parent)"
- echo " -B use base session image, with theories from other sessions"
- echo " -F focus on selected logic session: ignore unrelated theories"
+ echo " -A NAME ancestor session for options -R and -S (default: parent)"
echo " -D NAME=X set JVM system property"
echo " -J OPTION add JVM runtime option"
echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
- echo " -P use parent session image"
- echo " -R open ROOT entry of logic session"
- echo " -S NAME edit specified logic session, abbreviates -B -F -R -l NAME"
+ echo " -R NAME build image with requirements from other sessions"
+ echo " -S NAME like option -R, with focus on selected session"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
@@ -143,11 +140,9 @@
BUILD_JARS="jars"
ML_PROCESS_POLICY=""
JEDIT_LOGIC_ANCESTOR=""
-JEDIT_LOGIC_BASE=""
+JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_LOGIC_FOCUS=""
JEDIT_SESSION_DIRS=""
-JEDIT_LOGIC_ROOT=""
-JEDIT_LOGIC_PARENT=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
JEDIT_BUILD_MODE="normal"
@@ -155,38 +150,26 @@
function getoptions()
{
OPTIND=1
- while getopts "A:BFD:J:PRS:bd:fj:l:m:np:s" OPT
+ while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT
do
case "$OPT" in
A)
JEDIT_LOGIC_ANCESTOR="$OPTARG"
;;
- B)
- JEDIT_LOGIC_BASE="true"
- JEDIT_LOGIC_PARENT=""
- ;;
D)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
;;
- F)
- JEDIT_LOGIC_FOCUS="true"
- ;;
J)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
;;
- P)
- JEDIT_LOGIC_PARENT="true"
- JEDIT_LOGIC_BASE=""
- ;;
R)
- JEDIT_LOGIC_ROOT="true"
+ JEDIT_LOGIC="$OPTARG"
+ JEDIT_LOGIC_REQUIREMENTS="true"
;;
S)
JEDIT_LOGIC="$OPTARG"
- JEDIT_LOGIC_BASE="true"
- JEDIT_LOGIC_PARENT=""
+ JEDIT_LOGIC_REQUIREMENTS="true"
JEDIT_LOGIC_FOCUS="true"
- JEDIT_LOGIC_ROOT="true"
;;
b)
BUILD_ONLY=true
@@ -429,8 +412,8 @@
if [ "$BUILD_ONLY" = false ]
then
- export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
- JEDIT_LOGIC_PARENT JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
+ JEDIT_LOGIC_FOCUS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
classpath "$JEDIT_HOME/dist/jedit.jar"
exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
--- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Jun 06 11:12:37 2018 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Wed Jun 06 13:04:52 2018 +0200
@@ -40,9 +40,8 @@
options.string(jedit_logic_option))
def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
+ def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
- def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
- def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
def logic_info(options: Options): Option[Sessions.Info] =
try {
@@ -52,9 +51,7 @@
catch { case ERROR(_) => None }
def logic_root(options: Options): Position.T =
- if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") {
- logic_info(options).map(_.pos) getOrElse Position.none
- }
+ if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none
else Position.none
@@ -111,13 +108,11 @@
def session_base_info(options: Options): Sessions.Base_Info =
Sessions.base_info(options,
dirs = JEdit_Sessions.session_dirs(),
- session =
- if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
- else logic_name(options),
- ancestor_session = logic_ancestor,
- all_known = !logic_focus,
- focus_session = logic_focus,
- required_session = logic_base)
+ session = logic_name(options),
+ session_ancestor = logic_ancestor,
+ session_requirements = logic_requirements,
+ session_focus = logic_focus,
+ all_known = !logic_focus)
def session_build(
options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =