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