1.1 --- a/lib/Tools/build Wed May 07 12:25:35 2014 +0200
1.2 +++ b/lib/Tools/build Wed May 07 14:51:51 2014 +0200
1.3 @@ -144,7 +144,7 @@
1.4 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
1.5 "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
1.6 "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
1.7 - "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
1.8 + "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
1.9 "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
1.10 RC="$?"
1.11
2.1 --- a/src/Doc/Implementation/Integration.thy Wed May 07 12:25:35 2014 +0200
2.2 +++ b/src/Doc/Implementation/Integration.thy Wed May 07 14:51:51 2014 +0200
2.3 @@ -133,7 +133,6 @@
2.4
2.5 text %mlref {*
2.6 \begin{mldecls}
2.7 - @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
2.8 @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
2.9 Toplevel.transition -> Toplevel.transition"} \\
2.10 @{index_ML Toplevel.theory: "(theory -> theory) ->
2.11 @@ -150,10 +149,6 @@
2.12
2.13 \begin{description}
2.14
2.15 - \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
2.16 - causes the toplevel loop to echo the result state (in interactive
2.17 - mode).
2.18 -
2.19 \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
2.20 function.
2.21
3.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML Wed May 07 12:25:35 2014 +0200
3.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Wed May 07 14:51:51 2014 +0200
3.3 @@ -336,13 +336,11 @@
3.4 val _ =
3.5 Outer_Syntax.command @{command_spec "pcpodef"}
3.6 "HOLCF type definition (requires admissibility proof)"
3.7 - (typedef_proof_decl >>
3.8 - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)))
3.9 + (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
3.10
3.11 val _ =
3.12 Outer_Syntax.command @{command_spec "cpodef"}
3.13 "HOLCF type definition (requires admissibility proof)"
3.14 - (typedef_proof_decl >>
3.15 - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)))
3.16 + (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
3.17
3.18 end
4.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML Wed May 07 12:25:35 2014 +0200
4.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Wed May 07 14:51:51 2014 +0200
4.3 @@ -212,7 +212,6 @@
4.4
4.5 val _ =
4.6 Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
4.7 - (domaindef_decl >>
4.8 - (Toplevel.print oo (Toplevel.theory o mk_domaindef)))
4.9 + (domaindef_decl >> (Toplevel.theory o mk_domaindef))
4.10
4.11 end
5.1 --- a/src/HOL/Library/Set_Algebras.thy Wed May 07 12:25:35 2014 +0200
5.2 +++ b/src/HOL/Library/Set_Algebras.thy Wed May 07 14:51:51 2014 +0200
5.3 @@ -9,7 +9,7 @@
5.4 begin
5.5
5.6 text {*
5.7 - This library lifts operations like addition and muliplication to
5.8 + This library lifts operations like addition and multiplication to
5.9 sets. It was designed to support asymptotic calculations. See the
5.10 comments at the top of theory @{text BigO}.
5.11 *}
5.12 @@ -38,17 +38,17 @@
5.13 begin
5.14
5.15 definition
5.16 - set_zero[simp]: "0::('a::zero)set == {0}"
5.17 + set_zero[simp]: "(0::'a::zero set) = {0}"
5.18
5.19 instance ..
5.20
5.21 end
5.22 -
5.23 +
5.24 instantiation set :: (one) one
5.25 begin
5.26
5.27 definition
5.28 - set_one[simp]: "1::('a::one)set == {1}"
5.29 + set_one[simp]: "(1::'a::one set) = {1}"
5.30
5.31 instance ..
5.32
5.33 @@ -64,30 +64,30 @@
5.34 "x =o A \<equiv> x \<in> A"
5.35
5.36 instance set :: (semigroup_add) semigroup_add
5.37 -by default (force simp add: set_plus_def add.assoc)
5.38 + by default (force simp add: set_plus_def add.assoc)
5.39
5.40 instance set :: (ab_semigroup_add) ab_semigroup_add
5.41 -by default (force simp add: set_plus_def add.commute)
5.42 + by default (force simp add: set_plus_def add.commute)
5.43
5.44 instance set :: (monoid_add) monoid_add
5.45 -by default (simp_all add: set_plus_def)
5.46 + by default (simp_all add: set_plus_def)
5.47
5.48 instance set :: (comm_monoid_add) comm_monoid_add
5.49 -by default (simp_all add: set_plus_def)
5.50 + by default (simp_all add: set_plus_def)
5.51
5.52 instance set :: (semigroup_mult) semigroup_mult
5.53 -by default (force simp add: set_times_def mult.assoc)
5.54 + by default (force simp add: set_times_def mult.assoc)
5.55
5.56 instance set :: (ab_semigroup_mult) ab_semigroup_mult
5.57 -by default (force simp add: set_times_def mult.commute)
5.58 + by default (force simp add: set_times_def mult.commute)
5.59
5.60 instance set :: (monoid_mult) monoid_mult
5.61 -by default (simp_all add: set_times_def)
5.62 + by default (simp_all add: set_times_def)
5.63
5.64 instance set :: (comm_monoid_mult) comm_monoid_mult
5.65 -by default (simp_all add: set_times_def)
5.66 + by default (simp_all add: set_times_def)
5.67
5.68 -lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
5.69 +lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
5.70 by (auto simp add: set_plus_def)
5.71
5.72 lemma set_plus_elim:
5.73 @@ -95,11 +95,11 @@
5.74 obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
5.75 using assms unfolding set_plus_def by fast
5.76
5.77 -lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
5.78 +lemma set_plus_intro2 [intro]: "b \<in> C \<Longrightarrow> a + b \<in> a +o C"
5.79 by (auto simp add: elt_set_plus_def)
5.80
5.81 -lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
5.82 - (b +o D) = (a + b) +o (C + D)"
5.83 +lemma set_plus_rearrange:
5.84 + "((a::'a::comm_monoid_add) +o C) + (b +o D) = (a + b) +o (C + D)"
5.85 apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
5.86 apply (rule_tac x = "ba + bb" in exI)
5.87 apply (auto simp add: add_ac)
5.88 @@ -107,12 +107,10 @@
5.89 apply (auto simp add: add_ac)
5.90 done
5.91
5.92 -lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
5.93 - (a + b) +o C"
5.94 +lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C"
5.95 by (auto simp add: elt_set_plus_def add_assoc)
5.96
5.97 -lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
5.98 - a +o (B + C)"
5.99 +lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = a +o (B + C)"
5.100 apply (auto simp add: elt_set_plus_def set_plus_def)
5.101 apply (blast intro: add_ac)
5.102 apply (rule_tac x = "a + aa" in exI)
5.103 @@ -123,8 +121,7 @@
5.104 apply (auto simp add: add_ac)
5.105 done
5.106
5.107 -theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
5.108 - a +o (C + D)"
5.109 +theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = a +o (C + D)"
5.110 apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
5.111 apply (rule_tac x = "aa + ba" in exI)
5.112 apply (auto simp add: add_ac)
5.113 @@ -133,48 +130,43 @@
5.114 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
5.115 set_plus_rearrange3 set_plus_rearrange4
5.116
5.117 -lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
5.118 +lemma set_plus_mono [intro!]: "C \<subseteq> D \<Longrightarrow> a +o C \<subseteq> a +o D"
5.119 by (auto simp add: elt_set_plus_def)
5.120
5.121 -lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
5.122 - C + E <= D + F"
5.123 +lemma set_plus_mono2 [intro]: "(C::'a::plus set) \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C + E \<subseteq> D + F"
5.124 by (auto simp add: set_plus_def)
5.125
5.126 -lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
5.127 +lemma set_plus_mono3 [intro]: "a \<in> C \<Longrightarrow> a +o D \<subseteq> C + D"
5.128 by (auto simp add: elt_set_plus_def set_plus_def)
5.129
5.130 -lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
5.131 - a +o D <= D + C"
5.132 +lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) \<in> C \<Longrightarrow> a +o D \<subseteq> D + C"
5.133 by (auto simp add: elt_set_plus_def set_plus_def add_ac)
5.134
5.135 -lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
5.136 - apply (subgoal_tac "a +o B <= a +o D")
5.137 +lemma set_plus_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a +o B \<subseteq> C + D"
5.138 + apply (subgoal_tac "a +o B \<subseteq> a +o D")
5.139 apply (erule order_trans)
5.140 apply (erule set_plus_mono3)
5.141 apply (erule set_plus_mono)
5.142 done
5.143
5.144 -lemma set_plus_mono_b: "C <= D ==> x : a +o C
5.145 - ==> x : a +o D"
5.146 +lemma set_plus_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a +o C \<Longrightarrow> x \<in> a +o D"
5.147 apply (frule set_plus_mono)
5.148 apply auto
5.149 done
5.150
5.151 -lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
5.152 - x : D + F"
5.153 +lemma set_plus_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C + E \<Longrightarrow> x \<in> D + F"
5.154 apply (frule set_plus_mono2)
5.155 prefer 2
5.156 apply force
5.157 apply assumption
5.158 done
5.159
5.160 -lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
5.161 +lemma set_plus_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> C + D"
5.162 apply (frule set_plus_mono3)
5.163 apply auto
5.164 done
5.165
5.166 -lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
5.167 - x : a +o D ==> x : D + C"
5.168 +lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> D + C"
5.169 apply (frule set_plus_mono4)
5.170 apply auto
5.171 done
5.172 @@ -182,28 +174,27 @@
5.173 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
5.174 by (auto simp add: elt_set_plus_def)
5.175
5.176 -lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
5.177 +lemma set_zero_plus2: "(0::'a::comm_monoid_add) \<in> A \<Longrightarrow> B \<subseteq> A + B"
5.178 apply (auto simp add: set_plus_def)
5.179 apply (rule_tac x = 0 in bexI)
5.180 apply (rule_tac x = x in bexI)
5.181 apply (auto simp add: add_ac)
5.182 done
5.183
5.184 -lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
5.185 +lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C \<Longrightarrow> (a - b) \<in> C"
5.186 by (auto simp add: elt_set_plus_def add_ac)
5.187
5.188 -lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
5.189 +lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C \<Longrightarrow> a \<in> b +o C"
5.190 apply (auto simp add: elt_set_plus_def add_ac)
5.191 apply (subgoal_tac "a = (a + - b) + b")
5.192 apply (rule bexI, assumption)
5.193 apply (auto simp add: add_ac)
5.194 done
5.195
5.196 -lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
5.197 - by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
5.198 - assumption)
5.199 +lemma set_minus_plus: "(a::'a::ab_group_add) - b \<in> C \<longleftrightarrow> a \<in> b +o C"
5.200 + by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus)
5.201
5.202 -lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
5.203 +lemma set_times_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a * b \<in> C * D"
5.204 by (auto simp add: set_times_def)
5.205
5.206 lemma set_times_elim:
5.207 @@ -211,11 +202,11 @@
5.208 obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
5.209 using assms unfolding set_times_def by fast
5.210
5.211 -lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
5.212 +lemma set_times_intro2 [intro!]: "b \<in> C \<Longrightarrow> a * b \<in> a *o C"
5.213 by (auto simp add: elt_set_times_def)
5.214
5.215 -lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
5.216 - (b *o D) = (a * b) *o (C * D)"
5.217 +lemma set_times_rearrange:
5.218 + "((a::'a::comm_monoid_mult) *o C) * (b *o D) = (a * b) *o (C * D)"
5.219 apply (auto simp add: elt_set_times_def set_times_def)
5.220 apply (rule_tac x = "ba * bb" in exI)
5.221 apply (auto simp add: mult_ac)
5.222 @@ -223,12 +214,12 @@
5.223 apply (auto simp add: mult_ac)
5.224 done
5.225
5.226 -lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
5.227 - (a * b) *o C"
5.228 +lemma set_times_rearrange2:
5.229 + "(a::'a::semigroup_mult) *o (b *o C) = (a * b) *o C"
5.230 by (auto simp add: elt_set_times_def mult_assoc)
5.231
5.232 -lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
5.233 - a *o (B * C)"
5.234 +lemma set_times_rearrange3:
5.235 + "((a::'a::semigroup_mult) *o B) * C = a *o (B * C)"
5.236 apply (auto simp add: elt_set_times_def set_times_def)
5.237 apply (blast intro: mult_ac)
5.238 apply (rule_tac x = "a * aa" in exI)
5.239 @@ -239,10 +230,9 @@
5.240 apply (auto simp add: mult_ac)
5.241 done
5.242
5.243 -theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
5.244 - a *o (C * D)"
5.245 - apply (auto simp add: elt_set_times_def set_times_def
5.246 - mult_ac)
5.247 +theorem set_times_rearrange4:
5.248 + "C * ((a::'a::comm_monoid_mult) *o D) = a *o (C * D)"
5.249 + apply (auto simp add: elt_set_times_def set_times_def mult_ac)
5.250 apply (rule_tac x = "aa * ba" in exI)
5.251 apply (auto simp add: mult_ac)
5.252 done
5.253 @@ -250,48 +240,43 @@
5.254 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
5.255 set_times_rearrange3 set_times_rearrange4
5.256
5.257 -lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
5.258 +lemma set_times_mono [intro]: "C \<subseteq> D \<Longrightarrow> a *o C \<subseteq> a *o D"
5.259 by (auto simp add: elt_set_times_def)
5.260
5.261 -lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
5.262 - C * E <= D * F"
5.263 +lemma set_times_mono2 [intro]: "(C::'a::times set) \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C * E \<subseteq> D * F"
5.264 by (auto simp add: set_times_def)
5.265
5.266 -lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
5.267 +lemma set_times_mono3 [intro]: "a \<in> C \<Longrightarrow> a *o D \<subseteq> C * D"
5.268 by (auto simp add: elt_set_times_def set_times_def)
5.269
5.270 -lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
5.271 - a *o D <= D * C"
5.272 +lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C \<Longrightarrow> a *o D \<subseteq> D * C"
5.273 by (auto simp add: elt_set_times_def set_times_def mult_ac)
5.274
5.275 -lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
5.276 - apply (subgoal_tac "a *o B <= a *o D")
5.277 +lemma set_times_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a *o B \<subseteq> C * D"
5.278 + apply (subgoal_tac "a *o B \<subseteq> a *o D")
5.279 apply (erule order_trans)
5.280 apply (erule set_times_mono3)
5.281 apply (erule set_times_mono)
5.282 done
5.283
5.284 -lemma set_times_mono_b: "C <= D ==> x : a *o C
5.285 - ==> x : a *o D"
5.286 +lemma set_times_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a *o C \<Longrightarrow> x \<in> a *o D"
5.287 apply (frule set_times_mono)
5.288 apply auto
5.289 done
5.290
5.291 -lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
5.292 - x : D * F"
5.293 +lemma set_times_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C * E \<Longrightarrow> x \<in> D * F"
5.294 apply (frule set_times_mono2)
5.295 prefer 2
5.296 apply force
5.297 apply assumption
5.298 done
5.299
5.300 -lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
5.301 +lemma set_times_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> C * D"
5.302 apply (frule set_times_mono3)
5.303 apply auto
5.304 done
5.305
5.306 -lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
5.307 - x : a *o D ==> x : D * C"
5.308 +lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> D * C"
5.309 apply (frule set_times_mono4)
5.310 apply auto
5.311 done
5.312 @@ -299,20 +284,19 @@
5.313 lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
5.314 by (auto simp add: elt_set_times_def)
5.315
5.316 -lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
5.317 - (a * b) +o (a *o C)"
5.318 +lemma set_times_plus_distrib:
5.319 + "(a::'a::semiring) *o (b +o C) = (a * b) +o (a *o C)"
5.320 by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
5.321
5.322 -lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
5.323 - (a *o B) + (a *o C)"
5.324 +lemma set_times_plus_distrib2:
5.325 + "(a::'a::semiring) *o (B + C) = (a *o B) + (a *o C)"
5.326 apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
5.327 apply blast
5.328 apply (rule_tac x = "b + bb" in exI)
5.329 apply (auto simp add: ring_distribs)
5.330 done
5.331
5.332 -lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
5.333 - a *o D + C * D"
5.334 +lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D \<subseteq> a *o D + C * D"
5.335 apply (auto simp add:
5.336 elt_set_plus_def elt_set_times_def set_times_def
5.337 set_plus_def ring_distribs)
5.338 @@ -323,12 +307,10 @@
5.339 set_times_plus_distrib
5.340 set_times_plus_distrib2
5.341
5.342 -lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
5.343 - - a : C"
5.344 +lemma set_neg_intro: "(a::'a::ring_1) \<in> (- 1) *o C \<Longrightarrow> - a \<in> C"
5.345 by (auto simp add: elt_set_times_def)
5.346
5.347 -lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
5.348 - - a : (- 1) *o C"
5.349 +lemma set_neg_intro2: "(a::'a::ring_1) \<in> C \<Longrightarrow> - a \<in> (- 1) *o C"
5.350 by (auto simp add: elt_set_times_def)
5.351
5.352 lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
5.353 @@ -337,53 +319,63 @@
5.354 lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
5.355 unfolding set_times_def by (fastforce simp: image_iff)
5.356
5.357 -lemma finite_set_plus:
5.358 - assumes "finite s" and "finite t" shows "finite (s + t)"
5.359 - using assms unfolding set_plus_image by simp
5.360 +lemma finite_set_plus: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s + t)"
5.361 + unfolding set_plus_image by simp
5.362
5.363 -lemma finite_set_times:
5.364 - assumes "finite s" and "finite t" shows "finite (s * t)"
5.365 - using assms unfolding set_times_image by simp
5.366 +lemma finite_set_times: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s * t)"
5.367 + unfolding set_times_image by simp
5.368
5.369 lemma set_setsum_alt:
5.370 assumes fin: "finite I"
5.371 shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
5.372 (is "_ = ?setsum I")
5.373 -using fin proof induct
5.374 + using fin
5.375 +proof induct
5.376 + case empty
5.377 + then show ?case by simp
5.378 +next
5.379 case (insert x F)
5.380 have "setsum S (insert x F) = S x + ?setsum F"
5.381 using insert.hyps by auto
5.382 - also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
5.383 + also have "\<dots> = {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
5.384 unfolding set_plus_def
5.385 proof safe
5.386 - fix y s assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
5.387 + fix y s
5.388 + assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
5.389 then show "\<exists>s'. y + setsum s F = s' x + setsum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
5.390 using insert.hyps
5.391 by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def)
5.392 qed auto
5.393 finally show ?case
5.394 using insert.hyps by auto
5.395 -qed auto
5.396 +qed
5.397
5.398 lemma setsum_set_cond_linear:
5.399 - fixes f :: "('a::comm_monoid_add) set \<Rightarrow> ('b::comm_monoid_add) set"
5.400 + fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
5.401 assumes [intro!]: "\<And>A B. P A \<Longrightarrow> P B \<Longrightarrow> P (A + B)" "P {0}"
5.402 and f: "\<And>A B. P A \<Longrightarrow> P B \<Longrightarrow> f (A + B) = f A + f B" "f {0} = {0}"
5.403 assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
5.404 shows "f (setsum S I) = setsum (f \<circ> S) I"
5.405 -proof cases
5.406 - assume "finite I" from this all show ?thesis
5.407 +proof (cases "finite I")
5.408 + case True
5.409 + from this all show ?thesis
5.410 proof induct
5.411 + case empty
5.412 + then show ?case by (auto intro!: f)
5.413 + next
5.414 case (insert x F)
5.415 from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum S F)"
5.416 by induct auto
5.417 with insert show ?case
5.418 by (simp, subst f) auto
5.419 - qed (auto intro!: f)
5.420 -qed (auto intro!: f)
5.421 + qed
5.422 +next
5.423 + case False
5.424 + then show ?thesis by (auto intro!: f)
5.425 +qed
5.426
5.427 lemma setsum_set_linear:
5.428 - fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set"
5.429 + fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
5.430 assumes "\<And>A B. f(A) + f(B) = f(A + B)" "f {0} = {0}"
5.431 shows "f (setsum S I) = setsum (f \<circ> S) I"
5.432 using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
5.433 @@ -391,11 +383,11 @@
5.434 lemma set_times_Un_distrib:
5.435 "A * (B \<union> C) = A * B \<union> A * C"
5.436 "(A \<union> B) * C = A * C \<union> B * C"
5.437 -by (auto simp: set_times_def)
5.438 + by (auto simp: set_times_def)
5.439
5.440 lemma set_times_UNION_distrib:
5.441 - "A * UNION I M = UNION I (%i. A * M i)"
5.442 - "UNION I M * A = UNION I (%i. M i * A)"
5.443 -by (auto simp: set_times_def)
5.444 + "A * UNION I M = (\<Union>i\<in>I. A * M i)"
5.445 + "UNION I M * A = (\<Union>i\<in>I. M i * A)"
5.446 + by (auto simp: set_times_def)
5.447
5.448 end
6.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML Wed May 07 12:25:35 2014 +0200
6.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Wed May 07 14:51:51 2014 +0200
6.3 @@ -123,8 +123,7 @@
6.4 val _ =
6.5 Outer_Syntax.command @{command_spec "spark_vc"}
6.6 "enter into proof mode for a specific verification condition"
6.7 - (Parse.name >> (fn name =>
6.8 - (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
6.9 + (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
6.10
6.11 val _ =
6.12 Outer_Syntax.improper_command @{command_spec "spark_status"}
7.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed May 07 12:25:35 2014 +0200
7.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed May 07 14:51:51 2014 +0200
7.3 @@ -666,7 +666,6 @@
7.4 val _ =
7.5 Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
7.6 (Scan.repeat1 Parse.term >> (fn ts =>
7.7 - Toplevel.print o
7.8 Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts)));
7.9
7.10 end;
8.1 --- a/src/HOL/Tools/choice_specification.ML Wed May 07 12:25:35 2014 +0200
8.2 +++ b/src/HOL/Tools/choice_specification.ML Wed May 07 14:51:51 2014 +0200
8.3 @@ -201,7 +201,6 @@
8.4 Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
8.5 (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
8.6 Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
8.7 - >> (fn (cos, alt_props) => Toplevel.print o
8.8 - (Toplevel.theory_to_proof (process_spec cos alt_props))))
8.9 + >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
8.10
8.11 end
9.1 --- a/src/Pure/Isar/calculation.ML Wed May 07 12:25:35 2014 +0200
9.2 +++ b/src/Pure/Isar/calculation.ML Wed May 07 14:51:51 2014 +0200
9.3 @@ -118,9 +118,9 @@
9.4 val ctxt' = Proof.context_of state';
9.5 val _ =
9.6 if int then
9.7 - Pretty.writeln
9.8 - (Proof_Context.pretty_fact ctxt'
9.9 - (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
9.10 + Proof_Context.pretty_fact ctxt'
9.11 + (Proof_Context.full_name ctxt' (Binding.name calculationN), calc)
9.12 + |> Pretty.string_of |> Output.urgent_message
9.13 else ();
9.14 in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
9.15
10.1 --- a/src/Pure/Isar/isar_syn.ML Wed May 07 12:25:35 2014 +0200
10.2 +++ b/src/Pure/Isar/isar_syn.ML Wed May 07 14:51:51 2014 +0200
10.3 @@ -404,14 +404,12 @@
10.4 val _ =
10.5 Outer_Syntax.command @{command_spec "include"}
10.6 "include declarations from bundle in proof body"
10.7 - (Scan.repeat1 (Parse.position Parse.xname)
10.8 - >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
10.9 + (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
10.10
10.11 val _ =
10.12 Outer_Syntax.command @{command_spec "including"}
10.13 "include declarations from bundle in goal refinement"
10.14 - (Scan.repeat1 (Parse.position Parse.xname)
10.15 - >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
10.16 + (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
10.17
10.18 val _ =
10.19 Outer_Syntax.improper_command @{command_spec "print_bundles"}
10.20 @@ -425,7 +423,7 @@
10.21 val _ =
10.22 Outer_Syntax.command @{command_spec "context"} "begin local theory context"
10.23 ((Parse.position Parse.xname >> (fn name =>
10.24 - Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
10.25 + Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
10.26 Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
10.27 >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
10.28 --| Parse.begin);
10.29 @@ -443,7 +441,7 @@
10.30 (Parse.binding --
10.31 Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
10.32 >> (fn ((name, (expr, elems)), begin) =>
10.33 - (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
10.34 + Toplevel.begin_local_theory begin
10.35 (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
10.36
10.37 fun interpretation_args mandatory =
10.38 @@ -456,24 +454,20 @@
10.39 "prove sublocale relation between a locale and a locale expression"
10.40 ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
10.41 interpretation_args false >> (fn (loc, (expr, equations)) =>
10.42 - Toplevel.print o
10.43 Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
10.44 || interpretation_args false >> (fn (expr, equations) =>
10.45 - Toplevel.print o
10.46 Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
10.47
10.48 val _ =
10.49 Outer_Syntax.command @{command_spec "interpretation"}
10.50 "prove interpretation of locale expression in local theory"
10.51 (interpretation_args true >> (fn (expr, equations) =>
10.52 - Toplevel.print o
10.53 Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
10.54
10.55 val _ =
10.56 Outer_Syntax.command @{command_spec "interpret"}
10.57 "prove interpretation of locale expression in proof context"
10.58 (interpretation_args true >> (fn (expr, equations) =>
10.59 - Toplevel.print o
10.60 Toplevel.proof' (Expression.interpret_cmd expr equations)));
10.61
10.62
10.63 @@ -488,7 +482,7 @@
10.64 Outer_Syntax.command @{command_spec "class"} "define type class"
10.65 (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
10.66 >> (fn ((name, (supclasses, elems)), begin) =>
10.67 - (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
10.68 + Toplevel.begin_local_theory begin
10.69 (Class_Declaration.class_cmd I name supclasses elems #> snd)));
10.70
10.71 val _ =
10.72 @@ -498,17 +492,14 @@
10.73 val _ =
10.74 Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
10.75 (Parse.multi_arity --| Parse.begin
10.76 - >> (fn arities => Toplevel.print o
10.77 - Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
10.78 + >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
10.79
10.80 val _ =
10.81 Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
10.82 ((Parse.class --
10.83 ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
10.84 - Parse.multi_arity >> Class.instance_arity_cmd)
10.85 - >> (Toplevel.print oo Toplevel.theory_to_proof) ||
10.86 - Scan.succeed
10.87 - (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
10.88 + Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
10.89 + Scan.succeed (Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
10.90
10.91
10.92 (* arbitrary overloading *)
10.93 @@ -518,8 +509,7 @@
10.94 (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
10.95 Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
10.96 >> Parse.triple1) --| Parse.begin
10.97 - >> (fn operations => Toplevel.print o
10.98 - Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
10.99 + >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
10.100
10.101
10.102 (* code generation *)
10.103 @@ -559,20 +549,20 @@
10.104
10.105 val _ =
10.106 Outer_Syntax.command @{command_spec "have"} "state local goal"
10.107 - (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
10.108 + (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
10.109
10.110 val _ =
10.111 Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
10.112 - (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
10.113 + (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
10.114
10.115 val _ =
10.116 Outer_Syntax.command @{command_spec "show"}
10.117 "state local goal, solving current obligation"
10.118 - (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
10.119 + (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
10.120
10.121 val _ =
10.122 Outer_Syntax.command @{command_spec "thus"} "old-style alias of \"then show\""
10.123 - (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
10.124 + (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
10.125
10.126
10.127 (* facts *)
10.128 @@ -581,42 +571,42 @@
10.129
10.130 val _ =
10.131 Outer_Syntax.command @{command_spec "then"} "forward chaining"
10.132 - (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
10.133 + (Scan.succeed (Toplevel.proof Proof.chain));
10.134
10.135 val _ =
10.136 Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
10.137 - (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
10.138 + (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
10.139
10.140 val _ =
10.141 Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
10.142 - (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
10.143 + (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
10.144
10.145 val _ =
10.146 Outer_Syntax.command @{command_spec "note"} "define facts"
10.147 - (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
10.148 + (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
10.149
10.150 val _ =
10.151 Outer_Syntax.command @{command_spec "using"} "augment goal facts"
10.152 - (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
10.153 + (facts >> (Toplevel.proof o Proof.using_cmd));
10.154
10.155 val _ =
10.156 Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
10.157 - (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
10.158 + (facts >> (Toplevel.proof o Proof.unfolding_cmd));
10.159
10.160
10.161 (* proof context *)
10.162
10.163 val _ =
10.164 Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
10.165 - (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
10.166 + (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
10.167
10.168 val _ =
10.169 Outer_Syntax.command @{command_spec "assume"} "assume propositions"
10.170 - (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
10.171 + (Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
10.172
10.173 val _ =
10.174 Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
10.175 - (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
10.176 + (Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
10.177
10.178 val _ =
10.179 Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
10.180 @@ -624,26 +614,26 @@
10.181 (Parse_Spec.opt_thm_name ":" --
10.182 ((Parse.binding -- Parse.opt_mixfix) --
10.183 ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
10.184 - >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
10.185 + >> (Toplevel.proof o Proof.def_cmd));
10.186
10.187 val _ =
10.188 Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
10.189 (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
10.190 - >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
10.191 + >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
10.192
10.193 val _ =
10.194 Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
10.195 - (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
10.196 + (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
10.197
10.198 val _ =
10.199 Outer_Syntax.command @{command_spec "let"} "bind text variables"
10.200 (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
10.201 - >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
10.202 + >> (Toplevel.proof o Proof.let_bind_cmd));
10.203
10.204 val _ =
10.205 Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
10.206 (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
10.207 - >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
10.208 + >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
10.209
10.210 val _ =
10.211 Outer_Syntax.command @{command_spec "case"} "invoke local context"
10.212 @@ -651,22 +641,22 @@
10.213 Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
10.214 --| @{keyword ")"}) ||
10.215 Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
10.216 - Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
10.217 + Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
10.218
10.219
10.220 (* proof structure *)
10.221
10.222 val _ =
10.223 Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
10.224 - (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
10.225 + (Scan.succeed (Toplevel.proof Proof.begin_block));
10.226
10.227 val _ =
10.228 Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
10.229 - (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
10.230 + (Scan.succeed (Toplevel.proof Proof.end_block));
10.231
10.232 val _ =
10.233 Outer_Syntax.command @{command_spec "next"} "enter next proof block"
10.234 - (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
10.235 + (Scan.succeed (Toplevel.proof Proof.next_block));
10.236
10.237
10.238 (* end proof *)
10.239 @@ -675,61 +665,58 @@
10.240 Outer_Syntax.command @{command_spec "qed"} "conclude proof"
10.241 (Scan.option Method.parse >> (fn m =>
10.242 (Option.map Method.report m;
10.243 - Toplevel.print o Isar_Cmd.qed m)));
10.244 + Isar_Cmd.qed m)));
10.245
10.246 val _ =
10.247 Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
10.248 (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
10.249 (Method.report m1;
10.250 Option.map Method.report m2;
10.251 - Toplevel.print o Isar_Cmd.terminal_proof (m1, m2))));
10.252 + Isar_Cmd.terminal_proof (m1, m2))));
10.253
10.254 val _ =
10.255 Outer_Syntax.command @{command_spec ".."} "default proof"
10.256 - (Scan.succeed (Toplevel.print o Isar_Cmd.default_proof));
10.257 + (Scan.succeed Isar_Cmd.default_proof);
10.258
10.259 val _ =
10.260 Outer_Syntax.command @{command_spec "."} "immediate proof"
10.261 - (Scan.succeed (Toplevel.print o Isar_Cmd.immediate_proof));
10.262 + (Scan.succeed Isar_Cmd.immediate_proof);
10.263
10.264 val _ =
10.265 Outer_Syntax.command @{command_spec "done"} "done proof"
10.266 - (Scan.succeed (Toplevel.print o Isar_Cmd.done_proof));
10.267 + (Scan.succeed Isar_Cmd.done_proof);
10.268
10.269 val _ =
10.270 Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
10.271 - (Scan.succeed (Toplevel.print o Isar_Cmd.skip_proof));
10.272 + (Scan.succeed Isar_Cmd.skip_proof);
10.273
10.274 val _ =
10.275 Outer_Syntax.command @{command_spec "oops"} "forget proof"
10.276 - (Scan.succeed (Toplevel.print o Toplevel.forget_proof));
10.277 + (Scan.succeed Toplevel.forget_proof);
10.278
10.279
10.280 (* proof steps *)
10.281
10.282 val _ =
10.283 Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
10.284 - (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
10.285 + (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
10.286
10.287 val _ =
10.288 Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
10.289 - (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
10.290 + (Parse.nat >> (Toplevel.proof o Proof.prefer));
10.291
10.292 val _ =
10.293 Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
10.294 - (Method.parse >> (fn m =>
10.295 - (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_results m))));
10.296 + (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
10.297
10.298 val _ =
10.299 Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
10.300 - (Method.parse >> (fn m =>
10.301 - (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_end_results m))));
10.302 + (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
10.303
10.304 val _ =
10.305 Outer_Syntax.command @{command_spec "proof"} "backward proof step"
10.306 (Scan.option Method.parse >> (fn m =>
10.307 (Option.map Method.report m;
10.308 - Toplevel.print o
10.309 Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
10.310 Toplevel.skip_proof (fn i => i + 1))));
10.311
10.312 @@ -741,8 +728,8 @@
10.313
10.314 val _ =
10.315 Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
10.316 - (Scan.succeed (Toplevel.print o
10.317 - Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
10.318 + (Scan.succeed
10.319 + (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
10.320 Toplevel.skip_proof (fn h => (report_back (); h))));
10.321
10.322
10.323 @@ -792,8 +779,9 @@
10.324 Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
10.325
10.326 val _ =
10.327 - Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
10.328 - (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_state_context)));
10.329 + Outer_Syntax.improper_command @{command_spec "print_context"}
10.330 + "print context of local theory target"
10.331 + (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
10.332
10.333 val _ =
10.334 Outer_Syntax.improper_command @{command_spec "print_theory"}
11.1 --- a/src/Pure/Isar/keyword.ML Wed May 07 12:25:35 2014 +0200
11.2 +++ b/src/Pure/Isar/keyword.ML Wed May 07 14:51:51 2014 +0200
11.3 @@ -67,6 +67,7 @@
11.4 val is_proof_goal: string -> bool
11.5 val is_qed: string -> bool
11.6 val is_qed_global: string -> bool
11.7 + val is_printed: string -> bool
11.8 end;
11.9
11.10 structure Keyword: KEYWORD =
11.11 @@ -263,5 +264,7 @@
11.12 val is_qed = command_category [qed, qed_script, qed_block];
11.13 val is_qed_global = command_category [qed_global];
11.14
11.15 +val is_printed = is_theory_goal orf is_proof;
11.16 +
11.17 end;
11.18
12.1 --- a/src/Pure/Isar/obtain.ML Wed May 07 12:25:35 2014 +0200
12.2 +++ b/src/Pure/Isar/obtain.ML Wed May 07 14:51:51 2014 +0200
12.3 @@ -300,7 +300,7 @@
12.4
12.5 val goal = Var (("guess", 0), propT);
12.6 fun print_result ctxt' (k, [(s, [_, th])]) =
12.7 - Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
12.8 + Proof_Display.print_results int ctxt' (k, [(s, [th])]);
12.9 val before_qed =
12.10 Method.primitive_text (fn ctxt =>
12.11 Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
13.1 --- a/src/Pure/Isar/outer_syntax.ML Wed May 07 12:25:35 2014 +0200
13.2 +++ b/src/Pure/Isar/outer_syntax.ML Wed May 07 14:51:51 2014 +0200
13.3 @@ -203,14 +203,13 @@
13.4
13.5 (* local_theory commands *)
13.6
13.7 -fun local_theory_command do_print trans command_spec comment parse =
13.8 - command command_spec comment (Parse.opt_target -- parse
13.9 - >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
13.10 +fun local_theory_command trans command_spec comment parse =
13.11 + command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
13.12
13.13 -val local_theory' = local_theory_command false Toplevel.local_theory';
13.14 -val local_theory = local_theory_command false Toplevel.local_theory;
13.15 -val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
13.16 -val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
13.17 +val local_theory' = local_theory_command Toplevel.local_theory';
13.18 +val local_theory = local_theory_command Toplevel.local_theory;
13.19 +val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
13.20 +val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
13.21
13.22
13.23 (* inspect syntax *)
14.1 --- a/src/Pure/Isar/proof.ML Wed May 07 12:25:35 2014 +0200
14.2 +++ b/src/Pure/Isar/proof.ML Wed May 07 14:51:51 2014 +0200
14.3 @@ -365,8 +365,7 @@
14.4 else if mode = Backward then Proof_Context.pretty_ctxt ctxt
14.5 else [];
14.6 in
14.7 - [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
14.8 - (if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
14.9 + [Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1)),
14.10 Pretty.str ""] @
14.11 (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
14.12 (if verbose orelse mode = Forward then
14.13 @@ -1042,7 +1041,7 @@
14.14 local
14.15
14.16 fun gen_have prep_att prepp before_qed after_qed stmt int =
14.17 - local_goal (Proof_Display.print_results Markup.state int)
14.18 + local_goal (Proof_Display.print_results int)
14.19 prep_att prepp "have" before_qed after_qed stmt;
14.20
14.21 fun gen_show prep_att prepp before_qed after_qed stmt int state =
14.22 @@ -1056,7 +1055,7 @@
14.23
14.24 fun print_results ctxt res =
14.25 if ! testing then ()
14.26 - else Proof_Display.print_results Markup.state int ctxt res;
14.27 + else Proof_Display.print_results int ctxt res;
14.28 fun print_rule ctxt th =
14.29 if ! testing then rule := SOME th
14.30 else if int then
15.1 --- a/src/Pure/Isar/proof_display.ML Wed May 07 12:25:35 2014 +0200
15.2 +++ b/src/Pure/Isar/proof_display.ML Wed May 07 14:51:51 2014 +0200
15.3 @@ -22,8 +22,7 @@
15.4 val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
15.5 val method_error: string -> Position.T ->
15.6 {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
15.7 - val print_results: Markup.T -> bool -> Proof.context ->
15.8 - ((string * string) * (string * thm list) list) -> unit
15.9 + val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
15.10 val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
15.11 end
15.12
15.13 @@ -141,13 +140,13 @@
15.14
15.15 in
15.16
15.17 -fun print_results markup do_print ctxt ((kind, name), facts) =
15.18 +fun print_results do_print ctxt ((kind, name), facts) =
15.19 if not do_print orelse kind = "" then ()
15.20 else if name = "" then
15.21 - (Pretty.writeln o Pretty.mark markup)
15.22 + (Pretty.writeln o Pretty.mark Markup.state)
15.23 (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
15.24 else
15.25 - (Pretty.writeln o Pretty.mark markup)
15.26 + (Pretty.writeln o Pretty.mark Markup.state)
15.27 (case facts of
15.28 [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
15.29 Proof_Context.pretty_fact ctxt fact])
15.30 @@ -176,7 +175,7 @@
15.31
15.32 fun print_consts do_print ctxt pred cs =
15.33 if not do_print orelse null cs then ()
15.34 - else Pretty.writeln (pretty_consts ctxt pred cs);
15.35 + else Pretty.writeln (Pretty.mark Markup.state (pretty_consts ctxt pred cs));
15.36
15.37 end;
15.38
16.1 --- a/src/Pure/Isar/specification.ML Wed May 07 12:25:35 2014 +0200
16.2 +++ b/src/Pure/Isar/specification.ML Wed May 07 14:51:51 2014 +0200
16.3 @@ -301,7 +301,7 @@
16.4 |> Attrib.partial_evaluation ctxt'
16.5 |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
16.6 val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
16.7 - val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res);
16.8 + val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
16.9 in (res, lthy') end;
16.10
16.11 in
16.12 @@ -400,12 +400,12 @@
16.13 (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
16.14 val lthy'' =
16.15 if Attrib.is_empty_binding (name, atts) then
16.16 - (Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res); lthy')
16.17 + (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
16.18 else
16.19 let
16.20 val ([(res_name, _)], lthy'') =
16.21 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
16.22 - val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, res_name), res);
16.23 + val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
16.24 in lthy'' end;
16.25 in after_qed results' lthy'' end;
16.26 in
17.1 --- a/src/Pure/Isar/toplevel.ML Wed May 07 12:25:35 2014 +0200
17.2 +++ b/src/Pure/Isar/toplevel.ML Wed May 07 14:51:51 2014 +0200
17.3 @@ -22,7 +22,7 @@
17.4 val proof_of: state -> Proof.state
17.5 val proof_position_of: state -> int
17.6 val end_theory: Position.T -> state -> theory
17.7 - val pretty_state_context: state -> Pretty.T list
17.8 + val pretty_context: state -> Pretty.T list
17.9 val pretty_state: state -> Pretty.T list
17.10 val print_state: state -> unit
17.11 val pretty_abstract: state -> Pretty.T
17.12 @@ -32,14 +32,11 @@
17.13 val profiling: int Unsynchronized.ref
17.14 type transition
17.15 val empty: transition
17.16 - val print_of: transition -> bool
17.17 val name_of: transition -> string
17.18 val pos_of: transition -> Position.T
17.19 val name: string -> transition -> transition
17.20 val position: Position.T -> transition -> transition
17.21 val interactive: bool -> transition -> transition
17.22 - val set_print: bool -> transition -> transition
17.23 - val print: transition -> transition
17.24 val init_theory: (unit -> theory) -> transition -> transition
17.25 val is_init: transition -> bool
17.26 val modify_init: (unit -> theory) -> transition -> transition
17.27 @@ -198,14 +195,18 @@
17.28
17.29 (* print state *)
17.30
17.31 -val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
17.32 -
17.33 -fun pretty_state_context state =
17.34 +fun pretty_context state =
17.35 (case try node_of state of
17.36 NONE => []
17.37 - | SOME (Theory (gthy, _)) => pretty_context gthy
17.38 - | SOME (Proof (_, (_, gthy))) => pretty_context gthy
17.39 - | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy);
17.40 + | SOME node =>
17.41 + let
17.42 + val gthy =
17.43 + (case node of
17.44 + Theory (gthy, _) => gthy
17.45 + | Proof (_, (_, gthy)) => gthy
17.46 + | Skipped_Proof (_, (gthy, _)) => gthy);
17.47 + val lthy = Context.cases (Named_Target.theory_init) I gthy;
17.48 + in Local_Theory.pretty lthy end);
17.49
17.50 fun pretty_state state =
17.51 (case try node_of state of
17.52 @@ -312,23 +313,21 @@
17.53 {name: string, (*command name*)
17.54 pos: Position.T, (*source position*)
17.55 int_only: bool, (*interactive-only*) (* TTY / Proof General legacy*)
17.56 - print: bool, (*print result state*)
17.57 timing: Time.time option, (*prescient timing information*)
17.58 trans: trans list}; (*primitive transitions (union)*)
17.59
17.60 -fun make_transition (name, pos, int_only, print, timing, trans) =
17.61 - Transition {name = name, pos = pos, int_only = int_only, print = print,
17.62 +fun make_transition (name, pos, int_only, timing, trans) =
17.63 + Transition {name = name, pos = pos, int_only = int_only,
17.64 timing = timing, trans = trans};
17.65
17.66 -fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) =
17.67 - make_transition (f (name, pos, int_only, print, timing, trans));
17.68 +fun map_transition f (Transition {name, pos, int_only, timing, trans}) =
17.69 + make_transition (f (name, pos, int_only, timing, trans));
17.70
17.71 -val empty = make_transition ("", Position.none, false, false, NONE, []);
17.72 +val empty = make_transition ("", Position.none, false, NONE, []);
17.73
17.74
17.75 (* diagnostics *)
17.76
17.77 -fun print_of (Transition {print, ...}) = print;
17.78 fun name_of (Transition {name, ...}) = name;
17.79 fun pos_of (Transition {pos, ...}) = pos;
17.80
17.81 @@ -341,25 +340,20 @@
17.82
17.83 (* modify transitions *)
17.84
17.85 -fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) =>
17.86 - (name, pos, int_only, print, timing, trans));
17.87 +fun name name = map_transition (fn (_, pos, int_only, timing, trans) =>
17.88 + (name, pos, int_only, timing, trans));
17.89
17.90 -fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) =>
17.91 - (name, pos, int_only, print, timing, trans));
17.92 +fun position pos = map_transition (fn (name, _, int_only, timing, trans) =>
17.93 + (name, pos, int_only, timing, trans));
17.94
17.95 -fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) =>
17.96 - (name, pos, int_only, print, timing, trans));
17.97 +fun interactive int_only = map_transition (fn (name, pos, _, timing, trans) =>
17.98 + (name, pos, int_only, timing, trans));
17.99
17.100 -fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) =>
17.101 - (name, pos, int_only, print, timing, tr :: trans));
17.102 +fun add_trans tr = map_transition (fn (name, pos, int_only, timing, trans) =>
17.103 + (name, pos, int_only, timing, tr :: trans));
17.104
17.105 -val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) =>
17.106 - (name, pos, int_only, print, timing, []));
17.107 -
17.108 -fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) =>
17.109 - (name, pos, int_only, print, timing, trans));
17.110 -
17.111 -val print = set_print true;
17.112 +val reset_trans = map_transition (fn (name, pos, int_only, timing, _) =>
17.113 + (name, pos, int_only, timing, []));
17.114
17.115
17.116 (* basic transitions *)
17.117 @@ -415,6 +409,10 @@
17.118 let
17.119 val lthy = f thy;
17.120 val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
17.121 + val _ =
17.122 + if begin then
17.123 + Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
17.124 + else ();
17.125 in Theory (gthy, SOME lthy) end
17.126 | _ => raise UNDEF));
17.127
17.128 @@ -579,19 +577,22 @@
17.129 (* apply transitions *)
17.130
17.131 fun get_timing (Transition {timing, ...}) = timing;
17.132 -fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
17.133 - (name, pos, int_only, print, timing, trans));
17.134 +fun put_timing timing = map_transition (fn (name, pos, int_only, _, trans) =>
17.135 + (name, pos, int_only, timing, trans));
17.136
17.137 local
17.138
17.139 -fun app int (tr as Transition {trans, print, ...}) =
17.140 +fun app int (tr as Transition {name, trans, ...}) =
17.141 setmp_thread_position tr (fn state =>
17.142 let
17.143 val timing_start = Timing.start ();
17.144
17.145 val (result, opt_err) =
17.146 state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
17.147 - val _ = if int andalso not (! quiet) andalso print then print_state result else ();
17.148 +
17.149 + val _ =
17.150 + if int andalso not (! quiet) andalso Keyword.is_printed name
17.151 + then print_state result else ();
17.152
17.153 val timing_result = Timing.result timing_start;
17.154 val timing_props =
17.155 @@ -739,7 +740,7 @@
17.156 (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
17.157
17.158 val st'' = st'
17.159 - |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
17.160 + |> command (head_tr |> reset_trans |> forked_proof);
17.161 val end_result = Result (end_tr, st'');
17.162 val result =
17.163 Result_List [head_result, Result.get (presentation_context_of st''), end_result];
18.1 --- a/src/Pure/PIDE/command.ML Wed May 07 12:25:35 2014 +0200
18.2 +++ b/src/Pure/PIDE/command.ML Wed May 07 14:51:51 2014 +0200
18.3 @@ -226,12 +226,10 @@
18.4 else
18.5 let
18.6 val malformed' = Toplevel.is_malformed tr;
18.7 - val is_init = Toplevel.is_init tr;
18.8 - val is_proof = Keyword.is_proof (Toplevel.name_of tr);
18.9
18.10 val _ = Multithreading.interrupted ();
18.11 val _ = status tr Markup.running;
18.12 - val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
18.13 + val (errs1, result) = run true tr st;
18.14 val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
18.15 val errs = errs1 @ errs2;
18.16 val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
18.17 @@ -376,15 +374,10 @@
18.18 val _ =
18.19 print_function "print_state"
18.20 (fn {command_name, ...} =>
18.21 - SOME {delay = NONE, pri = 1, persistent = false, strict = true,
18.22 - print_fn = fn tr => fn st' =>
18.23 - let
18.24 - val is_init = Keyword.is_theory_begin command_name;
18.25 - val is_proof = Keyword.is_proof command_name;
18.26 - val do_print =
18.27 - not is_init andalso
18.28 - (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
18.29 - in if do_print then Toplevel.print_state st' else () end});
18.30 + if Keyword.is_printed command_name then
18.31 + SOME {delay = NONE, pri = 1, persistent = false, strict = true,
18.32 + print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
18.33 + else NONE);
18.34
18.35
18.36 (* combined execution *)
19.1 --- a/src/Pure/System/isabelle_process.ML Wed May 07 12:25:35 2014 +0200
19.2 +++ b/src/Pure/System/isabelle_process.ML Wed May 07 14:51:51 2014 +0200
19.3 @@ -200,7 +200,7 @@
19.4 val channel = rendezvous ();
19.5 val msg_channel = init_channels channel;
19.6 val _ = Session.init_protocol_handlers ();
19.7 - val _ = loop channel;
19.8 + val _ = (loop |> Unsynchronized.setmp Toplevel.quiet true) channel;
19.9 in Message_Channel.shutdown msg_channel end);
19.10
19.11 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
20.1 --- a/src/Pure/Tools/build.scala Wed May 07 12:25:35 2014 +0200
20.2 +++ b/src/Pure/Tools/build.scala Wed May 07 14:51:51 2014 +0200
20.3 @@ -288,7 +288,8 @@
20.4 if (is_session_dir(dir)) dir
20.5 else error("Bad session root directory: " + dir.toString)
20.6
20.7 - def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
20.8 + def find_sessions(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil)
20.9 + : Session_Tree =
20.10 {
20.11 def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
20.12 find_root(select, dir) ::: find_roots(select, dir)
20.13 @@ -320,13 +321,13 @@
20.14 else Nil
20.15 }
20.16
20.17 - val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
20.18 -
20.19 - more_dirs foreach { case (_, dir) => check_session_dir(dir) }
20.20 + val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
20.21 + dirs.foreach(check_session_dir(_))
20.22 + select_dirs.foreach(check_session_dir(_))
20.23
20.24 Session_Tree(
20.25 for {
20.26 - (select, dir) <- default_dirs ::: more_dirs
20.27 + (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
20.28 info <- find_dir(select, dir)
20.29 } yield info)
20.30 }
20.31 @@ -511,8 +512,7 @@
20.32 dirs: List[Path],
20.33 sessions: List[String]): Deps =
20.34 {
20.35 - val (_, tree) =
20.36 - find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, sessions)
20.37 + val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
20.38 dependencies(Ignore_Progress, inlined_files, false, false, tree)
20.39 }
20.40
20.41 @@ -722,7 +722,8 @@
20.42 all_sessions: Boolean = false,
20.43 build_heap: Boolean = false,
20.44 clean_build: Boolean = false,
20.45 - more_dirs: List[(Boolean, Path)] = Nil,
20.46 + dirs: List[Path] = Nil,
20.47 + select_dirs: List[Path] = Nil,
20.48 session_groups: List[String] = Nil,
20.49 max_jobs: Int = 1,
20.50 list_files: Boolean = false,
20.51 @@ -733,7 +734,7 @@
20.52 {
20.53 /* session tree and dependencies */
20.54
20.55 - val full_tree = find_sessions(options, more_dirs)
20.56 + val full_tree = find_sessions(options, dirs, select_dirs)
20.57 val (selected, selected_tree) =
20.58 full_tree.selection(requirements, all_sessions, session_groups, sessions)
20.59
20.60 @@ -972,7 +973,8 @@
20.61 all_sessions: Boolean = false,
20.62 build_heap: Boolean = false,
20.63 clean_build: Boolean = false,
20.64 - more_dirs: List[(Boolean, Path)] = Nil,
20.65 + dirs: List[Path] = Nil,
20.66 + select_dirs: List[Path] = Nil,
20.67 session_groups: List[String] = Nil,
20.68 max_jobs: Int = 1,
20.69 list_files: Boolean = false,
20.70 @@ -983,8 +985,8 @@
20.71 {
20.72 val results =
20.73 build_results(options, progress, requirements, all_sessions,
20.74 - build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
20.75 - system_mode, verbose, sessions)
20.76 + build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
20.77 + list_files, no_build, system_mode, verbose, sessions)
20.78
20.79 val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
20.80 if (rc != 0 && (verbose || !no_build)) {
20.81 @@ -1012,16 +1014,13 @@
20.82 Properties.Value.Boolean(no_build) ::
20.83 Properties.Value.Boolean(system_mode) ::
20.84 Properties.Value.Boolean(verbose) ::
20.85 - Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
20.86 + Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
20.87 val options = (Options.init() /: build_options)(_ + _)
20.88 - val more_dirs =
20.89 - select_dirs.map(d => (true, Path.explode(d))) :::
20.90 - include_dirs.map(d => (false, Path.explode(d)))
20.91 val progress = new Console_Progress(verbose)
20.92 progress.interrupt_handler {
20.93 - build(options, progress, requirements, all_sessions,
20.94 - build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
20.95 - system_mode, verbose, sessions)
20.96 + build(options, progress, requirements, all_sessions, build_heap, clean_build,
20.97 + dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
20.98 + max_jobs, list_files, no_build, system_mode, verbose, sessions)
20.99 }
20.100 case _ => error("Bad arguments:\n" + cat_lines(args))
20.101 }
21.1 --- a/src/Pure/Tools/build_doc.scala Wed May 07 12:25:35 2014 +0200
21.2 +++ b/src/Pure/Tools/build_doc.scala Wed May 07 14:51:51 2014 +0200
21.3 @@ -24,7 +24,7 @@
21.4 {
21.5 val selection =
21.6 for {
21.7 - (name, info) <- Build.find_sessions(options, Nil).topological_order
21.8 + (name, info) <- Build.find_sessions(options).topological_order
21.9 if info.groups.contains("doc")
21.10 doc = info.options.string("document_variants")
21.11 if all_docs || docs.contains(doc)
22.1 --- a/src/Pure/Tools/find_consts.ML Wed May 07 12:25:35 2014 +0200
22.2 +++ b/src/Pure/Tools/find_consts.ML Wed May 07 14:51:51 2014 +0200
22.3 @@ -113,7 +113,9 @@
22.4 |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
22.5 |> map (apsnd fst o snd);
22.6 in
22.7 - Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
22.8 + Pretty.block
22.9 + (Pretty.keyword1 "find_consts" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
22.10 + Pretty.fbreaks (map pretty_criterion raw_criteria)) ::
22.11 Pretty.str "" ::
22.12 Pretty.str
22.13 (if null matches
23.1 --- a/src/Pure/Tools/find_theorems.ML Wed May 07 12:25:35 2014 +0200
23.2 +++ b/src/Pure/Tools/find_theorems.ML Wed May 07 14:51:51 2014 +0200
23.3 @@ -483,7 +483,9 @@
23.4 then " (" ^ string_of_int returned ^ " displayed)"
23.5 else ""));
23.6 in
23.7 - Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
23.8 + Pretty.block
23.9 + (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
23.10 + Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) ::
23.11 Pretty.str "" ::
23.12 (if null theorems then [Pretty.str "nothing found"]
23.13 else
24.1 --- a/src/Pure/Tools/keywords.scala Wed May 07 12:25:35 2014 +0200
24.2 +++ b/src/Pure/Tools/keywords.scala Wed May 07 14:51:51 2014 +0200
24.3 @@ -150,7 +150,7 @@
24.4
24.5 def update_keywords(options: Options)
24.6 {
24.7 - val tree = Build.find_sessions(options, Nil)
24.8 + val tree = Build.find_sessions(options)
24.9
24.10 def chapter(ch: String): List[String] =
24.11 for ((name, info) <- tree.topological_order if info.chapter == ch) yield name
25.1 --- a/src/Pure/Tools/main.scala Wed May 07 12:25:35 2014 +0200
25.2 +++ b/src/Pure/Tools/main.scala Wed May 07 14:51:51 2014 +0200
25.3 @@ -41,13 +41,13 @@
25.4 else {
25.5 val options = Options.init()
25.6 val system_mode = mode == "" || mode == "system"
25.7 - val more_dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).map((false, _))
25.8 + val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
25.9 val session = Isabelle_System.default_logic(
25.10 Isabelle_System.getenv("JEDIT_LOGIC"),
25.11 options.string("jedit_logic"))
25.12
25.13 if (Build.build(options = options, build_heap = true, no_build = true,
25.14 - more_dirs = more_dirs, sessions = List(session)) == 0)
25.15 + dirs = dirs, sessions = List(session)) == 0)
25.16 system_dialog.return_code(0)
25.17 else {
25.18 system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")")
25.19 @@ -56,9 +56,8 @@
25.20 val (out, rc) =
25.21 try {
25.22 ("",
25.23 - Build.build(options = options, progress = system_dialog,
25.24 - build_heap = true, more_dirs = more_dirs,
25.25 - system_mode = system_mode, sessions = List(session)))
25.26 + Build.build(options = options, progress = system_dialog, build_heap = true,
25.27 + dirs = dirs, system_mode = system_mode, sessions = List(session)))
25.28 }
25.29 catch {
25.30 case exn: Throwable =>
26.1 --- a/src/Pure/Tools/print_operation.ML Wed May 07 12:25:35 2014 +0200
26.2 +++ b/src/Pure/Tools/print_operation.ML Wed May 07 14:51:51 2014 +0200
26.3 @@ -61,8 +61,8 @@
26.4 (* common print operations *)
26.5
26.6 val _ =
26.7 - register "context" "main context"
26.8 - (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state_context);
26.9 + register "context" "context of local theory target"
26.10 + (Pretty.string_of o Pretty.chunks o Toplevel.pretty_context);
26.11
26.12 val _ =
26.13 register "cases" "cases of proof context"
27.1 --- a/src/Pure/pure_syn.ML Wed May 07 12:25:35 2014 +0200
27.2 +++ b/src/Pure/pure_syn.ML Wed May 07 14:51:51 2014 +0200
27.3 @@ -11,9 +11,8 @@
27.4 Outer_Syntax.command
27.5 (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
27.6 (Thy_Header.args >> (fn header =>
27.7 - Toplevel.print o
27.8 - Toplevel.init_theory
27.9 - (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
27.10 + Toplevel.init_theory
27.11 + (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
27.12
27.13 val _ =
27.14 Outer_Syntax.command
28.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala Wed May 07 12:25:35 2014 +0200
28.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed May 07 14:51:51 2014 +0200
28.3 @@ -71,8 +71,7 @@
28.4
28.5 def session_list(): List[String] =
28.6 {
28.7 - val dirs = session_dirs().map((false, _))
28.8 - val session_tree = Build.find_sessions(PIDE.options.value, dirs)
28.9 + val session_tree = Build.find_sessions(PIDE.options.value, dirs = session_dirs())
28.10 val (main_sessions, other_sessions) =
28.11 session_tree.topological_order.partition(p => p._2.groups.contains("main"))
28.12 main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
29.1 --- a/src/Tools/jEdit/src/jEdit.props Wed May 07 12:25:35 2014 +0200
29.2 +++ b/src/Tools/jEdit/src/jEdit.props Wed May 07 14:51:51 2014 +0200
29.3 @@ -243,6 +243,7 @@
29.4 recent-buffer.shortcut2=C+CIRCUMFLEX
29.5 restore.remote=false
29.6 restore=false
29.7 +search.subdirs.toggle=true
29.8 select-block.shortcut2=C+8
29.9 sidekick-tree.dock-position=right
29.10 sidekick.auto-complete-popup-get-focus=true