# HG changeset patch
# User berghofe
# Date 1105449279 -3600
# Node ID 6f4959ba7664859446e1fce4dbfb50e980f5873d
# Parent  1e1aeaf1dec376ffb8c5fda2d0918030bbc6a450
excursion_result now also passes previous state to presentation functions.
This is useful for hiding proof scripts.

diff -r 1e1aeaf1dec3 -r 6f4959ba7664 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jan 11 14:08:07 2005 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Jan 11 14:14:39 2005 +0100
@@ -68,7 +68,7 @@
   val quiet: bool ref
   val exn_message: exn -> string
   val apply: bool -> transition -> state -> (state * (exn * string) option) option
-  val excursion_result: ((transition * (state -> 'a -> 'a)) list * 'a) -> 'a
+  val excursion_result: ((transition * (state -> state -> 'a -> 'a)) list * 'a) -> 'a
   val excursion: transition list -> unit
   val set_state: state -> unit
   val get_state: unit -> state
@@ -480,7 +480,7 @@
   | excur ((tr, f) :: trs) (st, res) =
       (case apply false tr st of
         Some (st', None) =>
-          excur trs (st', transform_error (fn () => f st' res) () handle exn =>
+          excur trs (st', transform_error (fn () => f st st' res) () handle exn =>
             raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
       | Some (st', Some exn_info) => raise EXCURSION_FAIL exn_info
       | None => raise EXCURSION_FAIL (TERMINATE, at_command tr));
@@ -494,7 +494,7 @@
   handle exn => error (exn_message exn);
 
 fun excursion trs =
-  excursion_result (map (fn tr => (tr, fn _ => fn _ => ())) trs, ());
+  excursion_result (map (fn tr => (tr, fn _ => fn _ => fn _ => ())) trs, ());
 
 end;