simplified Toplevel.add_hook: cover successful transactions only;
authorwenzelm
Wed Sep 03 11:09:08 2008 +0200 (2008-09-03)
changeset 28103b79e61861f0f
parent 28102 d27ea294fdd3
child 28104 c62364a6aeed
simplified Toplevel.add_hook: cover successful transactions only;
NEWS
src/Pure/Isar/toplevel.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/NEWS	Wed Sep 03 00:11:27 2008 +0200
     1.2 +++ b/NEWS	Wed Sep 03 11:09:08 2008 +0200
     1.3 @@ -181,9 +181,9 @@
     1.4  *** ML ***
     1.5  
     1.6  * Generic Toplevel.add_hook interface allows to analyze the result of
     1.7 -transactions (including failed ones).  For example, see
     1.8 -src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency
     1.9 -output of transactions resulting in a new theory state.
    1.10 +transactions.  E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML
    1.11 +for theorem dependency output of transactions resulting in a new
    1.12 +theory state.
    1.13  
    1.14  * Name bindings in higher specification mechanisms (notably
    1.15  LocalTheory.define, LocalTheory.note, and derived packages) are now
     2.1 --- a/src/Pure/Isar/toplevel.ML	Wed Sep 03 00:11:27 2008 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Sep 03 11:09:08 2008 +0200
     2.3 @@ -88,7 +88,7 @@
     2.4    val unknown_context: transition -> transition
     2.5    val status: transition -> Markup.T -> unit
     2.6    val error_msg: transition -> exn * string -> unit
     2.7 -  val add_hook: (transition -> state -> state * (exn * string) option -> unit) -> unit
     2.8 +  val add_hook: (transition -> state -> state -> unit) -> unit
     2.9    val transition: bool -> transition -> state -> (state * (exn * string) option) option
    2.10    val commit_exit: transition
    2.11    val excursion: transition list -> unit
    2.12 @@ -615,7 +615,7 @@
    2.13  
    2.14  (* post-transition hooks *)
    2.15  
    2.16 -local val hooks = ref ([]: (transition -> state -> state * (exn * string) option -> unit) list) in
    2.17 +local val hooks = ref ([]: (transition -> state -> state -> unit) list) in
    2.18  
    2.19  fun add_hook f = CRITICAL (fn () => change hooks (cons f));
    2.20  fun get_hooks () = CRITICAL (fn () => ! hooks);
    2.21 @@ -648,16 +648,16 @@
    2.22  fun transition int tr st =
    2.23    let
    2.24      val hooks = get_hooks ();
    2.25 -    fun apply_hooks st_err = hooks |> List.app (fn f => (try (fn () => f tr st st_err) (); ()));
    2.26 +    fun apply_hooks st' = hooks |> List.app (fn f => (try (fn () => f tr st st') (); ()));
    2.27  
    2.28      val ctxt = try context_of st;
    2.29      val res =
    2.30        (case app int tr st of
    2.31          (_, SOME TERMINATE) => NONE
    2.32 -      | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
    2.33 -      | (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr))
    2.34 -      | (state', NONE) => SOME (state', NONE));
    2.35 -    val _ = Option.map apply_hooks res;
    2.36 +      | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
    2.37 +      | (st', SOME exn) => SOME (st', SOME (exn_context ctxt exn, at_command tr))
    2.38 +      | (st', NONE) => SOME (st', NONE));
    2.39 +    val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
    2.40    in res end;
    2.41  
    2.42  end;
     3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Sep 03 00:11:27 2008 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Sep 03 11:09:08 2008 +0200
     3.3 @@ -175,8 +175,8 @@
     3.4  
     3.5  in
     3.6  
     3.7 -fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
     3.8 -  if print_mode_active thm_depsN andalso Toplevel.is_theory state' andalso is_none opt_err then
     3.9 +fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
    3.10 +  if print_mode_active thm_depsN andalso Toplevel.is_theory state' then
    3.11      let val (names, deps) =
    3.12        ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
    3.13      in
     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Sep 03 00:11:27 2008 +0200
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Sep 03 11:09:08 2008 +0200
     4.3 @@ -296,10 +296,9 @@
     4.4  
     4.5  in
     4.6  
     4.7 -fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
     4.8 +fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
     4.9    if ! show_theorem_dependencies andalso
    4.10 -    can Toplevel.theory_of state andalso
    4.11 -    Toplevel.is_theory state' andalso is_none opt_err
    4.12 +    can Toplevel.theory_of state andalso Toplevel.is_theory state'
    4.13    then
    4.14      let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
    4.15        if null names orelse null deps then ()