equal
deleted
inserted
replaced
69 private def err_unbalanced(name: String) = |
69 private def err_unbalanced(name: String) = |
70 if (name == "") err("unbalanced element") |
70 if (name == "") err("unbalanced element") |
71 else err("unbalanced element " + quote(name)) |
71 else err("unbalanced element " + quote(name)) |
72 |
72 |
73 private def parse_attrib(source: CharSequence): (String, String) = |
73 private def parse_attrib(source: CharSequence): (String, String) = |
74 { |
74 Properties.Eq.unapply(source.toString) getOrElse err_attribute() |
75 val s = source.toString |
|
76 val i = s.indexOf('=') |
|
77 if (i <= 0) err_attribute() |
|
78 (s.substring(0, i), s.substring(i + 1)) |
|
79 } |
|
80 |
75 |
81 |
76 |
82 def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = |
77 def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = |
83 { |
78 { |
84 /* stack operations */ |
79 /* stack operations */ |