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)
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
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
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
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
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
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
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?
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).
Dear David,
before you send more patches, can you please go back to the very start of
Hi all,
I have noticed that in c ertain circumstances both Isabelle/jEdit and
Isabelle/ProofGeneral will render certain constructs with a large number
of spaces in them.
The problem can be seen with the following testcase:
definition test a b ≡ undefined
notation (output) test (test //
10 matches
Mail list logo
