Consider using default font-lock -- faces not readable in many "dark" emacs color themes

[UlfNorell]

From jimburt...@gmail.com on June 30, 2009 12:31:24

agda2-highlight.el sets values for font-lock faces which are unreadable when using a "dark" emacs color theme such as color-theme-gray30, and which look very odd in terminal mode. This can be changed by customising the group, but most major-modes for programming languages, such as the haskell-mode, use the defaults. In this way, keywords etc are highlighted so that they are visible with any theme and consistent with other programming modes. Group customisation isn't ideal -- when trying to customise the group to use the defaults it is difficult to find out which foreground colour is used in the default face for, say, function names, and hard-coding it means it might still be hard to read in a terminal. If the user then switches color themes (e.g. to a light one for presentations) they may need to do the whole thing again.

I've attached a patch which makes agda2-highlight use the defaults (mostly) but it breaks the group customisation, so I wouldn't have thought it's what you want. What would be ideal would be font-locking that uses the defaults but which is still group customisable. The value of group customisation is debatable though, as most major modes don't provide it and if you used the defaults probably few users would need to customise them; if they needed to they could use a hook.

Attachment: agda2-highlight.el.faces.patch

Original issue: http://code.google.com/p/agda/issues/detail?id=174

[UlfNorell]

From nils.anders.danielsson on June 30, 2009 08:25:14

I agree that it would be nice if we could use the default font-lock faces. There are some problems with this, though:

• I have not found a reasonable mapping between font-lock's faces and Agda's "aspects". Your patch merges some of the aspects and uses Agda-specific faces for others.
• Sometimes several aspects apply to a single character. For instance, it is possible to uniformly underline operators, but use different foreground colours for those operators which are constructors and those which are not.

However, the problem that you mention can be partially solved. One can use different settings depending on whether the background colour is light or dark:

(defface agda2-highlight-symbol-face '((((background light)) (:foreground "gray25")) (((background dark)) (:foreground "gray75"))) "The face used for symbols like forall, =, ->, etc." :group 'agda2-highlight)

If you think this is a reasonable compromise then it would be helpful if you could supply a patch.

Status: InfoNeeded

[UlfNorell]

From jimburt...@gmail.com on June 30, 2009 14:31:56

Hi, personally I don't think it's important that every aspect is reflected in the face used. In fact, if you do this you can end up with a visually cluttered look which is counter-productive. E.g., I'd be happy for operators to use one face and, if I want to know which are constructors, refer to the definitions or rely on what I know already about them...I can see that this might seem like a backwards step for you. (The reason I left some agda faces in the patch is because I wasn't sure which default to use, but as I say I would err on the side of a quieter interface, such as giving both inductive and coinductive constructors font-lock-type-face.)

What about using font-lock levels? If we had level 1 using font-lock defaults (and providing less info) and level 2 working the way it does now, as I understand it everyone would get level 2, the status quo, unless they lowered the level, which people like me could do. If you think this sounds OK I'll work it out how to do it and fix something up.

[UlfNorell]

From nils.anders.danielsson on July 01, 2009 09:09:54

I agree that there is a risk of clutter, that's why by default some aspects are ignored, and others highlighted identically. However, I want to give the users the option to choose which things to highlight, rather than making the decision for them.

Your suggestion sounds OK with me, except that, instead of using font-lock levels (which come with certain conventions about what they mean), I would prefer to see another option added to agda2-highlight-face-groups.

Status: Accepted
Labels: Type-Enhancement Priority-Low

[UlfNorell]

From jimburt...@gmail.com on July 01, 2009 14:38:23

The attached patch works as you suggest, adding an option to agda2-highlight-face-groups. It does the trick but the only caveat is that changing themes requires you to customize the group again, as saving the customization puts hard coded values in .emacs. But it's a quicker way to get readable faces for any theme, so hopefully it should be useful (to me, if no one else! :-)).

Attachment: agda2-highlight.default-faces.patch

[UlfNorell]

From nils.anders.danielsson on July 01, 2009 17:05:58

Thanks. I'll probably have a proper look at your patch later this month (I'm quite busy right now).

Owner: nils.anders.danielsson

[UlfNorell]

From nils.anders.danielsson on July 21, 2009 06:52:48

Can you create a patch using darcs send instead?

Note that all functions and variables in agda2-highlight.el should be named agda2-highlight-.

"changing themes requires you to customize the group again, as saving the customization puts hard coded values in .emacs":

There is no reason to save the values of agda2-highlight-*-face when agda2-highlight-face-groups is used, so after changing themes it suffices to restart Emacs. For a smoother behaviour you could perhaps add a call to agda2-highlight-set-faces to some face- or theme-related hook, or to agda2-highlight-reload.

[UlfNorell]

From jimburt...@gmail.com on July 22, 2009 08:23:16

I renamed a couple of functions accordingly and here's a darcs patch. I'm not a darcs user, so I'm hoping this is done correctly. Re your comment, you're right that restarting emacs is sufficient to get the new default faces, which seems fine.

Attachment: agda2-highlight.default-faces.diff

[UlfNorell]

From nils.anders.danielsson on July 23, 2009 08:24:10

Status: Fixed