Open jeetu7 opened 4 years ago
jeetu7
commented
4 years ago For an example source idr file, pygments can generate prettly decent colorful html. The colors and lexer itself is customizable. Check the rarw code of gists input idr fileand output html. The output html should be downloaded and opened in your browser. Command used is as follows:
pygmentize -f html -O full -o /tmp/x.html ~/tmp/example.idr
So getting to html colorful code is easy. Next is linking it with declarations.
jeetu7
commented
4 years ago For linking, we have to customize (extend) the html formatter for idris1 in pygments. And also, to make it support idris2, we might have to extend the pygment's lexer as well.
For doing the linking part, we should be able to get this information from the idris2 compiler about how it parses and resolves the declaration and usage of types/variable/functions etc. Assuming the above information is available, conceptually the process of linking can go like this
Extracts information from compiling process about which line the compiler sees the token usage (which we want to show as clickable) and which we want to link to (the declaration of that token)
Modify the formatter of the pygment to add anchor to each line so that it can be hyperlinked to. Ref Html anchor links
Generate output file with line numbered source code in html (with anchors for each line number id-ed as line number itself). Example with line numbers is already possible with pygments Line numbered html output
pygmentize -f html -O full,linenos=1 -o /tmp/x.html ~/tmp/example.idr
Use this information in the formatter, or might be a second pass by some other script.
gallais
commented
4 years ago Do we gain much by using pygment rather than outputting e.g. markdown to be post-processed by pandoc?
Re, looking at rendered examples we can use htmlpreview.github.io. See for instance: your syntax highlighted file
jfdm
commented
4 years ago We must also look at how it works in Idris1 where you can use the --highlight flag dump an SExpr containing highlighting information. There is a tool idrishl which can generate HTML and LaTeX sources. The SExpr is a version of the same information sent out by Idris1 IDE mode for highlighting, and the source is the same information used by idrisdoc Idris1's javadoc like tool
jeetu7
commented
4 years ago @jfdm @gallais I will look into them. I might be little slow as I am learning Idris along the way.
Also any pointers, at which point I can get the info about compiler finding the linking of declaration of tokens and their usages. Where should I start (which file or written material). Can I store the info in some output file as in ctags. Or do I have to decipher the scheme output for that.
My aim is to get it going using whichever way is possible to get a wroking method. Then switch it step by step to better tools (preferably self contained idris methods).
Generate line numbered linkable source code. Now you can link to a particular line using
file:///tmp/x.html#line-5. Check the bottom two links for only html and particular line linked. You might have to reduce the size of the browser to actually notice the difference.
pygmentize -f html -O full,linenos=1,lineanchors=line -o /tmp/x.html ~/tmp/example.idr
MarcelineVQ (at IRC) pointed at the Agda browsable source code. Agda stdlib example . This looks good for browsing source code, wherein we can go through various variables and jump across the code for declarations/definitions etc. Also, we can discuss various approaches for doing the same here.