The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 03/03/2016 09:59 PM, Lucian M. Patcas wrote:
> Hi Clément,
Hi Lucian,

> 1. Is it possible to disable subscripting? I have many identifiers of
> the form c_n, where c is a string and n a number that I don't want to
> be displayed as a subscript.

Sure; `M-x company-coq-toggle-feature RET smart-subscripts RET` will disable 
them temporarily. To make that change permanent, use `M-x customize-variable 
RET company-coq-disabled-features RET`

> 2. Can comments be prettified?

They are in Emacs 25, which is currently in pretest. In 24, the 
prettification code isn't flexible enough.

> 3. Is it possible to generate prettified coqdoc documents?

Do you mean prettifying symbols inside of code blocks in comments ([…])? If 
so, yes, but only in Emacs 25.
Or did you have something else in mind?

> 4. I don't want Prop, bool etc to be prettified. What file do I have
> to edit to remove this behaviour?

No need to edit a file :) It should be enough to customize the variable 
`company-coq-prettify-symbols-alist`.

Cheers,
Clément.

> On 3 March 2016 at 11:42, Clément Pit--Claudel 
> <clement.pit AT gmail.com
> <mailto:clement.pit AT gmail.com>>
>  wrote:
> 
> I think prettification offers an interesting middle ground (see an
> example at
> https://github.com/cpitclaudel/company-coq/#prettification-of-operators-types-and-subscripts;
> these two screenshots show the same Emacs buffer, with and without
> the prettification layer). This should allow both kinds of SW
> engineers to work on the same files.
> 
> Clément.
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature