src/Pure/PIDE/yxml.scala
changeset 48996 a8bad1369ada
parent 45673 cd41e3903fbf
child 55553 4a5f65df29fa
     1.1 --- a/src/Pure/PIDE/yxml.scala	Wed Aug 29 12:18:21 2012 +0200
     1.2 +++ b/src/Pure/PIDE/yxml.scala	Wed Aug 29 12:55:41 2012 +0200
     1.3 @@ -93,10 +93,10 @@
     1.4  
     1.5      /* parse chunks */
     1.6  
     1.7 -    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
     1.8 +    for (chunk <- Library.separated_chunks(X, source) if chunk.length != 0) {
     1.9        if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
    1.10        else {
    1.11 -        Library.chunks(chunk, Y).toList match {
    1.12 +        Library.separated_chunks(Y, chunk).toList match {
    1.13            case ch :: name :: atts if ch.length == 0 =>
    1.14              push(name.toString, atts.map(parse_attrib))
    1.15            case txts => for (txt <- txts) add(XML.Text(txt.toString))