[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks

[Makarius]

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.


 	Makarius