coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] color info from coqdoc and .vo from coqtop
- Date: Fri, 16 May 2014 20:46:10 -0400
1) Is it possible for coqdoc to output the syntax coloring information (which it already computes to generate latex/html) in a format that I could easily use to implement syntax highlighting in my plugin [1] ? Ideally, it could be like a list of triples:
start_pos, end_pos, color
The positions index into the .v file.
Currently, I will have to somehow align the html generated by coqdoc
with the corresponding .v file in order to figure out the colors that my plugin should
use to render the .v file.
Is there an easier way to implement a more semantic syntax highlighting, similar
to the agda-emacs, or coqdoc's latex/html outputs, but unlike the simplistic style of CoqIDE?
For example, CoqIDE's colors don't distinguish inductive types from defined constants.
If someone could point me to the parts of coqdoc sources that I need to modify, that would be helpful too.
2) Is it possible to get the .vo file from the coqtop -ideslave
process after my plugin (or any other IDE) has fed to it the entire contents of a .v file?
A major use case would be a faster way to automatically compile all the dependencies of a .v file that a user opens using my plugin.
Suppose a user of my plugin opened the file A.v
and it has a line "Require Export B.v"
Currently, I compile the B.v using coqc.
However, if a compilation error occurs,
I have to open B.v file in the editor and then
feed the contents of it (to coqtop -ideslave) till the error location.
The user can then fix the error in B.v.
This is sometimes a huge waste of time for big files.
I wish my plugin could use coqtop even to compile the dependencies so
that if an error occurs, no duplicate work has to be done.
Proof general already does something similar. I'd be grateful to know how it manages to do the dependency compilation efficiently.
Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/- [Coq-Club] color info from coqdoc and .vo from coqtop, Abhishek Anand, 05/17/2014
- Re: [Coq-Club] color info from coqdoc and .vo from coqtop, AUGER Cédric, 05/17/2014
- Re: [Coq-Club] color info from coqdoc and .vo from coqtop, Abhishek Anand, 05/24/2014
- Re: [Coq-Club] color info from coqdoc and .vo from coqtop, AUGER Cédric, 05/17/2014
Archive powered by MHonArc 2.6.18.