The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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.

[1] : https://github.com/aa755/nbcoq

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/