[isabelle-dev] proper use of "error" channel

Makarius makarius at sketis.net
Tue Mar 23 00:11:00 CET 2010

On Tue, 23 Mar 2010, Alexander Krauss wrote:

> How does the "sys_error" function fit into this picture? I have been 
> using this in cases where you are suggesting to raise Fail.

Good question.  It is probably a candidate for the "old-style" category, 
because it conceals the source position.  Historically, it was introduced 
when Fail did not exist yet, and the error mechanism was completely 
different anyway.

In any case, changing the exception behaviour of ML code needs some care, 
since it essentially escapes the static checking of the language.


More information about the isabelle-dev mailing list