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

[Makarius]

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.


 	Makarius