--- a/src/Pure/Isar/toplevel.ML Mon Jun 21 16:39:39 2004 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Jun 21 16:39:58 2004 +0200
@@ -69,6 +69,7 @@
val get_state: unit -> state
val exn: unit -> (exn * string) option
val >> : transition -> bool
+ val >>> : transition list -> unit
type 'a isar
val loop: 'a isar -> unit
end;
@@ -489,7 +490,7 @@
(* apply transformers to global state *)
-nonfix >>;
+nonfix >> >>>;
fun >> tr =
(case apply true tr (get_state ()) of
@@ -499,6 +500,9 @@
check_stale state'; print_exn exn_info;
true));
+fun >>> [] = ()
+ | >>> (tr :: trs) = if >> tr then >>> trs else ();
+
(*Note: this is for Poly/ML only, we really do not intend to exhibit
interrupts here*)
fun get_interrupt src = Some (Source.get_single src) handle Interrupt => None;