equal
deleted
inserted
replaced
21 val command: Command, |
21 val command: Command, |
22 val status: List[Markup] = Nil, |
22 val status: List[Markup] = Nil, |
23 val results: SortedMap[Long, XML.Tree] = SortedMap.empty, |
23 val results: SortedMap[Long, XML.Tree] = SortedMap.empty, |
24 val markup: Markup_Tree = Markup_Tree.empty) |
24 val markup: Markup_Tree = Markup_Tree.empty) |
25 { |
25 { |
|
26 def markup_to_XML: XML.Body = markup.to_XML(command.source) |
|
27 |
|
28 |
26 /* accumulate content */ |
29 /* accumulate content */ |
27 |
30 |
28 private def add_status(st: Markup): State = copy(status = st :: status) |
31 private def add_status(st: Markup): State = copy(status = st :: status) |
29 private def add_markup(m: Text.Markup): State = copy(markup = markup + m) |
32 private def add_markup(m: Text.Markup): State = copy(markup = markup + m) |
30 |
33 |