src/Pure/PIDE/xml.scala
changeset 80435 de2ea807edd2
parent 80434 6f1c8084f672
child 80438 73e526bdb0dd
equal deleted inserted replaced
80434:6f1c8084f672 80435:de2ea807edd2
   122 
   122 
   123 
   123 
   124   /* traverse text */
   124   /* traverse text */
   125 
   125 
   126   def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = {
   126   def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = {
   127     def traverse(x: A, t: Tree): A =
   127     @tailrec def trav(x: A, list: List[Tree]): A =
   128       t match {
   128       list match {
   129         case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
   129         case Nil => x
   130         case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
   130         case XML.Wrapped_Elem(_, _, body) :: rest => trav(x, body ::: rest)
   131         case XML.Text(s) => op(x, s)
   131         case XML.Elem(_, body) :: rest => trav(x, body ::: rest)
   132       }
   132         case XML.Text(s) :: rest => trav(op(x, s), rest)
   133     body.foldLeft(a)(traverse)
   133       }
       
   134     trav(a, body)
   134   }
   135   }
   135 
   136 
   136   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
   137   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
   137   def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
   138   def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
   138 
   139