equal
deleted
inserted
replaced
231 fun raised name = "exception " ^ name ^ " raised"; |
231 fun raised name = "exception " ^ name ^ " raised"; |
232 fun raised_msg name msg = raised name ^ ": " ^ msg; |
232 fun raised_msg name msg = raised name ^ ": " ^ msg; |
233 |
233 |
234 fun exn_message TERMINATE = "Exit." |
234 fun exn_message TERMINATE = "Exit." |
235 | exn_message (BREAK _) = "Break." |
235 | exn_message (BREAK _) = "Break." |
|
236 | exn_message (FAIL (exn, msg)) = cat_lines [exn_message exn, msg] |
236 | exn_message Interrupt = "Interrupt (exec)." |
237 | exn_message Interrupt = "Interrupt (exec)." |
237 | exn_message (ERROR_MESSAGE msg) = msg |
238 | exn_message (ERROR_MESSAGE msg) = msg |
238 | exn_message (THEORY (msg, _)) = msg |
239 | exn_message (THEORY (msg, _)) = msg |
239 | exn_message (ProofContext.CONTEXT (msg, _)) = msg |
240 | exn_message (ProofContext.CONTEXT (msg, _)) = msg |
240 | exn_message (Proof.STATE (msg, _)) = msg |
241 | exn_message (Proof.STATE (msg, _)) = msg |