--- a/NEWS Wed Sep 03 00:11:27 2008 +0200
+++ b/NEWS Wed Sep 03 11:09:08 2008 +0200
@@ -181,9 +181,9 @@
*** ML ***
* Generic Toplevel.add_hook interface allows to analyze the result of
-transactions (including failed ones). For example, see
-src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency
-output of transactions resulting in a new theory state.
+transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML
+for theorem dependency output of transactions resulting in a new
+theory state.
* Name bindings in higher specification mechanisms (notably
LocalTheory.define, LocalTheory.note, and derived packages) are now
--- a/src/Pure/Isar/toplevel.ML Wed Sep 03 00:11:27 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Sep 03 11:09:08 2008 +0200
@@ -88,7 +88,7 @@
val unknown_context: transition -> transition
val status: transition -> Markup.T -> unit
val error_msg: transition -> exn * string -> unit
- val add_hook: (transition -> state -> state * (exn * string) option -> unit) -> unit
+ val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val commit_exit: transition
val excursion: transition list -> unit
@@ -615,7 +615,7 @@
(* post-transition hooks *)
-local val hooks = ref ([]: (transition -> state -> state * (exn * string) option -> unit) list) in
+local val hooks = ref ([]: (transition -> state -> state -> unit) list) in
fun add_hook f = CRITICAL (fn () => change hooks (cons f));
fun get_hooks () = CRITICAL (fn () => ! hooks);
@@ -648,16 +648,16 @@
fun transition int tr st =
let
val hooks = get_hooks ();
- fun apply_hooks st_err = hooks |> List.app (fn f => (try (fn () => f tr st st_err) (); ()));
+ fun apply_hooks st' = hooks |> List.app (fn f => (try (fn () => f tr st st') (); ()));
val ctxt = try context_of st;
val res =
(case app int tr st of
(_, SOME TERMINATE) => NONE
- | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
- | (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr))
- | (state', NONE) => SOME (state', NONE));
- val _ = Option.map apply_hooks res;
+ | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
+ | (st', SOME exn) => SOME (st', SOME (exn_context ctxt exn, at_command tr))
+ | (st', NONE) => SOME (st', NONE));
+ val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
in res end;
end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Sep 03 00:11:27 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Sep 03 11:09:08 2008 +0200
@@ -175,8 +175,8 @@
in
-fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
- if print_mode_active thm_depsN andalso Toplevel.is_theory state' andalso is_none opt_err then
+fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
+ if print_mode_active thm_depsN andalso Toplevel.is_theory state' then
let val (names, deps) =
ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
in
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Sep 03 00:11:27 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Sep 03 11:09:08 2008 +0200
@@ -296,10 +296,9 @@
in
-fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
+fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
if ! show_theorem_dependencies andalso
- can Toplevel.theory_of state andalso
- Toplevel.is_theory state' andalso is_none opt_err
+ can Toplevel.theory_of state andalso Toplevel.is_theory state'
then
let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
if null names orelse null deps then ()