Browsable source code

[jeetu7]

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.

• Browsable code for Idris2.
• Hosting Idris2 Browsable Code (probably on github.ion as Agda itself)
• Mechanism to convert local code written in Idris2 for local browsing.

[jeetu7]

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]

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

1. 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)

2. Modify the formatter of the pygment to add anchor to each line so that it can be hyperlinked to. Ref Html anchor links

3. 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

4. Use this information in the formatter, or might be a second pass by some other script.

[gallais]

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]

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]

@jfdm @gallais I will look into them. I might be little slow as I am learning Idris along the way.

1. 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.

2. 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).

3. 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

https://htmlpreview.github.io/?https://gist.githubusercontent.com/jeetu7/2873ac9befd63b1b0ef87347b5e41540/raw/3423e337d024df2f41653b2bd52614b1e6b7cb33/idris_doc_2.html

https://htmlpreview.github.io/?https://gist.githubusercontent.com/jeetu7/2873ac9befd63b1b0ef87347b5e41540/raw/3423e337d024df2f41653b2bd52614b1e6b7cb33/idris_doc_2.html#line-5