aya-dev
aya-dev copied to clipboard
aya-prover
A faithful pretty printer
There should be a pretty printer that only adds highlight/links/attributes to the input code, and doesn't change anything in the output. Similar to Agda's literate mode.
Implementation wise, I guess it's something that traverse the tree while holding an iterator of the token sequence. We could start from SyntaxHighlight.java
Like some RainbowVisitor?
Well I'm not sure wdym by rainbow visitor. I think the one in intellij is unrelated
We already have it: SyntaxHighlight.java. But it needs some generalization.
Most likely we're going to migrate to GK so it should worth doing this task later
We already have it: SyntaxHighlight.java. But it needs some generalization.
Most likely we're going to migrate to GK so it should worth doing this task later
Are we going to perform annotation together with parsing? If not, this issue might not depend on a GK parser.
We already have it: SyntaxHighlight.java. But it needs some generalization.
Most likely we're going to migrate to GK so it should worth doing this task later
Are we going to perform annotation together with parsing? If not, this issue might not depend on a GK parser.
The GK parser will surely deprecate the current Aya Lexer I guess
We already have it: SyntaxHighlight.java. But it needs some generalization.
SyntaxHighlight looks don't add any links.
We already have it: SyntaxHighlight.java. But it needs some generalization.
SyntaxHighlightlooks don't add any links.
Seems that we need to combine SyntaxHighlight and some code in CoreDistiller...
It would be nice if we can reuse these code. At least, SyntaxHighlight should be reused.
Seems that we need to combine
SyntaxHighlightand some code inCoreDistiller...
But the SyntaxHighlither/FaithfulDistiller will work with Concretes instead of Cores. However, this is not a serious problem.
I agree. By CoreDistiller I probably only mean the pp of those DefVars, which are still present in concrete