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

2013-04-03 Thread David Greenaway
Hi Makarius, On 02/04/13 21:17, Makarius wrote: On Tue, 2 Apr 2013, David Greenaway wrote: I would appreciate it if an Isabelle expert could review that patch and, if acceptable, apply it to mainline. (This can be easily done with hg import patch-file). before you send more patches, can

[isabelle-dev] Where are the error messages?

2013-04-03 Thread Dmitriy Traytel
Hi, theory Scratch imports Main begin term True x thm TrueI[OF TrueI] end behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands there is no indication of errors (except of the absence of a popup). This seams to apply to all Isar commands involving

Re: [isabelle-dev] Where are the error messages?

2013-04-03 Thread Makarius
On Wed, 3 Apr 2013, Dmitriy Traytel wrote: theory Scratch imports Main begin term True x thm TrueI[OF TrueI] end behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands there is no indication of errors (except of the absence of a popup). This seams to apply to all

Re: [isabelle-dev] Where are the error messages?

2013-04-03 Thread Makarius
On Wed, 3 Apr 2013, Dmitriy Traytel wrote: theory Scratch imports Main begin term True x thm TrueI[OF TrueI] end behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands there is no indication of errors (except of the absence of a popup). This seams to apply to all

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

2013-04-03 Thread Alexander Krauss
Hi David, On 04/03/2013 09:18 AM, David Greenaway wrote: On 02/04/13 21:17, Makarius wrote: before you send more patches, can you please go back to the very start of the mail thread from last time, which contains a lot of hints how things are done, including pointers to the documentation. I

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

2013-04-03 Thread David Greenaway
Hi Alexander, Thanks for your helpful reply. On 04/04/13 08:58, Alexander Krauss wrote: Hi David, On 04/03/2013 09:18 AM, David Greenaway wrote: [...] Does my 4 line patch violate the Isabelle style guidelines, or have I missed something about the correct etiquette for submitting patches?