search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
227 stars 36 forks source link

Include position information in the [location] attribute. #54

Closed gmalecha closed 3 years ago

gmalecha commented 3 years ago

This captures position information and includes it in the resulting html. The motivation is to allow integrating other data sources (e.g. timing information).

cpitclaudel commented 3 years ago

Looks great, thanks! But won't this give incorrect results when compiling from reST, or even from a Coq file with comments? The locations that SerAPI returns are relative to the beginning of each chunk, IIRC. And mapping these positions back is not completely trivial, though it can be done. WDYT?

cpitclaudel commented 3 years ago

Also, are you postprocessing the resulting HTML? (Is that why you want to reflect the locations in the generated HTML, too?)

gmalecha commented 3 years ago

I've only needed it for full files, the thought for handling snippets would be to include some hash of the entire snippet, e.g. <doc hash="....">...</doc> but I haven't implemented it yet.

I am not post-processing HTML, but I am using CSS to style different sentences, and might use it for JavaScript selection of elements as well.

gmalecha commented 3 years ago

Let me know if you have a preference for how things should be implemented. In theory, I could also implement this by counting characters in JavaScript, but it doesn't seem as nice.

cpitclaudel commented 3 years ago

Is the hash part to address duplication of line numbers across snippets? I was worrying about the numbers becoming relatively meaningless if they are not actual offsets in the original file — isn't that an issue?

I am not post-processing HTML, but I am using CSS to style different sentences, and might use it for JavaScript selection of elements as well.

Can you give me an example? If we invest in attaching info to each span, I'd like to make sure that this is info that will be generally useful.

Let me know if you have a preference for how things should be implemented. In theory, I could also implement this by counting characters in JavaScript, but it doesn't seem as nice.

I agree with you that that doesn't sound nice. But if you want to attach info to a given sentence, for example, then what you could do instead of offsets is use the index of that sentence in the file: document.querySelectorAll(".alectryon-input")[n] — that should be as robust as byte offsets.

Alternatively, you could use an Alectryon transform to attach the info you care about onto the sentence, and then subclass the html renderer to print that info into an attribute.

I think with an example I might be able to help more ^^

gmalecha commented 3 years ago

The reason for using position information is it is the information that it printed by TIMED=1 from Coq. I can use relative positions in that file instead.