Closed tkw1536 closed 5 years ago
Comment by @kohlhase:
Indeed, this is very good to know. I think this should be integrated into some kind JOBAD-like functionality. The IDs are of the form
So we only need to export the sourcerefs we have which have a file and line number component (start line number) through the presentation process. Then we can pick up the source references via JS.
Done.
Original issue UniFormal/MMT#402 by @florian-rabe:
When viewing sources in gitlab, every line has an id attribute.
So we can add links to the sources files to all MMT elements that have source references. We should do that.