[Agda] Re: A patch to agda2-mode.el

[Makoto Takeyama]

Dear all,

This is a minor warning about a behaviour change of agda2-mode (when
Ulf applies my patch).

If you are customising `agda2-change-default-font' to nil ("Don't change"),
that setting will be ignored after the patch.  To keep the "Don't change"
behaviour, please instead customise the new option `agda2-fontset-name'
to nil.


and Nisse,
> I noticed that you have selected a different default font size for
> Windows. Is this intentional?

Yes.  The current default 9x15 does not have a matching Kanji font but
9x18 does (regardless of X or Windows).  While we here on win needed
matching Kanji badly, I thought others would not prefer it to less
lines of taller chars.

Best Wishes,

Makoto


On Thu, 4 Sep 2008 17:35:41 +0100
"Nils Anders Danielsson" <nils.anders.danielsson at gmail.com> wrote:

> On Thu, Sep 4, 2008 at 08:11, Makoto Takeyama
> <makoto.takeyama at aist.go.jp> wrote:
> >
> > The new customisable variable agda2-fontset-name (default
> > "fontset-agda2") gives the fontset to which the current frame's
> > default is changed, or it is nil and the current frame's default is
> > unchanged.
> 
> You should post about this to the Agda list so that people do not get
> surprised when their font suddenly starts changing again.
> 
> > Another costomisable agda2-fontset-spec-of-fontset-agda2 is the
> > specification string for the fontset fontset-agda2 (which may not be
> > used if agda2-fontset-name is not "fontset-agda2").  The default spec
> > string is the same as before for non-windows.
> 
> I noticed that you have selected a different default font size for
> Windows. Is this intentional?
> 
> -- 
> /NAD

On Thu, 04 Sep 2008 16:11:05 +0900
Makoto Takeyama <makoto.takeyama at aist.go.jp> wrote:

> Hi Nisse and Ulf,
> 
> I have uploaded a patch "indirection_for_fontset-agda2" to agda2-mode.el
> at Agda Wiki
> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Patch.Submitted
> 
> This adds a level of indirection for the fontset to use for Agda.
> This change allows a fontset defined elsewhere to be used.
> 
> The new customisable variable agda2-fontset-name (default
> "fontset-agda2") gives the fontset to which the current frame's
> default is changed, or it is nil and the current frame's default is
> unchanged.
> 
> Another costomisable agda2-fontset-spec-of-fontset-agda2 is the
> specification string for the fontset fontset-agda2 (which may not be
> used if agda2-fontset-name is not "fontset-agda2").  The default spec
> string is the same as before for non-windows.
> 
> (I needed to change the default fontset spec now to align Japanese
> double-width characters.  Along the way I learned that specifying
> fontset spec directly is not the right way.  So far I could achieve
> the goal only with the wrong way (the right way is too dependent on
> environments), but hoping some Chinese/Japanese/Korean somewhere
> must have solved the problem already.)
> 
> Best Wishes,
> Makoto


-- 
Makoto Takeyama <makoto.takeyama at aist.go.jp>
AIST/CVS (National Institute of Advanced Industrial Science and Technology /
          Research Center for Verification and Semantics)
tel: +81-6-4863-5019   fax: +81-6-4863-5052