Email Gateway (Aug 18 2022 at 14:16): Email Gateway (Aug 18 2022 at 14:16):From: Makarius <makarius@sketis.net>
I've also seen this marker, but only as a small graphical triangle left of
the text area. (This was something like GNU Emacs 23.1.1.)
Makarius
Email Gateway (Aug 18 2022 at 14:17):From: David Aspinall <David.Aspinall@ed.ac.uk>
I replied off list to Rafal as I didn't try the fix:
(setq overlay-arrow-string "")
This marker is shown as text in tty mode when the graphical triangle
isn't available. It has the same overwriting behaviour where it's used
in other Emacs modes (e.g., edebug). The arrow doesn't get in the way
when the text is indented beyond the first column.
- David
Email Gateway (Aug 18 2022 at 14:17):From: Makarius <makarius@sketis.net>
As we are moving towards the next official release, I would love to see
the COMPATIBILITY more or less coincide with what we will recommend on our
installation web page.
Any feedback on various Linuxes, Mac OS, Cygwin is particularly welcome.
(Native Windows is not used for Isabelle Proof General.)
Makarius
Email Gateway (Aug 18 2022 at 14:18):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Any feedback on various Linuxes, Mac OS, Cygwin is particularly welcome. (Native Windows is not used for Isabelle Proof General.)
I know that xemacs is not a blessed version any more anyway, but one data point that may be interesting nevertheless:
I haven't managed so far to get any version of xemacs from the stable branch to work with Isabelle on Mac OS 10.6 (Snow Leopard).
The problem is with xemacs, not Isabelle: no version I've tried (current 21.4.22 from macports and fink, 21.4.20_3 from macports, 21.4.22 compiled from source, some other versions compiled from source) manages to start an external process (not even grep). Symptoms vary slightly, but mostly xemacs just hangs and takes 100% of one CPU. All of these work fine with Mac OS 10.5.
Current Carbon Emacs (based on GNU Emacs 22.3.1) seems to work reasonably well with current PG cvs, but only with Unicode Tokens, which frankly by default look horrible.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 14:18):From: Norbert Schirmer <schirmer@in.tum.de>
That depends on the default! If you magically get the fonts provided with isabelle (lib/fonts) it actually looks quite good!
Norbert
Email Gateway (Aug 18 2022 at 14:19):From: Makarius <makarius@sketis.net>
So how does it work on Ubuntu, then? In recent updates of both Ubuntu and
Java I've experienced some degradation of anti-aliasing. Maybe your
alternative setup can improve upon that.
Makarius
Email Gateway (Aug 18 2022 at 14:19):From: Gerwin Klein <gerwin.klein@nicta.com.au>
This may be my own fault actually, it is using some other default, not the Isabelle fonts.
Thanks for the hint, I'll see if I can get it to use lib/fonts instead.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 14:19):From: Makarius <makarius@sketis.net>
BTW, the (crude) truetype fonts shipped with Isabelle (and another version
with Proof General) are just homegrown by myself, but they turned out to
be less ugly than some others so I agreed to make them more widely
available.
I am still hoping for Stix to be released soon. It was announced for
September (actually in 2005), again for September this year, but there
have been further delays. Maybe next year, when GNU Hurd 1.0 comes out
...
Makarius
Email Gateway (Aug 18 2022 at 14:19):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Makarius wrote:
This might be slightly off-topic for the list, but I'm posting it here
in case someone finds it useful.
Well, my way of doing things won't necessarily help make your
antialiasing better, as I just turn it off. However, this level of
font-tweaking allows much finer control than anything available through
the GUI so you may find something to your liking.
Basically, I started with this guide and changed my system fonts to be
the microsoft ones:
http://ubuntuforums.org/showthread.php?t=208396
In /etc/fonts you can create a file local.conf where you can place
whatever settings you wish such that they won't get killed by ubuntu
upgrades etc. Changing the contents of this file and files it includes
gives immediate feedback within the system (I'm on 9.10), including in
character map, but NOT emacs. I think emacs needs a restart for these to
show up.
Mine just basically includes other things (first three files are from
the ubuntu forums link)
<include ignore_missing="yes">local-misc.conf</include>
<include ignore_missing="yes">local-aliases.conf</include>
<include ignore_missing="yes">local-msfonts-rules.conf</include>
<include ignore_missing="yes">local-raf.conf</include>
In local-misc, I changed my default treatment of fonts to:
<match target="font" >
<edit mode="assign" name="antialias" >
<bool>false</bool>
</edit>
<edit mode="assign" name="autohint" >
<bool>true</bool>
</edit>
<edit mode="assign" name="hintstyle" >
<const>hintslight</const>
</edit>
</match>
Which means turn off antialiasing, then enable the autohinter at a weak
setting by default.
So for fonts that come with their own hinting and aren't part of
msfonts, in local-raf.conf I define:
<!-- Fonts with their own hinting -->
<match target="font">
<test name="family">
<string>Lucida Console</string>
<string>BitStream Vera Serif</string>
<string>Cambria</string>
<string>Cambria Math</string>
</test>
<edit mode="assign" name="hinting">
<bool>true</bool>
</edit>
<edit name="autohint">
<bool>false</bool>
</edit>
</match>
For fonts that don't come with good hinting but the autohinter can deal
with:
<!-- I want to keep these aliased, but they look tragic without some
hinting -->
<match target="font">
<test name="family">
<string>Code2000</string>
<string>STIXGeneral</string>
<string>DejaVu Sans</string>
<string>DejaVu Sans Mono</string>
</test>
<edit mode="assign" name="autohint" >
<bool>true</bool>
</edit>
<edit mode="assign" name="hintstyle" >
<const>hintfull</const>
</edit>
</match>
And finally there are fonts where there is nothing you can do, they
simply were designed to be antialiased and subpixel smoothed:
<match target="font">
<test name="family">
<string>Consolas</string>
</test>
<edit mode="assign" name="antialias">
<bool>true</bool>
</edit>
<edit mode="assign" name="rgba">
<const>rgb</const>
</edit>
</match>
You can do other pretty tricks like antialiasing fonts once they go
beyond a certain size, but the above is sufficient to outline the basic
idea. I'm attaching my local config from /etc/fonts for those who want
to play around with it.
Sincerely,
Rafal Kolanski.
localfonts.zip
Email Gateway (Aug 18 2022 at 14:22):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Isabelle Users,
In PG 4.0 (CVS), in addition to colour, the progress through a theory is
marked with a "=>" at the next command to be processed. So:
text {* blah *}
lemma "1 + 1 = 2" oops
after one command advance becomes:
text {* blah *}
=>mma "1 + 1 = 2" oops
I do not like this, but I cannot turn it off. I've looked through all
the menus and don't see it, I've grepped though the PG source looking
for a "=>" I could turn into "", but haven't found anything relevant.
Does anyone know what I don't?
Sincerely,
Rafal Kolanski.
Last updated: Apr 18 2024 at 16:19 UTC