Re: [isabelle-dev] Accented characters
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 character encoding problem. Clearly, it renders correctly in Google Chrome but not in Firefox or Safari. This issue is a bit strange. It shows up on my Mac as in your picture from the Cambridge server, but it looks fine with the correct characters from the Munich and Sydney servers. It may have more to do with what the server expects as encoding in the source file than what the browser gets to see. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Accented characters
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 the HTML source. It may be a character encoding problem. Clearly, it renders correctly in Google Chrome but not in Firefox or Safari. This issue is a bit strange. It shows up on my Mac as in your picture from the Cambridge server, but it looks fine with the correct characters from the Munich and Sydney servers. It may have more to do with what the server expects as encoding in the source file than what the browser gets to see. The files are encoded in iso-8859-1 (latin-1), which is declared with an ?xml ..? processing instruction in the file. The difference between the three servers is the Content-Type header sent by the server: Cambridge: text/html; charset=utf-8 Munich: text/html Sydney: text/html; charset=iso-8859-1 Normally, the declaration in the document should override the declaration sent by the server; but probably the ?xml ..? processing instruction is ignored by Firefox and Safari, as the document is marked as html, not xml. The correct fix is to add an additional meta-element, specifying the charset, as outlined in the XHTML specification: -- Historically, the character encoding of an HTML document is either specified by a web server via the charset parameter of the HTTP Content-Type header, or via a meta element in the document itself. In an XML document, the character encoding of the document is specified on the XML declaration (e.g., ?xml version=1.0 encoding=EUC-JP?). In order to portably present documents with specific character encodings, the best approach is to ensure that the web server provides the correct headers. If this is not possible, a document that wants to set its character encoding explicitly must include both the XML declaration an encoding declaration and a meta http-equiv statement (e.g., meta http-equiv=Content-type content=text/html; charset=EUC-JP /). In XHTML-conforming user agents, the value of the encoding declaration of the XML declaration takes precedence. -- Greetings, Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Accented characters
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 even display correctly in the HTML source. It may be a character encoding problem. Clearly, it renders correctly in Google Chrome but not in Firefox or Safari. The issue also shows up on Linux. This issue is a bit strange. It shows up on my Mac as in your picture from the Cambridge server, but it looks fine with the correct characters from the Munich and Sydney servers. It may have more to do with what the server expects as encoding in the source file than what the browser gets to see. Indeed this appears to be a configuration issue with the Cambridge web server. For some of my personal pages (also delivered from Cambridge), the W3C validator shows a warning The character encoding specified in the HTTP header (utf-8) is different from the value in the meta element (iso-8859-1). So it would seem that the Cambridge web server erroneously expects all web pages to be UTF-8 encoded. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [rt.cl.cam.ac.uk #73409] AutoReply: Re: Accented characters
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.uk #73409]. Please include this in the subject line of all future correspondence about this issue. To do so, you may reply to this message. sys-ad...@cl.cam.ac.uk - 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 even display correctly in the HTML source. It may be a character encoding problem. Clearly, it renders correctly in Google Chrome but not in Firefox or Safari. The issue also shows up on Linux. This issue is a bit strange. It shows up on my Mac as in your picture from the Cambridge server, but it looks fine with the correct characters from the Munich and Sydney servers. It may have more to do with what the server expects as encoding in the source file than what the browser gets to see. Indeed this appears to be a configuration issue with the Cambridge web server. For some of my personal pages (also delivered from Cambridge), the W3C validator shows a warning The character encoding specified in the HTTP header (utf-8) is different from the value in the meta element (iso-8859-1). So it would seem that the Cambridge web server erroneously expects all web pages to be UTF-8 encoded. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [rt.cl.cam.ac.uk #73409] Re: Accented characters
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.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [rt.cl.cam.ac.uk #73409] Re: Accented characters
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 encoding only when the page doesn't declare its own encoding. In any case, thanks for your quick and very helpful reply! Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [rt.cl.cam.ac.uk #73409] Re: Accented characters
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 not to assert the encoding, but the distro's default IS. So either way round we can claim that we haven't changed the default! ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Proof General 4.1pre
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 users of PG 3.x with recent Isabelle snapshots or versions from the repository? 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. If there is the slightest doubt we can also keep the odd treatment of pgreal values in Isabelle2011 -- PG 4.1 would work nonetheless, despite our abuse of the protocol. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proof General 4.1pre
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 regularly experienced sync losses in connection with the undo-on-edit feature. I couldn't track this down enough to come up with a useful bug report yet, but it seems that switching off this feature solves the problem. Thus, if 4.1 is going to be used, I would recommend having undo-on-edit switched off by default (maybe this is the case anyway, I am not sure...) Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proof General 4.1pre
Quoting Makarius makar...@sketis.net: 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 using Aquamacs for the native cut-copy-paste. One thing that didn't work was fonts (under the assumption Unicode would produce the same results for both combinations; I have not special fonts installed), and instructions how to do this with minimal intervention would be appreciated. I think also the Isabelle/PG interaction did not work properly, and that's why I gave up in the end. PG 3.7.1.1 and Carbon Emacs 1.6 have their issues as well, but I know how to live with them ... Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] erroneous Legacy feature warnings about secondary search path
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 theory B imports A begin end Theory A loads an arbitrary file from HOL/Library, which is included in the legacy default search path, although the full path is given here to avoid the Legacy feature warning. If I load theory A by itself in ProofGeneral, it imports Cardinality.thy without warning. Similarly, if I load theory B by itself in ProofGeneral, there is no warning. But if I have both A.thy and B.thy open in ProofGeneral, step through A.thy first, and *then* start stepping through B.thy, I get the following warning when I import A from B: ### Legacy feature! File Cardinality.thy located via secondary search path: $ISABELLE_HOME/src/HOL/Library Can anyone explain this behavior? - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proof General 4.1pre
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 have not yet figured out how to set up auto-completion that XEmacs provides with any other Emacs. Does anyone know how to do this? Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
