feat: optimize pp-display for a better and faster goal view and query panel #900
Conversation
|
Funny that half of the citations in that paper are by Gerard Huet and Gilles Kahn... |
This is a total reimplementation of the pp-display library which uses Oppen's algorithm to format the goals correctly. It is much much faster and corrects a number of display problems.
rtetley
changed the title
| case DisplayType.box: | ||
| currentWidth += estimateBoxWidth(childBox, context); | ||
| break; | ||
| case DisplayType.break: |
There was a problem hiding this comment.
I haven't tried out this, but I believe the estimation would be more accurate if
- a
BreakwithshouldBreak: trueresets the current width estimateBoxWidthreturns the max width
There was a problem hiding this comment.
I am not sure what you mean ?
Currently the estimation of whether to break or not does not happen here but rather in the scanTokenStream function.
The box always has the max width but its only relevant to breaks if a box is a hvBox in which case all its breaks should happen.
Otherwise we use the estimation of a block which happens from break to break.
There was a problem hiding this comment.
Thanks, now I understand the algorithm. btw it seems the use of estimateBoxWidth in buildTokenStream results in a runtime that is quadratic wrt the depth of box. Maybe that's fine.
There was a problem hiding this comment.
Yeah, I agree there is definitely a more optimal way to do this. However buildTokenStream is only called once on receiving a ppString and in practice, even on examples that use to take a considerable amount of time, this version speeds everything up by an order of magnitude. I think there will be time later down the road to optimise this further.
This PR aims at making a better pretty printing algo for the goal view.
It is heavily inspired by the Oppen algorithm.
Closes #859
Closes #869
Closes #752
Closes #835