equal
deleted
inserted
replaced
205 if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body) |
205 if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body) |
206 else if (is_error(elem)) Output.error_prefix(body) |
206 else if (is_error(elem)) Output.error_prefix(body) |
207 else body |
207 else body |
208 |
208 |
209 text1 + text2 |
209 text1 + text2 |
|
210 } |
|
211 |
|
212 |
|
213 /* ML profiling */ |
|
214 |
|
215 object ML_Profiling |
|
216 { |
|
217 def unapply(msg: XML.Tree): Option[isabelle.ML_Profiling.Report] = |
|
218 msg match { |
|
219 case XML.Elem(_, List(tree)) if is_warning(msg) => |
|
220 Markup.ML_Profiling.unapply_report(tree) |
|
221 case _ => None |
|
222 } |
210 } |
223 } |
211 |
224 |
212 |
225 |
213 /* export */ |
226 /* export */ |
214 |
227 |