# HG changeset patch
# User wenzelm
# Date 1220432948 -7200
# Node ID b79e61861f0fb4bb3df3976f39292abdb4ca6ef4
# Parent  d27ea294fdd38cd0d788d622834448eb0d7afb0b
simplified Toplevel.add_hook: cover successful transactions only;

diff -r d27ea294fdd3 -r b79e61861f0f NEWS
--- 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
diff -r d27ea294fdd3 -r b79e61861f0f src/Pure/Isar/toplevel.ML
--- 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;
diff -r d27ea294fdd3 -r b79e61861f0f src/Pure/ProofGeneral/proof_general_emacs.ML
--- 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
diff -r d27ea294fdd3 -r b79e61861f0f src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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 ()