[isabelle-dev] proper use of "error" channel
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
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