Email Gateway (Aug 18 2022 at 14:22): Email Gateway (Aug 18 2022 at 14:22):From: Makarius <makarius@sketis.net>
People probably don't know PG 3.7.1.1 yet: it is PG 3.7.1 with some
minimal modifications to make it work more smoothly on GNU Emacs. It is
available from the Isabelle2009-1 download site.
I am still hoping for a version of PG 4.0 that is ready for prime time,
but for now this old version needs to fill the gap.
Makarius
Email Gateway (Aug 18 2022 at 14:23):From: Tim McKenzie <tjm1983@gmail.com>
Sorry; I intended to send this message to the list the first time
around; I replied to all on a previous message, and didn't notice
that the list wasn't included.
Thanks for your advice, everyone. I've done a bit more testing
with Proof General 3.7.1 and 3.7.1.1 and Emacs 22 and 23.
Although my testing hasn't been exhaustive, here are my
conclusions:
If X-Symbol has been active, but is then turned off, then when
Unicode tokens are turned on, any instances of \<^sub> will
disappear (causing Isabelle to refuse to process the buffer), but
only when you scroll up or down to where they are in the buffer
--- if none are visible when you turn Unicode tokens on, then you
can still successfully process the whole buffer. As long as X-
Symbol is never turned on this problem doesn't occur.
With Unicode tokens turned on, I can enter and process \<^sub>
correctly, but the next character doesn't actually appear as a
subscript. To get, for example, a * with a subscript R, I can
copy and paste it from the output buffer, or I can type *\<^sub>R
and then turn Unicode tokens off and back on again. This is
annoying, but I can live with it for now.
When Unicode tokens are turned on, everything in the Format menu
is greyed out.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 14:23):From: Tim McKenzie <tjm1983@gmail.com>
I posted on this list a while ago about trouble using Emacs 23 with
X-Symbol. The solution I decided to go with was to continue using
Emacs 22 (with Isabelle 2009 and Proof General 3.7.1). This was fine
at home, but this week my university upgraded to Emacs 23.
There was some suggestion of using Unicode tokens with Emacs 23, so I
tried that today. Unfortunately, I'm having trouble with my <^sub>s
disappearing, causing Isabelle to balk at some of the files I'm
editing. Has anyone seen this problem before? Does anyone know how I
might try to fix it? If not, I could ask the university to give me an
Emacs 22 to use, but this doesn't seem like a good long-term solution.
Tim
<><
Email Gateway (Aug 18 2022 at 14:23):From: David Aspinall <David.Aspinall@ed.ac.uk>
Tim's investigation of behaviour is useful (thanks). At a risk of
repeating myself, the summary from my point of view is:
XSymbol is not compatible with Emacs 23,.
Unicode Tokens is experimental in PG 3.7.1.(1) I do not recommend
using it with sub/superscripts. Please read the CHANGES file in the PG
distribution. PG 4.0 has a better implementation.
Mixing Unicode Tokens and X-Symbol in the same session is a recipe for
disaster!
I don't understand the comment about the Format menu. There are two
sub-menus, "Format Char" and "Format Region". Items in Format Region
are greyed out unless there is an active (selected) region.
- David
Tim McKenzie wrote:
Email Gateway (Aug 18 2022 at 14:24):From: Tim McKenzie <tjm1983@gmail.com>
I've just tested this with Proof General 3.7.1.1 and Emacs 22.3.1
and 23.1.1. The Format menu has no submenus. It has only the
following options, all of which are greyed out:
Subscript
Superscript
Supscript1 [sic]
Superscript1
Idsubscript1
Idsuperscript1
This is true regardless of whether I've selected anything.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 14:24):From: David Aspinall <David.Aspinall@ed.ac.uk>
The first version of Unicode Tokens in PG 3.7 was somewhat experimental
and did not use such a robust mechanism. There are warnings about this
in the documentation. If you're going to use Unicode Tokens instead of
X-Symbol, I recommend using a pre-release of PG 4.0, which has a much
improved implementation.
- David
Email Gateway (Aug 18 2022 at 14:26):From: Makarius <makarius@sketis.net>
I recommend using GNU Emacs 22 (Gtk if available) with PG 3.7.1. This is
definitely not a long term solution, but the PG 4 branch (required for
Emacs 23) hardly works at the moment.
Makarius
Email Gateway (Aug 18 2022 at 14:27):From: David Aspinall <David.Aspinall@ed.ac.uk>
I think that's a bit unfair. There are (I'm told) bad problems with
Emacs 23 on some non-Linux platforms, but these are not the fault of PG 4.
There are minor glitches with PG 4 but it is still under development, so
I need people to try it out. Please try it (on Emacs 22 or 23) and
report problems at http://proofgeneral.inf.ed.ac.uk/trac/. Please try
to provide decent test cases for problems as I can't investigate reports
like "messages are sometimes duplicated" or "Emacs 23 runs slowly".
See http://proofgeneral.inf.ed.ac.uk/devel
- D.
Email Gateway (Aug 18 2022 at 14:27):From: Makarius <makarius@sketis.net>
I would say the "messages are sometimes duplicated" problem is similar to
"out of sync with Isabelle" (#299), which is already closed as
"needmoreinfo". These problems are hard to pin down, because they are
probably based on race conditions in PG queue management. Nonetheless,
they are show stoppers.
Makarius
Email Gateway (Aug 18 2022 at 14:27):From: Alexander Krauss <krauss@in.tum.de>
David Aspinall wrote:
I agree that PG 4 needs more testers, but using it does create new
problems, including regular synchronization losses. I am using it for
daily work at the moment, which is possible, but I have to restart from
time to time. I have reported the specific problems that I could nail
down, and most have been fixed (thanks, David), but it still breaks
regularly. This is on a Linux platform with GNU Emacs 23.1.1.
In the end, everybody must find out what works best for him...
Alex
Email Gateway (Aug 18 2022 at 14:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I am currently using Emacs 23 together with PG 3.7.1.1 without X-Symbol
but Unicode tokens and it seems to work quite reasonable, though their
might be problems which I have not encountered yet.
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC