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

[Makarius]

On Fri, 5 Apr 2013, Thomas Sewell wrote:

> By comparison, David is providing you with what would be considered a 
> good bug report in most open-source communities. It comes with a clear 
> explanation not only of what the problem is but what causes it to occur, 
> and how it might be fixed. In such communities, the proposed patches are 
> nearly never applied as-is, but they provide a far more useful starting 
> point than the average bug report.

All my complaints on this (and related) mail threads can be reduced to 
this assumption about "most open-source comminities".  This universal 
standard simply does not exist, and the average open-source project just 
produces junk. Especially people from NICTA / L4.verified should care 
about the platform(s) they depend on -- this also includes Poly/ML.

Here we have a very unusual project -- it still exists after > 25 years 
and the system is in fairly good shape. This is not an accident, it is the 
consequence of a certain development process.  But the air is getting 
thinner and thinner as we still move on.

Larry had quite visionary ideas in his initial 1989 sketch of Isabelle, 
including "Programs like Isabelle are not products: when they have served 
their purpose, they are discarded."  Historically, my biggest mistake was 
to disregard that when there was still a chance.


 	Makarius