equal
deleted
inserted
replaced
138 (** markup **) |
138 (** markup **) |
139 |
139 |
140 fun output_result (id, data) = |
140 fun output_result (id, data) = |
141 Output.result (Markup.serial_properties id) data |
141 Output.result (Markup.serial_properties id) data |
142 |
142 |
143 val serialN = "serial" |
|
144 val parentN = "parent" |
143 val parentN = "parent" |
145 val textN = "text" |
144 val textN = "text" |
146 val memoryN = "memory" |
145 val memoryN = "memory" |
147 val successN = "success" |
146 val successN = "success" |
148 |
147 |