--- a/src/Pure/General/stack.ML Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/General/stack.ML Thu Aug 30 19:18:49 2012 +0200
@@ -10,7 +10,9 @@
val level: 'a T -> int
val init: 'a -> 'a T
val top: 'a T -> 'a
+ val bottom: 'a T -> 'a
val map_top: ('a -> 'a) -> 'a T -> 'a T
+ val map_bottom: ('a -> 'a) -> 'a T -> 'a T
val map_all: ('a -> 'a) -> 'a T -> 'a T
val push: 'a T -> 'a T
val pop: 'a T -> 'a T (*exception List.Empty*)
@@ -27,8 +29,16 @@
fun top (x, _) = x;
+fun bottom (x, []) = x
+ | bottom (_, xs) = List.last xs;
+
fun map_top f (x, xs) = (f x, xs);
+fun map_bottom f (x, []) = (f x, [])
+ | map_bottom f (x, rest) =
+ let val (ys, z) = split_last rest
+ in (x, ys @ [f z]) end;
+
fun map_all f (x, xs) = (f x, map f xs);
fun push (x, xs) = (x, x :: xs);