--- a/src/Pure/Thy/thy_syntax.ML Fri Mar 01 22:15:31 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Sun Mar 03 13:23:06 2013 +0100
@@ -16,6 +16,8 @@
val present_span: span -> Output.output
val parse_spans: Token.T list -> span list
datatype 'a element = Element of 'a * ('a element list * 'a) option
+ val atom: 'a -> 'a element
+ val fold_element: ('a -> 'b -> 'b) -> 'a element -> 'b -> 'b
val map_element: ('a -> 'b) -> 'a element -> 'b element
val flat_element: 'a element -> 'a list
val last_element: 'a element -> 'a
@@ -142,6 +144,9 @@
fun element (a, b) = Element (a, SOME b);
fun atom a = Element (a, NONE);
+fun fold_element f (Element (a, NONE)) = f a
+ | fold_element f (Element (a, SOME (elems, b))) = f a #> (fold o fold_element) f elems #> f b;
+
fun map_element f (Element (a, NONE)) = Element (f a, NONE)
| map_element f (Element (a, SOME (elems, b))) =
Element (f a, SOME ((map o map_element) f elems, f b));