--- a/Admin/isatest/isatest-makeall Mon Oct 26 18:52:29 2009 +0100
+++ b/Admin/isatest/isatest-makeall Tue Oct 27 12:16:26 2009 +0100
@@ -63,7 +63,7 @@
;;
sunbroy2)
- MFLAGS="-k -j 6"
+ MFLAGS="-k -j 2"
NICE="nice"
;;
--- a/Admin/isatest/isatest-makedist Mon Oct 26 18:52:29 2009 +0100
+++ b/Admin/isatest/isatest-makedist Tue Oct 27 12:16:26 2009 +0100
@@ -91,7 +91,7 @@
## spawn test runs
-#$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
+$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
# give test some time to copy settings and start
sleep 15
$SSH macbroy22 "$MAKEALL $HOME/settings/at-poly"
--- a/Admin/isatest/settings/sun-poly Mon Oct 26 18:52:29 2009 +0100
+++ b/Admin/isatest/settings/sun-poly Tue Oct 27 12:16:26 2009 +0100
@@ -23,6 +23,6 @@
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
#ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true -M 1"
+ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true -M 6 -q 2"
HOL_USEDIR_OPTIONS="-p 0"
--- a/doc/Contents Mon Oct 26 18:52:29 2009 +0100
+++ b/doc/Contents Tue Oct 27 12:16:26 2009 +0100
@@ -6,6 +6,7 @@
classes Tutorial on Type Classes
functions Tutorial on Function Definitions
codegen Tutorial on Code Generation
+ nitpick User's Guide to Nitpick in Isabelle/HOL
sugar LaTeX Sugar for Isabelle documents
Reference Manuals
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Oct 27 12:16:26 2009 +0100
@@ -2993,7 +2993,7 @@
| Const(@{const_name "power"},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
| Const(@{const_name "HOL.divide"},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
| _ => (FRPar.C (HOLogic.dest_number t |> snd,1)
- handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> valOf));
+ handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
fun tm_of_term m m' t =
case t of
@@ -3002,14 +3002,14 @@
| Const(@{const_name "HOL.minus"},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
| Const(@{const_name "HOL.times"},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
| _ => (FRPar.CP (num_of_term m' t)
- handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> valOf)
- | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> valOf));
+ handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
+ | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
fun term_of_num T m t =
case t of
FRPar.C (a,b) => (if b = 1 then num T a else if b=0 then (rz T)
else (divt T) $ num T a $ num T b)
-| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> valOf
+| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> the
| FRPar.Add(a,b) => (plust T)$(term_of_num T m a)$(term_of_num T m b)
| FRPar.Mul(a,b) => (timest T)$(term_of_num T m a)$(term_of_num T m b)
| FRPar.Sub(a,b) => (minust T)$(term_of_num T m a)$(term_of_num T m b)
@@ -3021,7 +3021,7 @@
fun term_of_tm T m m' t =
case t of
FRPar.CP p => term_of_num T m' p
-| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> valOf
+| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> the
| FRPar.tm_Add(a,b) => (plust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
| FRPar.tm_Mul(a,b) => (timest T)$(term_of_num T m' a)$(term_of_tm T m m' b)
| FRPar.tm_Sub(a,b) => (minust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
--- a/src/HOL/Induct/LList.thy Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Induct/LList.thy Tue Oct 27 12:16:26 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Induct/LList.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Shares NIL, CONS, List_case with List.thy
@@ -906,8 +905,8 @@
by (rule_tac l = l1 in llist_fun_equalityI, auto)
setup {*
-Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
- (map dest_Const [@{term LNil}, @{term LCons}])
+ Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+ (map dest_Const [@{term LNil}, @{term LCons}])
*}
end
--- a/src/HOL/IsaMakefile Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/IsaMakefile Tue Oct 27 12:16:26 2009 +0100
@@ -6,7 +6,20 @@
default: HOL
generate: HOL-Generate-HOL HOL-Generate-HOLLight
-images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-SMT HOL-Word TLA HOL4
+
+images: \
+ HOL \
+ HOL-Algebra \
+ HOL-Base \
+ HOL-Main \
+ HOL-Multivariate_Analysis \
+ HOL-NSA \
+ HOL-Nominal \
+ HOL-Plain \
+ HOL-SMT \
+ HOL-Word \
+ HOL4 \
+ TLA
#Note: keep targets sorted (except for HOL-Library and HOL-ex)
test: \
@@ -19,11 +32,11 @@
HOL-Hahn_Banach \
HOL-Hoare \
HOL-Hoare_Parallel \
- HOL-Import \
HOL-IMP \
HOL-IMPP \
HOL-IOA \
HOL-Imperative_HOL \
+ HOL-Import \
HOL-Induct \
HOL-Isar_Examples \
HOL-Lambda \
@@ -33,7 +46,6 @@
HOL-MicroJava \
HOL-Mirabelle \
HOL-Modelcheck \
- HOL-Multivariate_Analysis \
HOL-NanoJava \
HOL-Nitpick_Examples \
HOL-Nominal-Examples \
@@ -41,13 +53,13 @@
HOL-Old_Number_Theory \
HOL-Prolog \
HOL-SET_Protocol \
+ HOL-SMT-Examples \
HOL-SizeChange \
- HOL-SMT-Examples \
HOL-Statespace \
HOL-Subst \
- TLA-Buffer \
- TLA-Inc \
- TLA-Memory \
+ TLA-Buffer \
+ TLA-Inc \
+ TLA-Memory \
HOL-UNITY \
HOL-Unix \
HOL-W0 \
--- a/src/HOL/Library/Coinductive_List.thy Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Library/Coinductive_List.thy Tue Oct 27 12:16:26 2009 +0100
@@ -850,8 +850,8 @@
qed
setup {*
-Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
- (map dest_Const [@{term LNil}, @{term LCons}])
+ Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+ (map dest_Const [@{term LNil}, @{term LCons}])
*}
end
--- a/src/HOL/Rational.thy Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Rational.thy Tue Oct 27 12:16:26 2009 +0100
@@ -1064,22 +1064,22 @@
*}
setup {*
-Nitpick.register_frac_type @{type_name rat}
- [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
- (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
- (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
- (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
- (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
- (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
- (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
- (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
- (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
- (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
+ Nitpick.register_frac_type @{type_name rat}
+ [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
+ (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
+ (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
+ (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
+ (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
+ (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
+ (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
+ (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
+ (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
+ (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
*}
lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
- number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
- plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
- zero_rat_inst.zero_rat
+ number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
+ plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
+ zero_rat_inst.zero_rat
end
--- a/src/HOL/RealDef.thy Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/RealDef.thy Tue Oct 27 12:16:26 2009 +0100
@@ -1186,15 +1186,15 @@
*}
setup {*
-Nitpick.register_frac_type @{type_name real}
- [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
- (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
- (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
- (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
- (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
- (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
- (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
- (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
+ Nitpick.register_frac_type @{type_name real}
+ [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
+ (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
+ (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
+ (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
+ (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
+ (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
+ (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
+ (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
*}
lemmas [nitpick_def] = inverse_real_inst.inverse_real
--- a/src/HOL/Relation.thy Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Relation.thy Tue Oct 27 12:16:26 2009 +0100
@@ -607,6 +607,9 @@
lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
by (auto simp:inv_image_def)
+lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f"
+unfolding inv_image_def converse_def by auto
+
subsection {* Finiteness *}
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Oct 27 12:16:26 2009 +0100
@@ -271,7 +271,7 @@
Markup.markup Markup.sendback "apply metis")
| ERROR msg => (false, "Error: " ^ msg);
val _ = unregister result (Thread.self ());
- in () end handle Exn.Interrupt => ())
+ in () end)
in () end);
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Oct 27 12:16:26 2009 +0100
@@ -432,7 +432,7 @@
if auto orelse blocking then
go ()
else
- (SimpleThread.fork true (fn () => (go (); ()) handle Exn.Interrupt => ());
+ (SimpleThread.fork true (fn () => (go (); ()));
state)
end
--- a/src/HOL/Wellfounded.thy Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Wellfounded.thy Tue Oct 27 12:16:26 2009 +0100
@@ -14,19 +14,12 @@
subsection {* Basic Definitions *}
-constdefs
- wf :: "('a * 'a)set => bool"
+definition wf :: "('a * 'a) set => bool" where
"wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
- wfP :: "('a => 'a => bool) => bool"
+definition wfP :: "('a => 'a => bool) => bool" where
"wfP r == wf {(x, y). r x y}"
- acyclic :: "('a*'a)set => bool"
- "acyclic r == !x. (x,x) ~: r^+"
-
-abbreviation acyclicP :: "('a => 'a => bool) => bool" where
- "acyclicP r == acyclic {(x, y). r x y}"
-
lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
by (simp add: wfP_def)
@@ -59,14 +52,16 @@
lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
by (induct a arbitrary: x set: wf) blast
-(* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *)
-lemmas wf_asym = wf_not_sym [elim_format]
+lemma wf_asym:
+ assumes "wf r" "(a, x) \<in> r"
+ obtains "(x, a) \<notin> r"
+ by (drule wf_not_sym[OF assms])
lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
by (blast elim: wf_asym)
-(* [| wf r; (a,a) ~: r ==> PROP W |] ==> PROP W *)
-lemmas wf_irrefl = wf_not_refl [elim_format]
+lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r"
+by (drule wf_not_refl[OF assms])
lemma wf_wellorderI:
assumes wf: "wf {(x::'a::ord, y). x < y}"
@@ -82,7 +77,62 @@
subsection {* Basic Results *}
-text{*transitive closure of a well-founded relation is well-founded! *}
+text {* Point-free characterization of well-foundedness *}
+
+lemma wfE_pf:
+ assumes wf: "wf R"
+ assumes a: "A \<subseteq> R `` A"
+ shows "A = {}"
+proof -
+ { fix x
+ from wf have "x \<notin> A"
+ proof induct
+ fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A"
+ then have "x \<notin> R `` A" by blast
+ with a show "x \<notin> A" by blast
+ qed
+ } thus ?thesis by auto
+qed
+
+lemma wfI_pf:
+ assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}"
+ shows "wf R"
+proof (rule wfUNIVI)
+ fix P :: "'a \<Rightarrow> bool" and x
+ let ?A = "{x. \<not> P x}"
+ assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x"
+ then have "?A \<subseteq> R `` ?A" by blast
+ with a show "P x" by blast
+qed
+
+text{*Minimal-element characterization of well-foundedness*}
+
+lemma wfE_min:
+ assumes wf: "wf R" and Q: "x \<in> Q"
+ obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
+ using Q wfE_pf[OF wf, of Q] by blast
+
+lemma wfI_min:
+ assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q"
+ shows "wf R"
+proof (rule wfI_pf)
+ fix A assume b: "A \<subseteq> R `` A"
+ { fix x assume "x \<in> A"
+ from a[OF this] b have "False" by blast
+ }
+ thus "A = {}" by blast
+qed
+
+lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
+apply auto
+apply (erule wfE_min, assumption, blast)
+apply (rule wfI_min, auto)
+done
+
+lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
+
+text{* Well-foundedness of transitive closure *}
+
lemma wf_trancl:
assumes "wf r"
shows "wf (r^+)"
@@ -122,43 +172,8 @@
apply (erule wf_trancl)
done
+text {* Well-foundedness of subsets *}
-text{*Minimal-element characterization of well-foundedness*}
-lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
-proof (intro iffI strip)
- fix Q :: "'a set" and x
- assume "wf r" and "x \<in> Q"
- then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
- unfolding wf_def
- by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"])
-next
- assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
- show "wf r"
- proof (rule wfUNIVI)
- fix P :: "'a \<Rightarrow> bool" and x
- assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"
- let ?Q = "{x. \<not> P x}"
- have "x \<in> ?Q \<longrightarrow> (\<exists>z \<in> ?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"
- by (rule 1 [THEN spec, THEN spec])
- then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp
- with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast
- then show "P x" by simp
- qed
-qed
-
-lemma wfE_min:
- assumes "wf R" "x \<in> Q"
- obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
- using assms unfolding wf_eq_minimal by blast
-
-lemma wfI_min:
- "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)
- \<Longrightarrow> wf R"
- unfolding wf_eq_minimal by blast
-
-lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
-
-text {* Well-foundedness of subsets *}
lemma wf_subset: "[| wf(r); p<=r |] ==> wf(p)"
apply (simp (no_asm_use) add: wf_eq_minimal)
apply fast
@@ -167,7 +182,8 @@
lemmas wfP_subset = wf_subset [to_pred]
text {* Well-foundedness of the empty relation *}
-lemma wf_empty [iff]: "wf({})"
+
+lemma wf_empty [iff]: "wf {}"
by (simp add: wf_def)
lemma wfP_empty [iff]:
@@ -187,7 +203,20 @@
apply (rule Int_lower2)
done
-text{*Well-foundedness of insert*}
+text {* Exponentiation *}
+
+lemma wf_exp:
+ assumes "wf (R ^^ n)"
+ shows "wf R"
+proof (rule wfI_pf)
+ fix A assume "A \<subseteq> R `` A"
+ then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+
+ with `wf (R ^^ n)`
+ show "A = {}" by (rule wfE_pf)
+qed
+
+text {* Well-foundedness of insert *}
+
lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
apply (rule iffI)
apply (blast elim: wf_trancl [THEN wf_irrefl]
@@ -210,6 +239,7 @@
done
text{*Well-foundedness of image*}
+
lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
apply (simp only: wf_eq_minimal, clarify)
apply (case_tac "EX p. f p : Q")
@@ -351,7 +381,13 @@
by (rule wf_union_merge [where S = "{}", simplified])
-subsubsection {* acyclic *}
+subsection {* Acyclic relations *}
+
+definition acyclic :: "('a * 'a) set => bool" where
+ "acyclic r == !x. (x,x) ~: r^+"
+
+abbreviation acyclicP :: "('a => 'a => bool) => bool" where
+ "acyclicP r == acyclic {(x, y). r x y}"
lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
by (simp add: acyclic_def)
--- a/src/Pure/Concurrent/simple_thread.ML Mon Oct 26 18:52:29 2009 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML Tue Oct 27 12:16:26 2009 +0100
@@ -15,7 +15,7 @@
struct
fun fork interrupts body =
- Thread.fork (fn () => exception_trace (fn () => body ()),
+ Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Mon Oct 26 18:52:29 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Tue Oct 27 12:16:26 2009 +0100
@@ -33,14 +33,9 @@
val max_threads = Unsynchronized.ref 0;
-val tested_platform =
- let val ml_platform = getenv "ML_PLATFORM"
- in String.isSuffix "linux" ml_platform orelse String.isSuffix "darwin" ml_platform end;
-
fun max_threads_value () =
let val m = ! max_threads in
if m > 0 then m
- else if not tested_platform then 1
else Int.min (Int.max (Thread.numProcessors (), 1), 4)
end;
--- a/src/Pure/ML-Systems/polyml_common.ML Mon Oct 26 18:52:29 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Oct 27 12:16:26 2009 +0100
@@ -18,6 +18,9 @@
val forget_structure = PolyML.Compiler.forgetStructure;
+val _ = PolyML.Compiler.forgetValue "isSome";
+val _ = PolyML.Compiler.forgetValue "getOpt";
+val _ = PolyML.Compiler.forgetValue "valOf";
val _ = PolyML.Compiler.forgetValue "foldl";
val _ = PolyML.Compiler.forgetValue "foldr";
val _ = PolyML.Compiler.forgetValue "print";