[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
makarius at sketis.net
Thu Apr 4 12:37:12 CEST 2013
On Wed, 3 Apr 2013, Alexander Krauss wrote:
Thanks Alex, it always helps if someone else with substantial experience
explains things, so that I am not the lone voice in the desert. I let
your nice explanations stand as is.
> The area of your issue (interaction with the underlying ML system) is
> maintained by Makarius pretty much exclusively.
Just one concrete note here: it is David Matthews working here with me for
many years, to make it work very smoothly with Poly/ML while keeping
SML/NJ and older versions of Poly/ML on board somehow. I started myself
with ML pretty printing already in 1993, and can't say that will ever be
finished. In the mid-1990-ies there were certain gross shortcomings that
were even officially documented.
Note that when I venture myself to propose actual "patches" to Poly/ML,
the first thing David usually does is to turn the idea behind it in a
proper implementation in the sense of his code base, where he is the
proven expert. I am glad that he does take the time, and not just apply
the proposed patch and thus endanger the system integrity.
Also note that when I "improved" myself exception printing just some
months before the Isabelle2013, I messed up SML/NJ in a subtle way that
was not immediately visible. As a consequence some software archeologists
who try to reactivate Isabelle2013 in the distant future will have
problems working with it practically, because ML errors just produce
"exception Option raised".
So a change can never be a "fix". It is just some entropy on the code
base. Special efforts and attention is required to keep a positive
balance in the end.
More information about the isabelle-dev