# HG changeset patch
# User wenzelm
# Date 1087828798 -7200
# Node ID fefcf6cd858ad30e5deb2c9f78086b454bba266a
# Parent  edbc81e6080906c608003541e4147a1e4bb160f5
added >>> : transition list -> unit;

diff -r edbc81e60809 -r fefcf6cd858a src/Pure/Isar/toplevel.ML
--- 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;