--- a/NEWS Fri Oct 29 11:04:41 2010 +0200
+++ b/NEWS Fri Oct 29 11:07:21 2010 +0200
@@ -344,6 +344,10 @@
Fail if the argument is false. Due to inlining the source position of
failed assertions is included in the error output.
+* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
+text is in practice always evaluated with a stable theory checkpoint.
+Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
+
* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
meaning.
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Fri Oct 29 11:04:41 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Fri Oct 29 11:07:21 2010 +0200
@@ -226,11 +226,10 @@
text %mlantiq {*
\begin{matharray}{rcl}
@{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\
- @{ML_antiquotation_def "theory_ref"} & : & @{text ML_antiquotation} \\
\end{matharray}
\begin{rail}
- ('theory' | 'theory\_ref') nameref?
+ 'theory' nameref?
;
\end{rail}
@@ -243,10 +242,6 @@
theory @{text "A"} of the background theory of the current context
--- as abstract value.
- \item @{text "@{theory_ref}"} is similar to @{text "@{theory}"}, but
- produces a @{ML_type theory_ref} via @{ML "Theory.check_thy"} as
- explained above.
-
\end{description}
*}
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Oct 29 11:04:41 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Oct 29 11:07:21 2010 +0200
@@ -262,11 +262,10 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
- \indexdef{}{ML antiquotation}{theory\_ref}\hypertarget{ML antiquotation.theory-ref}{\hyperlink{ML antiquotation.theory-ref}{\mbox{\isa{theory{\isacharunderscore}ref}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\end{matharray}
\begin{rail}
- ('theory' | 'theory\_ref') nameref?
+ 'theory' nameref?
;
\end{rail}
@@ -279,10 +278,6 @@
theory \isa{A} of the background theory of the current context
--- as abstract value.
- \item \isa{{\isacharat}{\isacharbraceleft}theory{\isacharunderscore}ref{\isacharbraceright}} is similar to \isa{{\isacharat}{\isacharbraceleft}theory{\isacharbraceright}}, but
- produces a \verb|theory_ref| via \verb|Theory.check_thy| as
- explained above.
-
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarRef/Thy/Spec.thy Fri Oct 29 11:04:41 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Fri Oct 29 11:07:21 2010 +0200
@@ -159,7 +159,7 @@
text {*
\begin{matharray}{rcll}
- @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\
+ @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
@{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{attribute_def "defn"} & : & @{text attribute} \\
@{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@@ -1139,8 +1139,8 @@
asserted, and records within the internal derivation object how
presumed theorems depend on unproven suppositions.
- \begin{matharray}{rcl}
- @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
+ \begin{matharray}{rcll}
+ @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
\end{matharray}
\begin{rail}
@@ -1159,7 +1159,7 @@
\end{description}
- See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
+ See @{"file" "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
defining a new primitive rule as oracle, and turning it into a proof
method.
*}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 11:04:41 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 11:07:21 2010 +0200
@@ -179,7 +179,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcll}
- \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!)\\
+ \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
\indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isa{attribute} \\
\indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
@@ -1179,8 +1179,8 @@
asserted, and records within the internal derivation object how
presumed theorems depend on unproven suppositions.
- \begin{matharray}{rcl}
- \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \begin{matharray}{rcll}
+ \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
\end{matharray}
\begin{rail}
@@ -1199,7 +1199,7 @@
\end{description}
- See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
+ See \hyperlink{file.~~/src/HOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
defining a new primitive rule as oracle, and turning it into a proof
method.%
\end{isamarkuptext}%
--- a/src/FOL/IsaMakefile Fri Oct 29 11:04:41 2010 +0200
+++ b/src/FOL/IsaMakefile Fri Oct 29 11:07:21 2010 +0200
@@ -45,14 +45,13 @@
FOL-ex: FOL $(LOG)/FOL-ex.gz
$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \
- ex/Iff_Oracle.thy ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \
+ ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \
ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \
ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy \
- ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML \
- ex/Classical.thy ex/document/root.tex ex/Foundation.thy \
- ex/Intuitionistic.thy ex/Intro.thy ex/Propositional_Int.thy \
- ex/Propositional_Cla.thy ex/Quantifiers_Int.thy \
- ex/Quantifiers_Cla.thy
+ ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy \
+ ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy \
+ ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy \
+ ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
--- a/src/FOL/ex/Iff_Oracle.thy Fri Oct 29 11:04:41 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(* Title: FOL/ex/Iff_Oracle.thy
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-*)
-
-header {* Example of Declaring an Oracle *}
-
-theory Iff_Oracle
-imports FOL
-begin
-
-subsection {* Oracle declaration *}
-
-text {*
- This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}.
- The length is specified by an integer, which is checked to be even
- and positive.
-*}
-
-oracle iff_oracle = {*
- let
- fun mk_iff 1 = Var (("P", 0), @{typ o})
- | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
- in
- fn (thy, n) =>
- if n > 0 andalso n mod 2 = 0
- then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
- else raise Fail ("iff_oracle: " ^ string_of_int n)
- end
-*}
-
-
-subsection {* Oracle as low-level rule *}
-
-ML {* iff_oracle (@{theory}, 2) *}
-ML {* iff_oracle (@{theory}, 10) *}
-ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *}
-
-text {* These oracle calls had better fail. *}
-
-ML {*
- (iff_oracle (@{theory}, 5); error "?")
- handle Fail _ => warning "Oracle failed, as expected"
-*}
-
-ML {*
- (iff_oracle (@{theory}, 1); error "?")
- handle Fail _ => warning "Oracle failed, as expected"
-*}
-
-
-subsection {* Oracle as proof method *}
-
-method_setup iff = {*
- Scan.lift Parse.nat >> (fn n => fn ctxt =>
- SIMPLE_METHOD
- (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
- handle Fail _ => no_tac))
-*} "iff oracle"
-
-
-lemma "A <-> A"
- by (iff 2)
-
-lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
- by (iff 10)
-
-lemma "A <-> A <-> A <-> A <-> A"
- apply (iff 5)?
- oops
-
-lemma A
- apply (iff 1)?
- oops
-
-end
--- a/src/FOL/ex/ROOT.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/FOL/ex/ROOT.ML Fri Oct 29 11:07:21 2010 +0200
@@ -18,8 +18,7 @@
"Propositional_Cla",
"Quantifiers_Cla",
"Miniscope",
- "If",
- "Iff_Oracle"
+ "If"
];
(*regression test for locales -- sets several global flags!*)
--- a/src/HOL/IsaMakefile Fri Oct 29 11:04:41 2010 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 29 11:07:21 2010 +0200
@@ -1016,20 +1016,19 @@
ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
- ex/Induction_Schema.thy ex/InductiveInvariant.thy \
+ ex/Iff_Oracle.thy ex/Induction_Schema.thy ex/InductiveInvariant.thy \
ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \
ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
- ex/Normalization_by_Evaluation.thy \
- ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
- ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
- ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
- ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
- ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
- ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
- ex/Unification.thy ex/While_Combinator_Example.thy \
- ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
- ex/svc_test.thy
+ ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy \
+ ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \
+ ex/Quickcheck_Lattice_Examples.thy ex/ROOT.ML ex/Recdefs.thy \
+ ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
+ ex/SAT_Examples.thy ex/SVC_Oracle.thy ex/Serbian.thy ex/Sqrt.thy \
+ ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
+ ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \
+ ex/While_Combinator_Example.thy ex/document/root.bib \
+ ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Oct 29 11:07:21 2010 +0200
@@ -703,7 +703,7 @@
val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
- else raise exn;
+ else reraise exn;
val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Oct 29 11:07:21 2010 +0200
@@ -6,10 +6,11 @@
signature QUOTIENT_INFO =
sig
- exception NotFound
+ exception NotFound (* FIXME complicates signatures unnecessarily *)
type maps_info = {mapfun: string, relmap: string}
val maps_defined: theory -> string -> bool
+ (* FIXME functions called "lookup" must return option, not raise exception *)
val maps_lookup: theory -> string -> maps_info (* raises NotFound *)
val maps_update_thy: string -> maps_info -> theory -> theory
val maps_update: string -> maps_info -> Proof.context -> Proof.context
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Oct 29 11:07:21 2010 +0200
@@ -67,8 +67,8 @@
fun get_mapfun ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
- val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exn
+ val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
+ raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
in
Const (mapfun, dummyT)
end
@@ -104,8 +104,8 @@
fun get_rty_qty ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
- val qdata = quotdata_lookup thy s handle NotFound => raise exn
+ val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
+ raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
in
(#rtyp qdata, #qtyp qdata)
end
@@ -127,7 +127,7 @@
val thy = ProofContext.theory_of ctxt
in
Sign.typ_match thy (ty_pat, ty) Vartab.empty
- handle MATCH_TYPE => err ctxt ty_pat ty
+ handle Type.TYPE_MATCH => err ctxt ty_pat ty
end
(* produces the rep or abs constant for a qty *)
@@ -276,8 +276,8 @@
fun get_relmap ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
- val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exn
+ val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
+ raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
in
Const (relmap, dummyT)
end
@@ -299,9 +299,9 @@
fun get_equiv_rel ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
in
- #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exn
+ #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
+ raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
end
fun equiv_match_err ctxt ty_pat ty =
@@ -563,7 +563,8 @@
else
let
val rtrm' = #rconst (qconsts_lookup thy qtrm)
- handle NotFound => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
+ handle Quotient_Info.NotFound =>
+ term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
in
if Pattern.matches thy (rtrm', rtrm)
then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
--- a/src/HOL/Tools/sat_funcs.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Fri Oct 29 11:07:21 2010 +0200
@@ -274,22 +274,6 @@
| string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
(* ------------------------------------------------------------------------- *)
-(* take_prefix: *)
-(* take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *)
-(* ------------------------------------------------------------------------- *)
-
-(* int -> 'a list -> 'a list * 'a list *)
-
-fun take_prefix n xs =
-let
- fun take 0 (rxs, xs) = (rev rxs, xs)
- | take _ (rxs, []) = (rev rxs, [])
- | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs)
-in
- take n ([], xs)
-end;
-
-(* ------------------------------------------------------------------------- *)
(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *)
(* a proof from the resulting proof trace of the SAT solver. The *)
(* theorem returned is just "False" (with some of the given clauses as *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Iff_Oracle.thy Fri Oct 29 11:07:21 2010 +0200
@@ -0,0 +1,76 @@
+(* Title: HOL/ex/Iff_Oracle.thy
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Makarius
+*)
+
+header {* Example of Declaring an Oracle *}
+
+theory Iff_Oracle
+imports Main
+begin
+
+subsection {* Oracle declaration *}
+
+text {*
+ This oracle makes tautologies of the form @{prop "P <-> P <-> P <-> P"}.
+ The length is specified by an integer, which is checked to be even
+ and positive.
+*}
+
+oracle iff_oracle = {*
+ let
+ fun mk_iff 1 = Var (("P", 0), @{typ bool})
+ | mk_iff n = HOLogic.mk_eq (Var (("P", 0), @{typ bool}), mk_iff (n - 1));
+ in
+ fn (thy, n) =>
+ if n > 0 andalso n mod 2 = 0
+ then Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
+ else raise Fail ("iff_oracle: " ^ string_of_int n)
+ end
+*}
+
+
+subsection {* Oracle as low-level rule *}
+
+ML {* iff_oracle (@{theory}, 2) *}
+ML {* iff_oracle (@{theory}, 10) *}
+ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *}
+
+text {* These oracle calls had better fail. *}
+
+ML {*
+ (iff_oracle (@{theory}, 5); error "Bad oracle")
+ handle Fail _ => warning "Oracle failed, as expected"
+*}
+
+ML {*
+ (iff_oracle (@{theory}, 1); error "Bad oracle")
+ handle Fail _ => warning "Oracle failed, as expected"
+*}
+
+
+subsection {* Oracle as proof method *}
+
+method_setup iff = {*
+ Scan.lift Parse.nat >> (fn n => fn ctxt =>
+ SIMPLE_METHOD
+ (HEADGOAL (rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
+ handle Fail _ => no_tac))
+*} "iff oracle"
+
+
+lemma "A <-> A"
+ by (iff 2)
+
+lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
+ by (iff 10)
+
+lemma "A <-> A <-> A <-> A <-> A"
+ apply (iff 5)?
+ oops
+
+lemma A
+ apply (iff 1)?
+ oops
+
+end
--- a/src/HOL/ex/ROOT.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Oct 29 11:07:21 2010 +0200
@@ -12,6 +12,7 @@
];
use_thys [
+ "Iff_Oracle",
"Numeral",
"Higher_Order_Logic",
"Abstract_NAT",
--- a/src/Pure/Concurrent/simple_thread.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Fri Oct 29 11:07:21 2010 +0200
@@ -32,21 +32,21 @@
fun synchronized name lock e =
if Multithreading.available then
Exn.release (uninterruptible (fn restore_attributes => fn () =>
- let
- val immediate =
- if Mutex.trylock lock then true
- else
- let
- val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
- val time = Multithreading.real_time Mutex.lock lock;
- val _ = Multithreading.tracing_time true time
- (fn () => name ^ ": locked after " ^ Time.toString time);
- in false end;
- val result = Exn.capture (restore_attributes e) ();
- val _ =
- if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
- val _ = Mutex.unlock lock;
- in result end) ())
+ let
+ val immediate =
+ if Mutex.trylock lock then true
+ else
+ let
+ val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
+ val time = Multithreading.real_time Mutex.lock lock;
+ val _ = Multithreading.tracing_time true time
+ (fn () => name ^ ": locked after " ^ Time.toString time);
+ in false end;
+ val result = Exn.capture (restore_attributes e) ();
+ val _ =
+ if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
+ val _ = Mutex.unlock lock;
+ in result end) ())
else e ();
end;
--- a/src/Pure/General/exn.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Pure/General/exn.ML Fri Oct 29 11:07:21 2010 +0200
@@ -11,12 +11,13 @@
val get_exn: 'a result -> exn option
val capture: ('a -> 'b) -> 'a -> 'b result
val release: 'a result -> 'a
- val map_result: ('a -> 'a) -> 'a result -> 'a result
+ val map_result: ('a -> 'b) -> 'a result -> 'b result
exception Interrupt
val interrupt: unit -> 'a
val is_interrupt: exn -> bool
val interrupt_exn: 'a result
val is_interrupt_exn: 'a result -> bool
+ val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
exception EXCEPTIONS of exn list
val flatten: exn -> exn list
val flatten_list: exn list -> exn list
@@ -45,7 +46,7 @@
| release (Exn e) = reraise e;
fun map_result f (Result x) = Result (f x)
- | map_result f e = e;
+ | map_result f (Exn e) = (Exn e);
(* interrupts *)
@@ -55,7 +56,7 @@
fun interrupt () = raise Interrupt;
fun is_interrupt Interrupt = true
- | is_interrupt (IO.Io {cause = Interrupt, ...}) = true
+ | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
| is_interrupt _ = false;
val interrupt_exn = Exn Interrupt;
@@ -63,6 +64,9 @@
fun is_interrupt_exn (Exn exn) = is_interrupt exn
| is_interrupt_exn _ = false;
+fun interruptible_capture f x =
+ Result (f x) handle e => if is_interrupt e then reraise e else Exn e;
+
(* nested exceptions *)
--- a/src/Pure/IsaMakefile Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Pure/IsaMakefile Fri Oct 29 11:07:21 2010 +0200
@@ -20,6 +20,7 @@
## Pure
BOOTSTRAP_FILES = \
+ General/exn.ML \
ML-Systems/bash.ML \
ML-Systems/compiler_polyml-5.2.ML \
ML-Systems/compiler_polyml-5.3.ML \
@@ -73,7 +74,6 @@
General/basics.ML \
General/binding.ML \
General/buffer.ML \
- General/exn.ML \
General/file.ML \
General/graph.ML \
General/heap.ML \
--- a/src/Pure/Isar/local_defs.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Pure/Isar/local_defs.ML Fri Oct 29 11:07:21 2010 +0200
@@ -44,8 +44,9 @@
fun cert_def ctxt eq =
let
- fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
- quote (Syntax.string_of_term ctxt eq));
+ fun err msg =
+ cat_error msg ("The error(s) above occurred in definition:\n" ^
+ quote (Syntax.string_of_term ctxt eq));
val ((lhs, _), eq') = eq
|> Sign.no_vars ctxt
|> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
@@ -245,7 +246,7 @@
(CONVERSION (meta_rewrite_conv ctxt') THEN'
MetaSimplifier.rewrite_goal_tac [def] THEN'
resolve_tac [Drule.reflexive_thm])))
- handle ERROR msg => cat_error msg "Failed to prove definitional specification."
+ handle ERROR msg => cat_error msg "Failed to prove definitional specification"
end;
in (((c, T), rhs), prove) end;
--- a/src/Pure/ML/ml_antiquote.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Fri Oct 29 11:07:21 2010 +0200
@@ -71,12 +71,6 @@
"Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
|| Scan.succeed "ML_Context.the_global_context ()");
-val _ = value "theory_ref"
- (Scan.lift Args.name >> (fn name =>
- "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^
- ML_Syntax.print_string name ^ ")")
- || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
-
val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
--- a/src/Pure/Syntax/syn_trans.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Fri Oct 29 11:07:21 2010 +0200
@@ -547,7 +547,7 @@
fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
| ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
- val exn_results = map (Exn.capture ast_of) pts;
+ val exn_results = map (Exn.interruptible_capture ast_of) pts;
val exns = map_filter Exn.get_exn exn_results;
val results = map_filter Exn.get_result exn_results
in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
@@ -571,7 +571,7 @@
Term.list_comb (term_of ast, map term_of asts)
| term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
- val exn_results = map (Exn.capture term_of) asts;
+ val exn_results = map (Exn.interruptible_capture term_of) asts;
val exns = map_filter Exn.get_exn exn_results;
val results = map_filter Exn.get_result exn_results
in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
--- a/src/Pure/more_thm.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Pure/more_thm.ML Fri Oct 29 11:07:21 2010 +0200
@@ -12,6 +12,7 @@
structure Ctermtab: TABLE
structure Thmtab: TABLE
val aconvc: cterm * cterm -> bool
+ type attribute = Context.generic * thm -> Context.generic * thm
end;
signature THM =
@@ -64,6 +65,7 @@
val close_derivation: thm -> thm
val add_axiom: binding * term -> theory -> (string * thm) * theory
val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
+ type attribute = Context.generic * thm -> Context.generic * thm
type binding = binding * attribute list
val empty_binding: binding
val rule_attribute: (Context.generic -> thm -> thm) -> attribute
@@ -382,6 +384,9 @@
(** attributes **)
+(*attributes subsume any kind of rules or context modifiers*)
+type attribute = Context.generic * thm -> Context.generic * thm;
+
type binding = binding * attribute list;
val empty_binding: binding = (Binding.empty, []);
--- a/src/Pure/thm.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Pure/thm.ML Fri Oct 29 11:07:21 2010 +0200
@@ -39,7 +39,6 @@
(*theorems*)
type thm
type conv = cterm -> thm
- type attribute = Context.generic * thm -> Context.generic * thm
val rep_thm: thm ->
{thy_ref: theory_ref,
tags: Properties.T,
@@ -350,9 +349,6 @@
type conv = cterm -> thm;
-(*attributes subsume any kind of rules or context modifiers*)
-type attribute = Context.generic * thm -> Context.generic * thm;
-
(*errors involving theorems*)
exception THM of string * int * thm list;
--- a/src/Tools/Code/code_runtime.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Oct 29 11:07:21 2010 +0200
@@ -105,7 +105,7 @@
val (program_code, [SOME value_name']) = serializer naming program' [value_name];
val value_code = space_implode " "
(value_name' :: "()" :: map (enclose "(" ")") args);
- in Exn.capture (value ctxt cookie) (program_code, value_code) end;
+ in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
fun partiality_as_none e = SOME (Exn.release e)
handle General.Match => NONE
--- a/src/Tools/quickcheck.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/Tools/quickcheck.ML Fri Oct 29 11:07:21 2010 +0200
@@ -170,9 +170,10 @@
fun mk_testers_strict ctxt t =
let
- val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
- val testers = map (fn generator => Exn.capture (generator ctxt) t) generators;
- in if forall (is_none o Exn.get_result) testers
+ val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
+ val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators;
+ in
+ if forall (is_none o Exn.get_result) testers
then [(Exn.release o snd o split_last) testers]
else map_filter Exn.get_result testers
end;
--- a/src/ZF/simpdata.ML Fri Oct 29 11:04:41 2010 +0200
+++ b/src/ZF/simpdata.ML Fri Oct 29 11:07:21 2010 +0200
@@ -59,10 +59,10 @@
in
-val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
+val defBEX_regroup = Simplifier.simproc_global @{theory}
"defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
-val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
+val defBALL_regroup = Simplifier.simproc_global @{theory}
"defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
end;