src/Pure/PIDE/xml.scala
changeset 80431 c748adebc67f
parent 80430 89cd8fedefa7
child 80432 b42f95f18a71
equal deleted inserted replaced
80430:89cd8fedefa7 80431:c748adebc67f
    61     def traverse(trees: List[Tree]): Unit = {
    61     def traverse(trees: List[Tree]): Unit = {
    62       @tailrec def trav(list: List[Trav]): Unit =
    62       @tailrec def trav(list: List[Trav]): Unit =
    63         list match {
    63         list match {
    64           case Nil =>
    64           case Nil =>
    65           case Text(s) :: rest => text(s); trav(rest)
    65           case Text(s) :: rest => text(s); trav(rest)
    66           case Elem(markup, Nil) :: rest => elem(markup, end = true); trav(rest)
    66           case Elem(markup, body) :: rest =>
    67           case Elem(markup, body) :: rest => elem(markup); trav(body ::: End(markup.name) :: rest)
    67             if (markup.is_empty) trav(body ::: rest)
       
    68             else if (body.isEmpty) { elem(markup, end = true); trav(rest) }
       
    69             else { elem(markup); trav(body ::: End(markup.name) :: rest) }
    68           case End(name) :: rest => end_elem(name); trav(rest)
    70           case End(name) :: rest => end_elem(name); trav(rest)
    69           case _ :: _ => ???
    71           case _ :: _ => ???
    70         }
    72         }
    71       trav(trees)
    73       trav(trees)
    72     }
    74     }