Re: [isabelle-dev] Proof General 4.1pre

2011-01-13 Thread Andreas Lochbihler
> Are there still users of PG 3.x with recent Isabelle snapshots or versions > from the repository? I am using PG 3.7.1.1 with XEmacs 21.4.21 and a recent version from the Isabelle repository. My motivation for not switching is that PG 4.x did not seem to work with XEmacs when I tried, and I hav

[isabelle-dev] erroneous "Legacy feature" warnings about secondary search path

2011-01-13 Thread Brian Huffman
Hello all, I recently discovered that warnings about the secondard search path are generated more often than they ought to be. I am using repository version 1fa4725c4656. Create two files A.thy and B.thy with the following contents: theory A imports "~~/src/HOL/Library/Cardinality" begin end th

Re: [isabelle-dev] Proof General 4.1pre

2011-01-13 Thread Gerwin Klein
On 14/01/2011, at 1:39 AM, Makarius wrote: > There is now a development snapshot of Proof General 4.1pre, provided by > David Aspinall: > > http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.1pre110112.tgz > > It looks pretty stable to me. There are only few remaining entries at > http:

Re: [isabelle-dev] Proof General 4.1pre

2011-01-13 Thread Clemens Ballarin
Quoting Makarius : Are there still users of PG 3.x with recent Isabelle snapshots or versions from the repository? I do. I recently tried to use PG 4.0 with Aquamacs 2.1. That didn't seem to work, so I went back to PG 3.7.1.1 and Carbon Emacs 1.6 (based on GNU Emacs 22.3.1). I'd prefer

Re: [isabelle-dev] Proof General 4.1pre

2011-01-13 Thread Alexander Krauss
The question is if PG 4.1 converges sufficiently fast for Isabelle2011, and if we should switch to the PGIP update for floating point settings. This would mean to discontinue 4.0 and 3.x altogether. I've been using PG 4.1 for a while now from cvs, and it works nicely, except that I've regularl

[isabelle-dev] Proof General 4.1pre

2011-01-13 Thread Makarius
There is now a development snapshot of Proof General 4.1pre, provided by David Aspinall: http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.1pre110112.tgz It looks pretty stable to me. There are only few remaining entries at http://proofgeneral.inf.ed.ac.uk/trac/ Are there still user

Re: [isabelle-dev] [rt.cl.cam.ac.uk #73409] Re: Accented characters

2011-01-13 Thread Martyn Johnson via RT
> I am surprised that the web server cannot be configured to add the UTF-8 > default encoding only when the page doesn't declare its own encoding. Indeed. I presume it doesn't want to be fussed with parsing the page, which is the browser's job. It's interesting that Apache's built-in default is

Re: [isabelle-dev] [rt.cl.cam.ac.uk #73409] Re: Accented characters

2011-01-13 Thread Tjark Weber via RT
On Thu, 2011-01-13 at 11:48 +, Piete Brooks via RT wrote: > > Indeed this appears to be a configuration issue with the Cambridge web > > server. > > See http://www.cl.cam.ac.uk/news/2011/01/web-server-changes/ I am surprised that the web server cannot be configured to add the UTF-8 default en

Re: [isabelle-dev] Accented characters

2011-01-13 Thread Johannes Hölzl
Am Donnerstag, den 13.01.2011, 12:33 +0100 schrieb Lars Noschinski: > On 13.01.2011 12:15, Gerwin Klein wrote: > > On 13/01/2011, at 8:51 PM, Larry Paulson wrote: > > > >> Accented characters on our website no longer display correctly on > >> Macs. I don't know precisely when this happened, but I'm

[isabelle-dev] [rt.cl.cam.ac.uk #73409] Re: Accented characters

2011-01-13 Thread Martyn Johnson via RT
> So it would seem that the Cambridge web server erroneously expects all > web pages to be UTF-8 encoded. The pagemaster explicitly requested this change. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.

[isabelle-dev] [rt.cl.cam.ac.uk #73409] AutoReply: Re: Accented characters

2011-01-13 Thread Tjark Weber via RT
This message has been automatically generated in response to the creation of a trouble ticket regarding "Re: [isabelle-dev] Accented characters", a summary of which appears below. There is no need to reply to this message immediately. Your ticket has been assigned an ID of [rt.cl.cam.ac

Re: [isabelle-dev] [rt.cl.cam.ac.uk #73409] Re: Accented characters

2011-01-13 Thread Piete Brooks via RT
> Indeed this appears to be a configuration issue with the Cambridge web > server. See http://www.cl.cam.ac.uk/news/2011/01/web-server-changes/ > The character encoding specified in the HTTP header (utf-8) is different > from the value in the element (iso-8859-1). ... and it's left to the brows

Re: [isabelle-dev] Accented characters

2011-01-13 Thread Tjark Weber
On Thu, 2011-01-13 at 22:15 +1100, Gerwin Klein wrote: > On 13/01/2011, at 8:51 PM, Larry Paulson wrote: > > Accented characters on our website no longer display correctly on > > Macs. I don't know precisely when this happened, but I'm sure it's > > fairly recent. In fact, the characters don't eve

Re: [isabelle-dev] Accented characters

2011-01-13 Thread Lars Noschinski
On 13.01.2011 12:15, Gerwin Klein wrote: On 13/01/2011, at 8:51 PM, Larry Paulson wrote: Accented characters on our website no longer display correctly on Macs. I don't know precisely when this happened, but I'm sure it's fairly recent. In fact, the characters don't even display correctly in th

Re: [isabelle-dev] Accented characters

2011-01-13 Thread Gerwin Klein
On 13/01/2011, at 8:51 PM, Larry Paulson wrote: > Accented characters on our website no longer display correctly on Macs. I > don't know precisely when this happened, but I'm sure it's fairly recent. In > fact, the characters don't even display correctly in the HTML source. It may > be a charac

Re: [isabelle-dev] Accented characters

2011-01-13 Thread Tjark Weber
On Thu, 2011-01-13 at 09:51 +, Larry Paulson wrote: > Accented characters on our website no longer display correctly on > Macs. I don't know precisely when this happened, but I'm sure it's > fairly recent. In fact, the characters don't even display correctly in > the HTML source. It may be a ch