equal
deleted
inserted
replaced
99 |
99 |
100 def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = |
100 def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = |
101 { |
101 { |
102 def traverse(x: A, t: Tree): A = |
102 def traverse(x: A, t: Tree): A = |
103 t match { |
103 t match { |
104 case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse) |
104 case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse) |
105 case XML.Elem(_, ts) => (x /: ts)(traverse) |
105 case XML.Elem(_, ts) => ts.foldLeft(x)(traverse) |
106 case XML.Text(s) => op(x, s) |
106 case XML.Text(s) => op(x, s) |
107 } |
107 } |
108 (a /: body)(traverse) |
108 body.foldLeft(a)(traverse) |
109 } |
109 } |
110 |
110 |
111 def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length } |
111 def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length } |
112 |
112 |
113 |
113 |