equal
deleted
inserted
replaced
120 List(XML.Elem(Markup(Markup.WRITELN, Markup.Serial(i)), XML.string(title))) ::: |
120 List(XML.Elem(Markup(Markup.WRITELN, Markup.Serial(i)), XML.string(title))) ::: |
121 XML.string(message_suffix) |
121 XML.string(message_suffix) |
122 (results, message) |
122 (results, message) |
123 } |
123 } |
124 |
124 |
125 (results, List(XML.Elem(Markup(Markup.TRACING_MESSAGE, Nil), message))) |
125 (results, List(XML.elem(Markup.TRACING_MESSAGE, message))) |
126 } |
126 } |
127 } |
127 } |
128 } |
128 } |
129 |
129 |
130 abstract class Program_Progress extends Progress { |
130 abstract class Program_Progress extends Progress { |