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

[Christian Urban]

On Thursday, April 4, 2013 at 12:42:42 (+0200), Makarius wrote:
 > 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?  

Could the reason be that more often than wanted the answer to
emails on the Isabelle mailing lists is: 

  "person ?X, you have no business here" 

  "any changes to ?X are restricted to exactly one person"
  
  you are on the wrong mailing list (isabelle vs isabelle-dev)

  you did not look up the history from ?X years ago

  you did not follow conventions (usually about *informal* 
  conventions for theory names, ML-styles, source comments etc)

  you better refer to changesets with [cryptic] hashes like dd6dd81381fb 
  
  this is not a bug, but a running gag


Maybe the latter answers might be more perceived answers
than actual answers, but I hope people get the gist.

Christian