The Coq mailing list

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

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 02/20/2015 03:20 PM, Pierre-Marie Pédrot wrote:
> That is strange, because trunk does understand that sort of parlance.

Ah, Indeed, it works for me too. A silly mistake. Are there examples of to 
interoperate with this? I found a few minimal references online, but no 
simple examples.

> What use case are you exactly hoping for? 

I'm hoping to get better auto-completion support in proof-general. The idea 
is that if I can get a list of known identifiers, I can feed that to 
company-mode, and get suggestions as I type for theorem names. I have that 
working currently, but with the plain coq toplevel parsing through the huge 
output of SearchPattern takes a while.

The patch that I'm currently using solves this nicely by letting you 
constrain the output of all search functions to just names instead of 
names+types.

> I do not know the exact
> state of ProofGeneral, and I do not know if the latest version uses the
> XML protocol (which I doubt), but if that is the case, you're going to
> run into trouble...

I don't think PG uses XML. I'm not familiar at all with the XML protocol, 
either; I'll look into this, thanks for the pointer!

Other than that, is there no way to list identifiers when the toplevel is 
started with just coqtop? I think a feature to just list identifiers would be 
useful, until PG transitions to the apparently better XLM-based interface at 
least.

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1

iQEcBAEBAgAGBQJU552OAAoJEC0HUjwO/okMaTgH/jX6J6xItGc6N2P9ICdAOIMV
qNpQt1iAXh3YK/DYp0vGd4PFr5UAqTcZm8/3U3Gv8vMefid7SuTZXPEFztRPiFBo
M9lr6Y4kDekIl1BxdTZej1RuYiMHSjIZqi/e93ObOGLnmGj1b1DSU5241SEdj5Uw
4NdGnHwqFGB2RZe1sVXMfF68PE5vOoJz3keY29P8Ie6UBvkvIYbHNw9JRR56lFxW
niQeaWZfG2HcjEnbjztlVYre39BsVUz6IDqVO3ou3f9CDAB78yap3VniP7L6X0aK
imKJ+o/orMqEnw+6mJYlZbF2paON6AoPE3qPogWMlT/3AAp/oVUuRZ1Z4xlOdtU=
=2Qg/
-----END PGP SIGNATURE-----