equal
deleted
inserted
replaced
92 } |
92 } |
93 |
93 |
94 |
94 |
95 /* document object model (W3C DOM) */ |
95 /* document object model (W3C DOM) */ |
96 |
96 |
|
97 def get_data(node: Node): Option[XML.Tree] = |
|
98 node.getUserData(Markup.DATA) match { |
|
99 case tree: XML.Tree => Some(tree) |
|
100 case _ => None |
|
101 } |
|
102 |
97 def document_node(doc: Document, tree: Tree): Node = |
103 def document_node(doc: Document, tree: Tree): Node = |
98 { |
104 { |
99 def DOM(tr: Tree): Node = tr match { |
105 def DOM(tr: Tree): Node = tr match { |
100 case Elem(Markup.DATA, Nil, List(data, t)) => |
106 case Elem(Markup.DATA, Nil, List(data, t)) => |
101 val node = DOM(t) |
107 val node = DOM(t) |