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

2013-04-04 Thread 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)

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

2013-04-04 Thread 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

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

2013-04-04 Thread Gerwin Klein
On 04/04/2013, at 12:42 PM, Makarius makar...@sketis.net 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

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

2013-04-04 Thread Makarius
On Fri, 5 Apr 2013, David Greenaway wrote: What practical things could such volunteers do that you would find helpful? So how about maintaining Proof General, seriously, no-nonse? And there are other unmaintained parts, such as WWW_Find. (Note that several other people have worked there

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

2013-04-04 Thread David Greenaway
On 05/04/13 09:32, Makarius wrote: On Fri, 5 Apr 2013, David Greenaway wrote: What practical things could such volunteers do that you would find helpful? So how about maintaining Proof General, seriously, no-nonse? As somebody who isn't a Proof General user, nor an Emacs user, nor has ever