equal
deleted
inserted
replaced
110 |
110 |
111 def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty) |
111 def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty) |
112 |
112 |
113 def rich_text(id: Document.Command_ID, body: XML.Body): Command = |
113 def rich_text(id: Document.Command_ID, body: XML.Body): Command = |
114 { |
114 { |
115 val (text, markup) = XML.content_markup(body) |
115 val text = XML.content(body) |
|
116 val markup = Markup_Tree.from_XML(body) |
116 unparsed(id, text, markup) |
117 unparsed(id, text, markup) |
117 } |
118 } |
118 |
119 |
119 |
120 |
120 /* perspective */ |
121 /* perspective */ |