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

[Makarius]

On Thu, 4 Apr 2013, Thomas Sewell wrote:

> David's investigation explains a problem we had a few years ago where 
> some custom tactics of mine were killing my colleagues' ProofGeneral 
> sessions when they encountered errors. The workaround at the time was to 
> remove all potentially useful debugging information (terms, in 
> particular) from the relevant exceptions. Unfortunately this made 
> tracking down the bugs in the tactics somewhat challenging.
>
> In hindsight, I should probably put the debug terms in the tracebuffer 
> and thrown a vanilla exception. Hindsight is perfect, of course.

So why did none of you guys ever report that?  We have a very reactive 
isabelle-users mailing list, compared to most other project's "issue 
trackers".  It is also possible to discuss anything for inter-release 
Isabelle versions here on isabelle-dev, although its reactivity needs to 
be specifically slowed down to avoid hazards in the development process.


Having a certain observation or undesirable behaviour on someone's TODO 
list for 1-2 years already, it is like to be a matter of the past now.

Instead we have a lot of wasted time here with patches that are proposed 
in a way to make it an urgent and immediate issue to be "fixed" while you 
wait.


 	Makarius